Samuel MIMRAM

Contents

0 Introduction 10
0.1 Proving instead of testing . . . . . . . . . . . . . . . . . . . . . . 10
0.2 Typing as proving . . . . . . . . . . . . . . . . . . . . . . . . . . 11
0.3 Checking programs . . . . . . . . . . . . . . . . . . . . . . . . . . 13
0.4 Checking proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
0.5 Searching for proofs . . . . . . . . . . . . . . . . . . . . . . . . . 15
0.6 Foundations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15
0.7 In this course . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16
0.8 Other references on programs and proofs . . . . . . . . . . . . . . 17
0.9 About this document . . . . . . . . . . . . . . . . . . . . . . . . . 17

1 Typed functional programming 18

1.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.1.1 Hello world . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.1.2 Execution . . . . . . . . . . . . . . . . . . . . . . . . . . . 18
1.1.3 A statically typed language . . . . . . . . . . . . . . . . . 19
1.1.4 A functional language . . . . . . . . . . . . . . . . . . . . 19
1.1.5 Other features . . . . . . . . . . . . . . . . . . . . . . . . 20
1.2 Basic constructions . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.2.1 Declarations . . . . . . . . . . . . . . . . . . . . . . . . . . 20
1.2.2 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 21
1.2.3 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.2.4 Products . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.2.5 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22
1.2.6 Strings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.2.7 Unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.3 Recursive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.3.1 Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 23
1.3.2 Usual recursive types . . . . . . . . . . . . . . . . . . . . . 24
1.3.3 Abstract description . . . . . . . . . . . . . . . . . . . . . 26
1.3.4 Option types and exceptions . . . . . . . . . . . . . . . . 28
1.4 The typing system . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1.4.1 Usefulness of typing . . . . . . . . . . . . . . . . . . . . . 29
1.4.2 Properties of typing . . . . . . . . . . . . . . . . . . . . . 30
1.4.3 Safety . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
1.5 Typing as proving . . . . . . . . . . . . . . . . . . . . . . . . . . 38
1.5.1 Arrow as implication . . . . . . . . . . . . . . . . . . . . . 38
1.5.2 Other connectives . . . . . . . . . . . . . . . . . . . . . . 38
1.5.3 Limitations of the correspondence . . . . . . . . . . . . . 40
CONTENTS 3

2 Propositional logic 41
2.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41
2.1.1 From provability to proofs . . . . . . . . . . . . . . . . . . 41
2.1.2 Intuitionism . . . . . . . . . . . . . . . . . . . . . . . . . . 42
2.1.3 Formalizing proofs . . . . . . . . . . . . . . . . . . . . . . 43
2.1.4 Properties of the logical system . . . . . . . . . . . . . . . 44
2.2 Natural deduction . . . . . . . . . . . . . . . . . . . . . . . . . . 44
2.2.1 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.2.2 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45
2.2.3 Inference rules . . . . . . . . . . . . . . . . . . . . . . . . 46
2.2.4 Intuitionistic natural deduction . . . . . . . . . . . . . . . 46
2.2.5 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
2.2.6 Fragments . . . . . . . . . . . . . . . . . . . . . . . . . . . 49
2.2.7 Admissible rules . . . . . . . . . . . . . . . . . . . . . . . 49
2.2.8 Definable connectives . . . . . . . . . . . . . . . . . . . . 52
2.2.9 Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . 53
2.2.10 Structural rules . . . . . . . . . . . . . . . . . . . . . . . . 54
2.2.11 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . 55
2.3 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56
2.3.1 Cuts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 57
2.3.2 Proof substitution . . . . . . . . . . . . . . . . . . . . . . 57
2.3.3 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . 58
2.3.4 Consistency . . . . . . . . . . . . . . . . . . . . . . . . . . 61
2.3.5 Intuitionism . . . . . . . . . . . . . . . . . . . . . . . . . . 62
2.3.6 Commutative cuts . . . . . . . . . . . . . . . . . . . . . . 63
2.4 Proof search . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 65
2.4.1 Reversible rules . . . . . . . . . . . . . . . . . . . . . . . . 65
2.4.2 Proof search . . . . . . . . . . . . . . . . . . . . . . . . . . 66
2.5 Classical logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67
2.5.1 Axioms for classical logic . . . . . . . . . . . . . . . . . . 70
2.5.2 The intuition behind classical logic . . . . . . . . . . . . . 72
2.5.3 A variant of natural deduction . . . . . . . . . . . . . . . 74
2.5.4 Cut-elimination in classical logic . . . . . . . . . . . . . . 76
2.5.5 De Morgan laws . . . . . . . . . . . . . . . . . . . . . . . 77
2.5.6 Boolean models . . . . . . . . . . . . . . . . . . . . . . . . 81
2.5.7 DPLL . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 83
2.5.8 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 85
2.5.9 Double-negation translation . . . . . . . . . . . . . . . . . 91
2.5.10 Intermediate logics . . . . . . . . . . . . . . . . . . . . . . 93
2.6 Sequent calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
2.6.1 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 94
2.6.2 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95
2.6.3 Intuitionistic rules . . . . . . . . . . . . . . . . . . . . . . 98
2.6.4 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . 98
2.6.5 Proof search . . . . . . . . . . . . . . . . . . . . . . . . . . 98
2.7 Hilbert calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
2.7.1 Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 102
2.7.2 Other connectives . . . . . . . . . . . . . . . . . . . . . . 104
2.7.3 Relationship with natural deduction . . . . . . . . . . . . 105
2.8 Kripke semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 106
CONTENTS 4

2.8.1 Kripke structures . . . . . . . . . . . . . . . . . . . . . . . 106

2.8.2 Completeness . . . . . . . . . . . . . . . . . . . . . . . . . 108

3 Pure λ-calculus 111

3.1 λ-terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
3.1.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 112
3.1.2 Bound and free variables . . . . . . . . . . . . . . . . . . . 113
3.1.3 Renaming and α-equivalence . . . . . . . . . . . . . . . . 113
3.1.4 Substitution . . . . . . . . . . . . . . . . . . . . . . . . . . 114
3.2 β-reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
3.2.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 115
3.2.2 An example . . . . . . . . . . . . . . . . . . . . . . . . . . 116
3.2.3 Reduction and redexes . . . . . . . . . . . . . . . . . . . . 116
3.2.4 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 116
3.2.5 β-reduction paths . . . . . . . . . . . . . . . . . . . . . . 117
3.2.6 Normalization . . . . . . . . . . . . . . . . . . . . . . . . . 117
3.2.7 β-equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 118
3.2.8 η-equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 118
3.3 Computing in the λ-calculus . . . . . . . . . . . . . . . . . . . . . 119
3.3.1 Identity . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
3.3.2 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . 119
3.3.3 Pairs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 120
3.3.4 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . 121
3.3.5 Fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . 123
3.3.6 Turing completeness . . . . . . . . . . . . . . . . . . . . . 127
3.3.7 Self-interpreting . . . . . . . . . . . . . . . . . . . . . . . 129
3.3.8 Adding constructors . . . . . . . . . . . . . . . . . . . . . 129
3.4 Confluence of the λ-calculus . . . . . . . . . . . . . . . . . . . . . 130
3.4.1 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 130
3.4.2 The parallel β-reduction . . . . . . . . . . . . . . . . . . . 131
3.4.3 Properties of the parallel β-reduction . . . . . . . . . . . . 132
3.4.4 Confluence and the Church-Rosser theorem . . . . . . . . 136
3.5 Implementing reduction . . . . . . . . . . . . . . . . . . . . . . . 137
3.5.1 Reduction strategies . . . . . . . . . . . . . . . . . . . . . 137
3.5.2 Normalization by evaluation . . . . . . . . . . . . . . . . . 143
3.6 Nameless syntaxes . . . . . . . . . . . . . . . . . . . . . . . . . . 148
3.6.1 The Barendregt convention . . . . . . . . . . . . . . . . . 148
3.6.2 De Bruijn indices . . . . . . . . . . . . . . . . . . . . . . . 148
3.6.3 Combinatory logic . . . . . . . . . . . . . . . . . . . . . . 153

4 Simply typed λ-calculus 165

4.1 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
4.1.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
4.1.2 Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . 165
4.1.3 λ-terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
4.1.4 Typing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 166
4.1.5 Basic properties of the typing system . . . . . . . . . . . . 167
4.1.6 Type checking, type inference and typability . . . . . . . 168
4.1.7 The Curry-Howard correspondence . . . . . . . . . . . . . 170
4.1.8 Subject reduction . . . . . . . . . . . . . . . . . . . . . . . 173
CONTENTS 5

4.1.9 η-expansion . . . . . . . . . . . . . . . . . . . . . . . . . . 176

4.1.10 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 177
4.2 Strong normalization . . . . . . . . . . . . . . . . . . . . . . . . . 177
4.2.1 A normalization strategy . . . . . . . . . . . . . . . . . . 177
4.2.2 Strong normalization . . . . . . . . . . . . . . . . . . . . . 178
4.2.3 First consequences . . . . . . . . . . . . . . . . . . . . . . 181
4.2.4 Deciding convertibility . . . . . . . . . . . . . . . . . . . . 182
4.2.5 Weak normalization . . . . . . . . . . . . . . . . . . . . . 183
4.3 Other connectives . . . . . . . . . . . . . . . . . . . . . . . . . . . 185
4.3.1 Products . . . . . . . . . . . . . . . . . . . . . . . . . . . 188
4.3.2 Unit . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 191
4.3.3 Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . 191
4.3.4 Empty type . . . . . . . . . . . . . . . . . . . . . . . . . . 193
4.3.5 Commuting conversions . . . . . . . . . . . . . . . . . . . 194
4.3.6 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . 195
4.3.7 Strong normalization . . . . . . . . . . . . . . . . . . . . . 196
4.4 Curry style typing . . . . . . . . . . . . . . . . . . . . . . . . . . 197
4.4.1 A typing system . . . . . . . . . . . . . . . . . . . . . . . 197
4.4.2 Principal types . . . . . . . . . . . . . . . . . . . . . . . . 198
4.4.3 Computing the principal type . . . . . . . . . . . . . . . . 199
4.4.4 Hindley-Milner type inference . . . . . . . . . . . . . . . . 205
4.4.5 Bidirectional type checking . . . . . . . . . . . . . . . . . 214
4.5 Hilbert calculus and combinators . . . . . . . . . . . . . . . . . . 216
4.6 Classical logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 219
4.6.1 Felleisen’s C . . . . . . . . . . . . . . . . . . . . . . . . . . 219
4.6.2 The λµ-calculus . . . . . . . . . . . . . . . . . . . . . . . 222
4.6.3 Classical logic as a typing system . . . . . . . . . . . . . . 224
4.6.4 A more symmetric calculus . . . . . . . . . . . . . . . . . 226

5 First-order logic 227

5.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
5.1.1 Signature . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
5.1.2 Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 227
5.1.3 Substitutions . . . . . . . . . . . . . . . . . . . . . . . . . 228
5.1.4 Formulas . . . . . . . . . . . . . . . . . . . . . . . . . . . 228
5.1.5 Bound and free variables . . . . . . . . . . . . . . . . . . . 229
5.1.6 Natural deduction rules . . . . . . . . . . . . . . . . . . . 230
5.1.7 Classical first order logic . . . . . . . . . . . . . . . . . . . 231
5.1.8 Sequent calculus rules . . . . . . . . . . . . . . . . . . . . 233
5.1.9 Cut elimination . . . . . . . . . . . . . . . . . . . . . . . . 234
5.1.10 Eigenvariables . . . . . . . . . . . . . . . . . . . . . . . . 235
5.1.11 Curry-Howard . . . . . . . . . . . . . . . . . . . . . . . . 236
5.2 Theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239
5.2.1 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . 239
5.2.2 Properties of theories . . . . . . . . . . . . . . . . . . . . 239
5.2.3 Models . . . . . . . . . . . . . . . . . . . . . . . . . . . . 240
5.2.4 Presburger arithmetic . . . . . . . . . . . . . . . . . . . . 243
5.2.5 Peano and Heyting arithmetic . . . . . . . . . . . . . . . . 244
5.3 Set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 246
5.3.1 Naive set theory . . . . . . . . . . . . . . . . . . . . . . . 246
CONTENTS 6

5.3.2 Zermelo-Fraenkel set theory . . . . . . . . . . . . . . . . . 248

5.3.3 Intuitionistic set theory . . . . . . . . . . . . . . . . . . . 252
5.4 Unification . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 257
5.4.1 Equation systems . . . . . . . . . . . . . . . . . . . . . . . 258
5.4.2 Most general unifier . . . . . . . . . . . . . . . . . . . . . 258
5.4.3 The unification algorithm . . . . . . . . . . . . . . . . . . 259
5.4.4 Implementation . . . . . . . . . . . . . . . . . . . . . . . . 262
5.4.5 Efficient implementation . . . . . . . . . . . . . . . . . . . 263
5.4.6 Resolution . . . . . . . . . . . . . . . . . . . . . . . . . . . 265

6 Agda 268
6.1 What is Agda? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 268
6.1.1 Features of proof assistants . . . . . . . . . . . . . . . . . 268
6.1.2 Installation . . . . . . . . . . . . . . . . . . . . . . . . . . 272
6.2 Getting started with Agda . . . . . . . . . . . . . . . . . . . . . . 272
6.2.1 Getting help . . . . . . . . . . . . . . . . . . . . . . . . . 272
6.2.2 Shortcuts . . . . . . . . . . . . . . . . . . . . . . . . . . . 273
6.2.3 The standard library . . . . . . . . . . . . . . . . . . . . . 274
6.2.4 Hello world . . . . . . . . . . . . . . . . . . . . . . . . . . 274
6.2.5 Our first proof . . . . . . . . . . . . . . . . . . . . . . . . 275
6.2.6 Our first proof, step by step . . . . . . . . . . . . . . . . . 276
6.2.7 Our first proof, again . . . . . . . . . . . . . . . . . . . . 278
6.3 Basic Agda . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 278
6.3.1 The type of types . . . . . . . . . . . . . . . . . . . . . . . 280
6.3.2 Arrow types . . . . . . . . . . . . . . . . . . . . . . . . . . 280
6.3.3 Functions . . . . . . . . . . . . . . . . . . . . . . . . . . . 281
6.3.4 Postulates . . . . . . . . . . . . . . . . . . . . . . . . . . . 282
6.3.5 Records . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283
6.3.6 Modules . . . . . . . . . . . . . . . . . . . . . . . . . . . . 283
6.4 Inductive types: data . . . . . . . . . . . . . . . . . . . . . . . . . 283
6.4.1 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . 284
6.4.2 Pattern matching . . . . . . . . . . . . . . . . . . . . . . . 284
6.4.3 The induction principle . . . . . . . . . . . . . . . . . . . 286
6.4.4 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . 288
6.4.5 Lists . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289
6.4.6 Options . . . . . . . . . . . . . . . . . . . . . . . . . . . . 289
6.4.7 Vectors . . . . . . . . . . . . . . . . . . . . . . . . . . . . 290
6.4.8 Finite sets . . . . . . . . . . . . . . . . . . . . . . . . . . . 291
6.4.9 Integers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 292
6.5 Inductive types: logic . . . . . . . . . . . . . . . . . . . . . . . . 293
6.5.1 Implication . . . . . . . . . . . . . . . . . . . . . . . . . . 293
6.5.2 Product . . . . . . . . . . . . . . . . . . . . . . . . . . . . 293
6.5.3 Unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . 295
6.5.4 Empty type . . . . . . . . . . . . . . . . . . . . . . . . . . 295
6.5.5 Negation . . . . . . . . . . . . . . . . . . . . . . . . . . . 295
6.5.6 Coproduct . . . . . . . . . . . . . . . . . . . . . . . . . . . 296
6.5.7 Π-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 297
6.5.8 Σ-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 298
6.5.9 Predicates . . . . . . . . . . . . . . . . . . . . . . . . . . . 299
6.6 Equality . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 301
CONTENTS 7

6.6.1 Equality and pattern matching . . . . . . . . . . . . . . . 302

6.6.2 Main properties . . . . . . . . . . . . . . . . . . . . . . . . 302
6.6.3 Half of even numbers . . . . . . . . . . . . . . . . . . . . . 303
6.6.4 Reasoning . . . . . . . . . . . . . . . . . . . . . . . . . . . 303
6.6.5 Definitional equality . . . . . . . . . . . . . . . . . . . . . 304
6.6.6 More properties with equality . . . . . . . . . . . . . . . . 305
6.6.7 The J rule . . . . . . . . . . . . . . . . . . . . . . . . . . . 307
6.6.8 Decidable equality . . . . . . . . . . . . . . . . . . . . . . 307
6.6.9 Heterogeneous equality . . . . . . . . . . . . . . . . . . . 308
6.7 Proving programs in practice . . . . . . . . . . . . . . . . . . . . 310
6.7.1 Extrinsic vs intrinsic proofs . . . . . . . . . . . . . . . . . 310
6.7.2 Insertion sort . . . . . . . . . . . . . . . . . . . . . . . . . 312
6.7.3 The importance of the specification . . . . . . . . . . . . . 316
6.8 Termination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 316
6.8.1 Termination and consistency . . . . . . . . . . . . . . . . 316
6.8.2 Structural recursion . . . . . . . . . . . . . . . . . . . . . 317
6.8.3 A bit of computability . . . . . . . . . . . . . . . . . . . . 318
6.8.4 The number of bits . . . . . . . . . . . . . . . . . . . . . . 320
6.8.5 The fuel technique . . . . . . . . . . . . . . . . . . . . . . 320
6.8.6 Well-founded induction . . . . . . . . . . . . . . . . . . . 322
6.8.7 Division and modulo . . . . . . . . . . . . . . . . . . . . . 327

7 Formalization of important results 331

7.1 Safety of a simple language . . . . . . . . . . . . . . . . . . . . . 331
7.2 Natural deduction . . . . . . . . . . . . . . . . . . . . . . . . . . 334
7.3 Pure λ-calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . 336
7.3.1 Naive approach . . . . . . . . . . . . . . . . . . . . . . . . 336
7.3.2 De Bruijn indices . . . . . . . . . . . . . . . . . . . . . . . 337
7.3.3 Keeping track of free variables . . . . . . . . . . . . . . . 340
7.3.4 Normalization by evaluation . . . . . . . . . . . . . . . . . 340
7.3.5 Confluence . . . . . . . . . . . . . . . . . . . . . . . . . . 341
7.4 Combinatory logic . . . . . . . . . . . . . . . . . . . . . . . . . . 344
7.5 Simply typed λ-calculus . . . . . . . . . . . . . . . . . . . . . . . 346
7.5.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 346
7.5.2 Strong normalization . . . . . . . . . . . . . . . . . . . . . 349
7.5.3 Normalization by evaluation . . . . . . . . . . . . . . . . . 353

8 Dependent type theory 358

8.1 Core dependent type theory . . . . . . . . . . . . . . . . . . . . . 358
8.1.1 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 358
8.1.2 Free variables and substitution . . . . . . . . . . . . . . . 359
8.1.3 Contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . 359
8.1.4 Definitional equality . . . . . . . . . . . . . . . . . . . . . 360
8.1.5 Sequents . . . . . . . . . . . . . . . . . . . . . . . . . . . . 360
8.1.6 Rules for contexts . . . . . . . . . . . . . . . . . . . . . . 361
8.1.7 Rules for equality . . . . . . . . . . . . . . . . . . . . . . . 361
8.1.8 Axiom rule . . . . . . . . . . . . . . . . . . . . . . . . . . 362
8.1.9 Terms and rules for type constructors . . . . . . . . . . . 362
8.1.10 Rules for Π-types . . . . . . . . . . . . . . . . . . . . . . . 363
8.1.11 Admissible rules . . . . . . . . . . . . . . . . . . . . . . . 365
CONTENTS 8

8.2 Universes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 366

8.2.1 The type of Type . . . . . . . . . . . . . . . . . . . . . . . 366
8.2.2 Russell’s paradox in type theory . . . . . . . . . . . . . . 366
8.2.3 Girard’s paradox . . . . . . . . . . . . . . . . . . . . . . . 370
8.2.4 The hierarchy of universes . . . . . . . . . . . . . . . . . . 374
8.3 More type constructors . . . . . . . . . . . . . . . . . . . . . . . . 377
8.3.1 Empty type . . . . . . . . . . . . . . . . . . . . . . . . . . 377
8.3.2 Unit type . . . . . . . . . . . . . . . . . . . . . . . . . . . 378
8.3.3 Products . . . . . . . . . . . . . . . . . . . . . . . . . . . 379
8.3.4 Dependent sums . . . . . . . . . . . . . . . . . . . . . . . 380
8.3.5 Coproducts . . . . . . . . . . . . . . . . . . . . . . . . . . 381
8.3.6 Booleans . . . . . . . . . . . . . . . . . . . . . . . . . . . 382
8.3.7 Natural numbers . . . . . . . . . . . . . . . . . . . . . . . 383
8.3.8 Other type constructors . . . . . . . . . . . . . . . . . . . 385
8.4 Inductive types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 385
8.4.1 W-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 386
8.4.2 Rules for W-types . . . . . . . . . . . . . . . . . . . . . . 389
8.4.3 More inductive types . . . . . . . . . . . . . . . . . . . . . 389
8.4.4 The positivity condition . . . . . . . . . . . . . . . . . . . 392
8.4.5 Disjointedness and injectivity of constructors . . . . . . . 396
8.5 Implementing type theory . . . . . . . . . . . . . . . . . . . . . . 397
8.5.1 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . 398
8.5.2 Evaluation . . . . . . . . . . . . . . . . . . . . . . . . . . 399
8.5.3 Convertibility . . . . . . . . . . . . . . . . . . . . . . . . . 401
8.5.4 Typechecking . . . . . . . . . . . . . . . . . . . . . . . . . 403
8.5.5 Testing . . . . . . . . . . . . . . . . . . . . . . . . . . . . 405

9 Homotopy type theory 406

9.1 Identity types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 407
9.1.1 Definitional and propositional equality . . . . . . . . . . . 407
9.1.2 Propositional equality in Agda . . . . . . . . . . . . . . . 407
9.1.3 The rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 408
9.1.4 Leibniz equality . . . . . . . . . . . . . . . . . . . . . . . . 410
9.1.5 Extensionality of equality . . . . . . . . . . . . . . . . . . 411
9.1.6 Uniqueness of identity proofs . . . . . . . . . . . . . . . . 413
9.2 Types as spaces . . . . . . . . . . . . . . . . . . . . . . . . . . . . 415
9.2.1 Intuition about the model . . . . . . . . . . . . . . . . . . 415
9.2.2 The structure of paths . . . . . . . . . . . . . . . . . . . . 419
9.3 n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 421
9.3.1 Propositions . . . . . . . . . . . . . . . . . . . . . . . . . 421
9.3.2 Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 426
9.3.3 n-types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 431
9.3.4 Propositional truncation . . . . . . . . . . . . . . . . . . . 434
9.4 Univalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 445
9.4.1 Operations with paths . . . . . . . . . . . . . . . . . . . . 445
9.4.2 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . 447
9.4.3 Univalence . . . . . . . . . . . . . . . . . . . . . . . . . . 450
9.4.4 Applications of univalence . . . . . . . . . . . . . . . . . . 451
9.4.5 Describing identity types . . . . . . . . . . . . . . . . . . 452
9.4.6 Describing propositions . . . . . . . . . . . . . . . . . . . 453
CONTENTS 9

9.4.7 Incompatibility with set theoretic interpretation . . . . . 454

9.4.8 Equivalences . . . . . . . . . . . . . . . . . . . . . . . . . 457
9.4.9 Function extensionality . . . . . . . . . . . . . . . . . . . 457
9.4.10 Propositional extensionality . . . . . . . . . . . . . . . . . 463
9.5 Higher inductive types . . . . . . . . . . . . . . . . . . . . . . . . 464
9.5.1 Rules for higher types . . . . . . . . . . . . . . . . . . . . 464
9.5.2 Paths over . . . . . . . . . . . . . . . . . . . . . . . . . . . 467
9.5.3 The circle as a higher inductive type . . . . . . . . . . . . 468
9.5.4 Useful higher inductive types . . . . . . . . . . . . . . . . 471

A Appendix 473
A.1 Relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473
A.1.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 473
A.1.2 Closure . . . . . . . . . . . . . . . . . . . . . . . . . . . . 473
A.1.3 Quotient . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474
A.1.4 Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . 474
A.2 Monoids . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 474
A.2.1 Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . 474
A.2.2 Free monoids . . . . . . . . . . . . . . . . . . . . . . . . . 474
A.3 Well-founded orders . . . . . . . . . . . . . . . . . . . . . . . . . 475
A.3.1 Partial orders . . . . . . . . . . . . . . . . . . . . . . . . . 475
A.3.2 Well-founded orders . . . . . . . . . . . . . . . . . . . . . 475
A.3.3 Lexicographic order . . . . . . . . . . . . . . . . . . . . . 476
A.3.4 Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 477
A.3.5 Multisets . . . . . . . . . . . . . . . . . . . . . . . . . . . 478
A.4 Cantor’s diagonal argument . . . . . . . . . . . . . . . . . . . . . 479
A.4.1 A general Cantor argument . . . . . . . . . . . . . . . . . 479
A.4.2 Agda formalization . . . . . . . . . . . . . . . . . . . . . . 481
 Chapter 0

Introduction

These are the extended notes for the course CSC_51051_EP (formerly INF551),
which I am teaching at École Polytechnique since 2019. The goal is to give a
first introduction to the Curry-Howard correspondence between programs and
proofs from a theoretical programmer’s perspective: we want to understand
the theory behind logic and programming languages, but also to write concrete
programs (in OCaml) and proofs (in Agda). Although most of the material is
self-contained, the reader is supposed to be already acquainted with logic and
programming.

0.1 Proving instead of testing

Most of the current software development is validated by performing tests: we
run the programs with various values for the parameters, chosen in order to
cover most branches of the program, and, if no bug has occurred during those
executions, we consider that the program is good enough for production. The
reason for this is that we consider that if the program uses “small” constants
and “regular enough” functions then a large number of tests should be able
to cover all the general behaviors of the program. Seriously following such a
discipline greatly reduces the number of bugs, especially the simple ones, but we
all know that it does not completely eliminates those: in some very particular
and unlucky situations, problems still do happen.
In mathematics, the usual approach is quite different. For instance, when
proving a property P (n) over natural numbers, a typical mathematician will not
test that P (0) holds, P (1) holds, P (2) holds, and so on, up to a big number, and,
if the property is experimentally always verified, claim: “I am almost certain
that the property P is always true”. He will maybe perform some tests in order
to determine whether the conjecture is plausible or not, but in the end he will
write down a proof, which ensures that the property P (n) is always satisfied, for
eternity, even if someone makes a particularly unlucky or perverse choice for n.
Proving instead of testing does require some extra work, but the confidence it
brings to the results is incomparable.
Let us present an extreme example of why this is the right way to proceed.
On day one, our mathematician finds out using a formal computation software
that Z ∞
sin(t) π
dt =
0 t 2
On day two, he tries to play around a bit with such formulas and finds out that
Z ∞
sin(t) sin(t/101) π
dt =
0 t t/101 2
CHAPTER 0. INTRODUCTION 11

On day three, he thinks maybe a pattern could emerge and discovers that
Z ∞
sin(t) sin(t/101) sin(t/201) π
dt =
0 t t/101 t/201 2
On day four, he gets quite confident and conjectures that, for every n ∈ N,
Z ∞ Y n
!
sin(t/(100i + 1)) π
dt =
0 i=0
t/(100i + 1) 2
He then spends the rest of the year heating his computer and the planet, suc-
cessfully proving the conjecture for increasing values of n. This approach seems
to be justified since the most complicated function involved in here is the sine,
which is quite regular (it is periodic), and all the constants are small (we get
factors such as 100), so that if something bad ought to happen it will happen
for a not-so-big value of n and testing should discover it. In fact, the conjecture
breaks starting at
n = 15 341 178 777 673 149 429 167 740 440 969 249 338 310 889
and none of the usual tests would have found this out. There is a nice explana-
tion for this which we will not give here, see [BB01, Bae18], but the moral is: if
you want to be sure of something, don’t test it, prove it.
On the computer science side, analogous examples abound where errors have
been found in programs which were heavily tested. The number of such exam-
ples have recently increased with the advent of parallel computing (for instance,
in order to exploit all the cores that you have on your laptop or even your
smartphone), where bugs might be triggered by some particular and very rare
scheduling of processes. Already in the 70s, Dijkstra was claiming that program
testing can be used to show the presence of bugs, but never to show their ab-
sence! [Dij70], and the idea of formally verifying programs can even be traced
back 20 years before that by, as usual, Turing [Tur49]. If we want to have soft-
ware we can really trust (and not trust most of the time), we should move from
testing to proving in computer science too.
In this course, you will learn how to perform such proofs, as well as the
theory behind it. Actually, the most complicated program we will prove correct
here is a sorting algorithm and I can already hear you thinking “come on, we
have been writing sorting algorithms for decades, we should know how to write
one by now”. While I understand your point, I have two remarks to provide
for this. Firstly, proving a more realistic program is only a matter of time
(and experience): the course covers most of the concepts required to perform
proofs, and attacking full-fledged code will not require new techniques, only
patience. Secondly, in 2015, some researchers found out, using formal methods,
that the default sorting algorithm (the one in the standard library, not some
obscure library found on GitHub) in both Python and Java (not some obscure
programming language) was flawed, and the bug had been there for more than
a decade [dGdBB+ 19]...

0.2 Typing as proving

But how can we achieve this goal of applying techniques of proofs to programs?
It turns out that we do not even need to come up with some new ideas, thanks to
CHAPTER 0. INTRODUCTION 12

the so-called proof-as-program correspondence discovered in the 1960s by Curry

and Howard: a program is secretly the same as a proof! More precisely, in a
typed functional programming language, the type of a program can be read as
a formula, and the program itself contains exactly the information required to
prove this formula. This is the one thing to remember from this course:
PROGRAM = PROOF
This deep relationship allows the use of techniques from mathematics in order
to study programs, but also can be used to extract computational contents from
proofs in mathematics.
The goal of this course is to give precise meaning to this vague description,
but let us give an example in order to understand it better. In a functional
language such as OCaml, we can write a function such as
let comp f g x = g (f x)

and the compiler will automatically infer a type for it. Here, it will be
('a -> 'b) -> ('b -> 'c) -> ('a -> 'c)
meaning that for any types ’a, ’b and ’c,

– if f is a function which takes a value of type ’a as argument and returns

a value of type ’b,
– if g is a function which takes a value of type ’b as argument and returns
a value of type ’c, and

– if x is a value of type ’a,

then the result is of type ’c. For instance, with the function succ of type
int -> int (it adds one to an integer), and the function string_of_int of type
int -> string (it converts an integer to a string), the expression
comp succ string_of_int 2

will be of type string (it will evaluate to "3"). Now, if we read -> as a logical
implication ⇒, the type can be written as

(A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)

which is a valid formula. This is not by chance: in some sense, the program
comp can be considered as a way of proving that this formula is valid.
Of course, if we want to prove richer properties of programs (or use programs
to prove more interesting formulas), we should use a logic which is more expres-
sive than propositional logic. In this course, we will present dependent types
which achieve this, while keeping the proof-as-program correspondence. For in-
stance, the euclidean division, which computes the quotient and remainder of
two integers, is usually given the type
int -> int -> int * int
CHAPTER 0. INTRODUCTION 13

stating that it takes two integers as arguments and returns a pair of integers.
This typing is very weak, in the sense that there are many different functions
which also have this type. With dependent types, we will be able to give it the
type

(m : int) → (n : int’) → Σ(q : int).Σ(r : int).((m = nq + r) × (0 ⩽ r < |n|))

which can be read as the formula

∀m ∈ int.∀n ∈ int’.∃q ∈ int.∃r ∈ int.((m = nq + r) ∧ (0 ⩽ r < |n|))

and entirely specifies its behavior (here, int’ stands for the type of non-zero
integers, division by zero being undefined).

0.3 Checking programs

In order to help formalize proofs with the aid of a computer people have de-
veloped proof assistants such as Agda, Coq or Lean: those are programs which
help the user to gradually develop proofs (which is necessary due to their typical
size) and automatically check that they are correct. While those have progressed
much over the years, in practice, proving that a program is correct still takes
much more time than testing it (but, again, the result is infinitely superior). For
this reason, they have been used in areas where there is a strong incentive to do
it: applications where human lives (or large amounts of money) are involved.
This technology is part of a bigger family of tools and techniques called
formal methods whose aim is to guarantee the functioning of programs, with
various automation levels and expressiveness. As usual, the more precise the
invariants you are going to prove about your programs, the less automated you
can be:

abstract proof
interpretation assistants
(AbsInt, Astrée, ...) (Agda, Coq, ...)
automation expressiveness
Hoare logic
(Why3, ...)

There is quite a number of industrial successes of uses of formal methods. For

instance, the line 14 in Paris and the CDGVAL at Roissy airport have been
proved using the B-method, Airbus is heavily using various formal tools (AbsInt,
Astrée, CompCert, Frama-C), etc. We should also mention here the CompCert
project, which provides a fully certified compiler for a (subset of) C: even though
your program is proved to be bug-free, the compiler (which is not an easy piece
of software) might itself be the cause of problems in your program...
The upside of automated methods is that, of course, they allow for reaching
one’s goal much more quickly. Their downside is that when they do not apply to
a particular problem, one is left without a way out. On the other side, virtually
any property can be shown in a proof assistant, provided that one is smart
enough and has enough time to spend.
CHAPTER 0. INTRODUCTION 14

0.4 Checking proofs

Verifying that a proof is correct is a task which can be automatically and effi-
ciently performed (it amounts to checking that a program is correctly typed); in
contrast, finding a proof is an art. The situation is somewhat similar to analy-
sis in mathematics, where differentiating a function is a completely mechanical
task, while integrating requires the use of many methods and tricks [Mun19].
This means that computer science can also be of some help to mathematicians:
we can formalize mathematical proofs in proof assistants and ensure that no one
has made a mistake. And it happens that mathematicians, even famous ones,
make subtle mistakes.
For instance, in the 1990s, the Fields medalist Voevodsky wrote a paper
solving an important conjecture by Grothendieck [KV91], which roughly states
that spaces are the same as strict ∞-categories in which all morphisms are
weakly invertible (don’t worry if you do not precisely understand all the terms
in this sentence). A few years later, this was shown to be wrong because someone
provided a counter-example [Sim98], but no one could exactly point out what
was the mistake in the original proof. Because of this, Voevodsky thought
for more than 20 years (i.e. even after the counter-example was found) that
his proof was still correct. Understanding that there was indeed a mistake
lead him to use proof assistants for all his proofs and, in fact, propose a new
foundation for mathematics using logics, which is nowadays called homotopy
type theory [Uni13]. Quoting him [Voe14]:
I now do my mathematics with a proof assistant and do not have to
worry all the time about mistakes in my arguments or about how to
convince others that my arguments are correct.
But I think that the sense of urgency that pushed me to hurry with
the program remains. Sooner or later computer proof assistants will
become the norm, but the longer this process takes the more misery
associated with mistakes and with unnecessary self-verification the
practitioners of the field will have to endure.
As a much simpler example, suppose that we want to prove that all horses
have the same color (sic). We show by induction on n the property P (n) =
“every set of n horses is monochromatic”. For n = 0 and n = 1, the property is
obvious. Now suppose that P (n) holds and consider a set H of n + 1 horses. We
can figure H as a big set, in which we can pick two distinct elements (horses)
h1 and h2 and consider the sets H1 = H \ {h2 } and H2 = H \ {h1 }:

h1 h2

H1 H2

By induction hypothesis all the horses in H1 have the same color and all the
horses in H2 have the same color. Therefore, by transitivity, all the horses in H
CHAPTER 0. INTRODUCTION 15

have the same color. Of course this proof is not valid, because we all know that
there are horses of various colors (can you spot the mistake?). Formalizing the
proof in a proof assistant will force you to fill in all the details, thus removing
the possibility for potential errors in vague arguments, and will ensure that the
arguments given are actually valid, so that flaws such as in the above proof
will be uncovered. This is not limited to small proofs: large and important
proofs have been fully checked, such as the four color theorem (in Coq) in graph
theory [Gon08], the Feit-Thompson theorem (in Coq) which is central in the
classification of finite simple groups [GAA+ 13], a proof of the Kepler conjecture
on dense sphere packing (in HOL light and Isabelle) [HAB+ 17], or results from
condensed mathematics (the “liquid tensor experiment”, in Lean) [Sch22].

0.5 Searching for proofs

Closely related to proof checking is proof search, or automated theorem proving,
i.e. have the computer try by itself to find a proof for a given formula. For
simple enough fragments of logic (e.g. propositional logic) this can be done:
proof theory allows to carefully design efficient new proof search procedures. For
richer logics, it quickly becomes undecidable: it was first hoped that we could
algorithmically decide whether an arbitrary formula is provable or not, this is
Hilbert and Ackermann’s Entscheidungsproblem formulated in 1928 [HA28], but
this was shown not to be the case in 1936 independently by Church [Chu36b,
Chu36a] and Turing [Tur37a], respectively using λ-terms and Turing machines as
formalism for expressing algorithms. Still, modern proof assistants (e.g. Coq or
Lean) have so called tactics which can fill in some specific proofs, even though
the logic is rich. For example, they are able to take care of showing boring
identities such as (x + y) − x = y in abelian groups.
Understanding proof theory allows us to formulate problems in a logical fash-
ion and solve them. It thus applies to various fields, even outside theoretical
computer science. For instance, McCarthy, a founder of Artificial Intelligence
(the name is due to him!), was a strong advocate of using mathematical logic
to represent knowledge and manipulate it [McC60]. Neural networks are admit-
tedly more fashionable these days, but one never knows what the future will be
made of.
Although we will see some proof search techniques in this course, this will
not be a central subject. The reason for this is that the main message is that
we should take proofs seriously: since a proof is the same as a program, we are
not interested in provability, but rather in proofs themselves, and proof search
techniques give us very little control over the proofs they produce.

0.6 Foundations
At the beginning of the 20th century, some annoying paradoxes surfaced in
mathematics, such as Russell’s paradox, motivating Hilbert’s program to provide
an axiomatization on which all mathematics could be founded and show that
this axiomatization is consistent: this is sometimes called the foundational crisis.
Although Gödel’s incompleteness theorems established that there is no definite
answer to this question, various formalisms have been elaborated, in which one
CHAPTER 0. INTRODUCTION 16

can develop most of usual mathematics. One of the most widely used is set
theory, as axiomatized by Zermelo and Fraenkel, but other formalisms have
been proposed, such as Russell’s theory of types [WR12], where the modern
type theory originates from: in fact, type theory can be taken as a foundation
of mathematics. People usually see set theory as being more fundamental, since
we see a type as representing a set (e.g. A ⇒ B is the set of functions from
the set of A to the one of B), but we can also view type theory as being more
fundamental since we can formalize set theory in type theory. The one you take
for foundations is a matter of taste: are you more into chickens or into eggs?
Type theory also provides a solid framework in which one can study basic
philosophical questions such as: What is reasoning? What is a proof? If I know
that something exists, do I know this thing? What does it mean for two things
to be equal? and so on. We could spend pages discussing those matters (and
others have done so), but we rather like to formalize things, and we will see that
very satisfactory answers to those questions can be given with a few inference
rules. The meaning of life remains an open question, though.
By taking an increasingly important part in our lives and influencing the way
we see the (mathematical) world, these ideas even have evolved for some of us
into some sort of religion based on the computational trinitarism, which stems
from the observation that computation manifests itself in three forms [Har11]:

categories

logic programming

The aim of the present text is to explain the bottom line of the above diagram
and leave categories for other books [Mac71, LS88, Jac99]. Another closely
related religion is constructivism, a doctrine according to which something can
be accepted only if it can actually be constructed. It will play a central role in
here, because programs precisely constitute a mean to describe the construction
of things.

0.7 In this course

As a first introduction to functional and typed languages, we first present OCaml
in chapter 1, in which most example programs given here are written. We
present propositional logic in chapter 2 (the proofs), λ-calculus in chapter 3 (the
programs), and the simply-typed variant λ-calculus in chapter 4 (the programs
are the proofs). We then generalize the correspondence between proofs and
programs to richer logics: we present first-order logic in chapter 5, and, in
chapter 6, the proof assistant Agda, which is used in chapter 7 to formalize most
important results in this book, and is based on the dependent types detailed
in chapter 8. We finally give an introduction to the recent developments in
homotopy type theory in chapter 9.
CHAPTER 0. INTRODUCTION 17

0.8 Other references on programs and proofs

Although we claim some originality in the treatment and the covered topics,
this book is certainly not the first one about the subject. Excellent references
include Girard’s Proofs and Types [Gir89], Girard’s Blind Spot [Gir11], Leroy’s
College de France course Programmer = démontrer ? La correspondance de
Curry-Howard aujourd’hui, Pierce’s Types and Programming Languages [Pie02],
Sørensen and Urzyczyn’s Lectures on the Curry-Howard isomorphism [SU06],
the “HoTT book” Homotopy Type Theory: Univalent Foundations of Mathemat-
ics [Uni13], Programming Language Foundations in Agda [WK19] and Software
foundations [PdAC+ 10].

0.9 About this document

This book was first published in 2020, and the version you are currently read-
ing was compiled on December 3, 2024. Regular revisions can be expected if
mistakes are found. Should you find one, please send me a mail at the address
[email protected].

Reading on the beach. A printed copy of this course can be ordered from Ama-
zon: https://www.amazon.com/dp/B08C97TD9G/.

Color of the cover. In case you wonder, the color of the cover was chosen because
it seemed obvious to me that

program = proof = purple

Code snippets. Most of the code shown in this book is excerpted from larger files
which are regularly compiled in order to ensure their correctness. The process
of extracting snippets for inclusion into LATEX is automated with a tool whose
code is freely available at https://github.com/smimram/snippetor.

Thanks. Many people have (knowingly or not) contributed to the development

of this book. I would like to particularly express my thanks to David Baelde,
Olivier Bournez, Eric Finster, Emmanuel Haucourt, Daniel Hirschkoff, Stéphane
Lengrand, Assia Mahboubi, Paul-André Melliès, Gabriel Scherer, Pierre-Yves
Strub, Benjamin Werner.
I would also like to express my thanks to the readers of the book who
have suggested corrections and improvements: Eduardo Jorge Barbosa, Brian
Berns, Alve Björk, Aghilas Boussaa, Florian Chudigiewitsch, Adam Dingle,
Aran Donohue, Maximilian Doré, Leonid Dubinsky, Sylvain Henry, Zhicheng
Hui, Chhi’mèd Künzang, Yuxi Liu, Jeremy Roach, Kyle Stemen, Marc Sunet,
Kenton Van, Yuval Wyborski, Uma Zalakain.
 Chapter 1

Typed functional programming

1.1 Introduction
As an illustration of typed functional programming, we present here the OCaml
programming language, which was developed by Leroy and collaborators, fol-
lowing ideas from Milner [Mil78]. We present here some of the basics of the
language both because it will be used in order to provide illustrative implemen-
tations, and also because we will detail the theory behind it and generalize it in
later chapters. This is not meant to be a complete introduction to programming
in OCaml: advanced courses and documentation can be found on the website
http://ocaml.org/, as well as in books [CMP00, MMH13].
After a brief tour of the language, we present the most important construc-
tions in section 1.2, and detail recursive types, which are the main way of con-
structing types throughout the book, in section 1.3. In section 1.4, we present
the ideas behind the typing system and the guarantees it brings. Finally, we
illustrate how types can be thought of as formulas in section 1.5.

1.1.1 Hello world. The mandatory “Hello world!” program, which prints Hello
world!, can be written as follows:
(* Our first program. *)
print_endline "Hello, world!"

This illustrates the concise syntax of the language (compared to Java for in-
stance). Comments are written using (* ... *). Application of a function to
arguments does not require parenthesis. The indentation is not relevant in pro-
grams (unlike e.g. Python), but you are of course strongly encouraged to indent
your programs nicely.

1.1.2 Execution. The programs written in OCaml can be compiled to efficient

native code by using ocamlopt, but there is also a “toplevel” which allows to
interactively evaluate commands. It can be launched by typing ocaml, or utop
if you want a fancier version. For instance:
# 2 + 2;;
- : int = 4
We have typed 2 + 2, followed by ;; to indicate the end of our program. The
toplevel then indicates that this is an integer (it is of type int) and that the
result is 4. We call value an expression which cannot be reduced further: 2+2
is not a value, whereas 4 is: the execution of a program consists in reducing
expressions to values in an appropriate way (e.g. 2+2 reduces to 4).
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 19

1.1.3 A statically typed language. The OCaml language is typed, meaning

that every term has a type indicating the kind of data it is. A type can be
thought of as a particular set of values, e.g. int represents the set of integers,
string represents the set of strings, and so on. In this way, the expressions 2+2
and 4 have the type int (they are integers), and the function string_of_int
which gives the string representation of an integer has type int -> string,
meaning that it is a function which takes an integer as argument and returns a
string. Moreover, typing is statically checked: when compiling a program, the
compiler ensures that all the types match, and we use values of the expected
type. For instance, if we try to compile the program
let s = string_of_int 3.2
the compiler will complain with
Error: This expression has type float but an expression was
expected of type int
because the string_of_int function expects an integer whereas we have pro-
vided a float number as argument. This discipline is very strict in OCaml (we
sometimes say that the typing is strong): this ensures that the program will not
raise an error during execution because an unexpected value was provided to a
function (this is a theorem!). In other words, quoting Milner [Mil78]:
Well-typed programs cannot go wrong.
Moreover, the types are inferred, meaning that the user never has to specify the
types, they are guessed automatically. For instance, in the definition
let f x = x + 1
we know that the addition takes two integers as arguments and returns an
integer: therefore x must be of type int and the compiler infers that f must be
a function of type int -> int. However, if for some reason we want to specify
the types, it is still possible:
let f (x : int) : int = x + 1

1.1.4 A functional language. The language is functional, meaning that it

has good support for defining functions and manipulating them just as any
other value. For instance, suppose that we have a list l of integers, and we want
to double all its elements. We can use the List.map function from the standard
library, which is of type
('a -> 'b) -> 'a list -> 'b list
meaning that it takes as arguments a function f of type 'a -> 'b (here 'a
and 'b are intended to mean “any type”), and a list whose elements are of type
'a, and returns the list whose elements are of type 'b, obtained by applying f
to all the elements of the list. We can then define the “doubled list” by
let l2 = List.map (fun x -> 2 * x) l
where we apply the function x 7→ 2 × x to every element: note that the function
List.map takes a function as argument and that we did not even have to give
a name to the function above by using the construction fun (such a function is
sometimes called anonymous).
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 20

1.1.5 Other features. There are some other important features of the OCaml
language that we mention only briefly here, because we will not use them much.

References. As in most programming languages, OCaml has support for values

that we can modify, here called references: they can be thought of as memory
cells, from which we can retrieve the value and also change it. We can create
a reference r containing x with let r = ref x, then we can obtain its contents
with !r and change it to y with r := y. For instance, incrementing a counter
10 times is done by
let () =
let r = ref 0 in
for i = 0 to 9 do
r := !r + 1
done

Garbage collection. Unlike languages such as C, OCaml has a Garbage Collector

which takes care of allocating and freeing memory. This means that freeing
memory for a value which is not used anymore is taken care of for us. This
prevents many common bugs such as writing in a part of memory which was
freed or freeing a memory region twice by mistake.

Other traits. In addition to the functional programming style, OCaml has sup-
port for many other styles of programming including imperative (e.g. references
described above), objects, etc. OCaml also has support for records, arrays, mod-
ules, generalized algebraic data types, etc.

1.2 Basic constructions

1.2.1 Declarations. Values are declared with the let keyword. For instance,
let x = 3
declares that the variable x refers to the value 3. Note that, unless we explicitly
use the reference mechanism, these values cannot be modified. An expression
can also contain some local definitions which are only visible in the rest of the
expression. For instance, in
let x =
let y = 2 in
y * y
the definition of the variable y is only valid in the following expression y * y.
A program consists in a sequence of such definitions. In the case where a
function “does not return anything”, such as printing, by convention it returns
a value of type unit, and we often use the construction let () = ... in order
to ensure that this is the case. For instance:
let x = "hello"

let () = print_string ("The value of x is " ^ x)

CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 21

1.2.2 Functions. Functions are also defined using let definition, specifying
the arguments after the name of the variable. For instance,

let add x y = x + y
which would be of type
int -> int -> int
Note that arrows are implicitly bracketed to the right: this type means

int -> (int -> int)

Application of a function to arguments is written as the juxtaposition of the
function and the arguments, e.g.
let x = add 3 4

(no need for parenthesis). Partial application is supported, meaning that we do

not have to give all the arguments to a function (functions are sometimes called
curried). For instance, the incrementing of an integer can be defined by
let incr = add 1

The value incr thus defined is the function which takes an argument y and
returns add 1 y, so that the above definition is equivalent to
let incr y = add 1 y
This is in accordance to the bracketing of the types above: add is a function
which, when given an integer argument, returns a function of type int -> int.
As mentioned above, anonymous functions can be defined by the construc-
tion fun x -> .... The add function could thus have been equivalently defined
by
let add = fun x y -> x + y

or even
let add x = fun y -> x + y
Functions can be recursive, meaning that they can call themselves. In this case,
the rec keyword has to be used. For instance, the factorial function is defined
by

let rec fact n =

if n = 0 then 1 else n * fact (n - 1)
It is possible to define two mutually recursive functions f and g by using the
following syntax:

let rec f x = ...

and g x = ...
This means that we can use both f and g in the definitions of f and g (see
figure 1.4 below for an example).
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 22

1.2.3 Booleans. The type corresponding to booleans is bool, its two values
being true and false. The usual operators are present: conjunction &&, dis-
junction ||, and negation not. In order to test whether two values x and y
are equal or different, one can use x = y and x <> y. They can be used in
conditional branchings
if ... then ... else ...
or loops
while ... do ... done
Beware that the operators == and != also exist, but they compare values
physically, i.e. check whether they have the same memory location, not if they
have the same contents. For instance, using the toplevel, we have:
# let x = ref 0;;
val x : int ref = {contents = 0}
# let y = ref 0;;
val y : int ref = {contents = 0}
# x = x;;
- : bool = true
# x = y;;
- : bool = true
# x == x;;
- : bool = true
# x == y;;
- : bool = false

1.2.4 Products. The pair of x and y is written x,y. For instance, we can
consider the pair 3,"hello" which has the product type int * string (it is a
pair consisting of an integer and a string). Note that addition could have been
defined as
let add' (x,y) = x + y
resulting in a slightly different function than above: it now has the type
(int * int) -> int
meaning that it takes one argument, which is a pair of integers, and returns an
integer. This means that partial application is not directly available as before,
although we could still write
let incr' = fun y -> add (1,y)

1.2.5 Lists. We quite often use lists in OCaml. The empty list is [], and
x::l is the list obtained by putting the value x before a list l. Most expected
functions on lists are available in the module List. For instance,
– @ concatenates two lists,
– List.length computes the length of a list,
– List.map applies a function to all the elements of a list,
– List.iter executes a function for all the elements of a list,
– List.mem tests whether a value belongs to a list.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 23

1.2.6 Strings. Strings are written as "this is a string" and the related func-
tions can be found in the module String. For instance, the function String.length
computes the length of a string and String.sub computes a substring (at given
indices) of a string. Concatenation is obtained by ^.

1.2.7 Unit. In OCaml, the type unit contains only one element, written ().
As explained above, this is the value returned by functions which only have an
effect and return no meaningful value (e.g. printing a string). They are also
quite useful as an argument for functions which have an effect. For instance, if
we define
let f = print_string "hello"
the program will write “hello” at the beginning of the execution, because the
expression defining f is evaluated. However, if we define
let f () = print_string "hello"
nothing will be printed because we define a function taking a unit as argument.
In the course of the program, we can then use f () in order to print “hello”.

1.3 Recursive types

A very useful way of defining new data types in OCaml is by recursive types,
whose elements are constructed from other types using specific constructions,
called constructors.

1.3.1 Trees. As a first example, consider trees (more specifically, planar binary
trees with integer labels) such as

4 1

1 3

5 2

Here, a tree consists of finitely many nodes which are labeled by an integer and
can either have two children, which are themselves trees, or none (in which case
they are called leaves). This description translates immediately to the following
type definition in OCaml:
type tree =
| Node of int * tree * tree
| Leaf of int
This says that a tree is recursively characterized as being Node applied to a
triple consisting of an integer and two trees or Leaf applied to an integer. For
instance, the above tree is represented as
let t = Node (3, Node (4, Leaf 1, Node (3, Leaf 5, Leaf 2)), Leaf 1)
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 24

Here, Node and Leaf are not functions (Leaf 1 does not reduce to anything),
they are called constructors. By convention, constructor names have to begin
with a capital letter, in order to distinguish them from function names (which
have to begin with a lowercase letter).

Pattern matching. Any element of the type tree is obtained as a constructor

applied to some arguments. OCaml provides the match construction which
allows to distinguish between the various possible cases of constructors and
return a result accordingly: this is called pattern matching. For instance, the
function computing the height of a tree can be implemented as
let rec height t =
match t with
| Node (n, t1, t2) -> 1 + max (height t1) (height t2)
| Leaf n -> 0
Here, Node (n, t1, t2) is called a pattern and n, t1 and t2 are variables which
will be defined as the values corresponding to the tree we are currently matching
with, and could be given any other names. As another example, the sum of the
labels in a tree can be computed as
let rec sum t =
match t with
| Node (n, t1, t2) -> n + sum t1 + sum t2
| Leaf n -> n

It is sometimes useful to add conditions to matching cases, which can be done

using the when construction. For instance, if we wanted to match only nodes
with strictly positive labels, we could have used, in our pattern matching, a case
of the form

| Node (n, t1, t2) when n > 0 -> ...

In case where multiple cases match, the first one is chosen. OCaml tests that
all the possible values are handled in a pattern matching (and issues a warning
otherwise). Finally, one can write
let f = function ...

instead of
let f x = match x with ...
(this shortcut was introduced because it is very common to directly match on
the argument of a function).

1.3.2 Usual recursive types. It is interesting to note that many (most) usual
types can be encoded as recursive types.

Booleans. The type of booleans can be encoded as

type bool = True | False
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 25

although OCaml chose not to do that for performance reasons. A case construc-
tion

if b then e1 else e2
could then be encoded as
match b with
| True -> e1
| False -> e2

Lists. Lists are also a recursive type:

type 'a list =
| Nil
| Cons of 'a * 'a list
In OCaml, [] is a notation for Nil and x::l a notation for Cons (x, l). The
length of a list can be computed as

let rec length l =

match l with
| x::l -> 1 + length l
| [] -> 0
Note that the type of list is parametrized over a type ’a. We are thus able to
define, at once, the type of lists containing elements of type ’a, for any type ’a.

Coproducts. We have seen that the elements of a product type 'a * 'b are pairs
x , y consisting of an element x of type ’a and an element y of type ’b. We can
define coproducts consisting of an element of type ’a or an element of type ’b
by
type ('a, 'b) coprod =
| Left of 'a
| Right of 'b

An element of this type is of the form Left x with x of type ’a or Right y with
y of type ’b. For instance, we can define a function which provides the string
representation of a value which is either an integer or a float by
let to_string = function
| Left n -> string_of_int n
| Right x -> string_of_float x
which is of type (int, float) coprod -> string.

Unit. The type unit has () as the only value. It could have been defined as
type unit =
| T
having () being a notation for T.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 26

Empty type. The “empty type” can be defined as

type empty = |
i.e. a recursive type with no constructor (we still need to write | for syntactical
reasons). There is thus no values of that type.

Natural numbers. Natural numbers (in unary notation) can be defined as

type nat =
| Zero
| Suc of nat
(any natural number is either 0 or the successor of a natural number) and
addition as
let rec add m n =
match m with
| Zero -> n
| Suc m -> Suc (add m n)
Of course, it would be a bad idea to use this type for heavy computations,
and int provides access to machine binary integers (and thus natural numbers),
which are much more efficient.

1.3.3 Abstract description. As indicated before, a type can be thought of as

a set of values. We would now like to briefly sketch a mathematical definition
of the set of values corresponding to inductive types.
Suppose fixed a set U, which we can think of as the set of all possible values
an OCaml program can manipulate. We write P(U) for the powerset of U,
i.e. the set of all subsets of U, which is ordered by inclusion. Any recursive
definition induces a function F : P(U) → P(U) sending a set X to the set
obtained by applying the constructors to the elements of X. For instance, with
the definition tree of section 1.3.1, the induced function is

F (X) = {Node(n,t1 ,t2 ) | n ∈ N and t1 , t2 ∈ X} ∪ {Leaf(n) | n ∈ N}

The set associated to tree is intuitively the smallest set X ⊆ U which is closed
under adding nodes and leaves, i.e. such that F (X) = X, provided that such a
set exists. Such a set X satisfying F (X) = X is called a fixpoint of F .
In order to be able to interpret the type of trees as the smallest fixpoint of F ,
we should first show that such a fixpoint indeed exists. A crucial observation in
order to do so is the fact that the function F : P(U) → P(U) is monotone, in
the sense that, for X, Y ∈ U,

X ⊆ Y implies F (X) ⊆ F (Y ).

Theorem 1.3.3.1 (Knaster-Tarski [Kna28, Tar55]). The set

\
fix(F ) = {X ∈ P(U) | F (X) ⊆ X}

is the least fixpoint of F : we have

F (fix(F )) = fix(F )
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 27

and, for every fixpoint X of F ,

fix(F ) ⊆ X

Proof. We write C = {X ∈ P(U) | F (X) ⊆ X} for the set of prefixpoints of F .

Given X ∈ C, we have \
fix(F ) = C⊆X (1.1)
and therefore, since F is increasing,

F (fix(F )) ⊆ F (X) ⊆ X (1.2)

Since this holds for any X ∈ C, we have

\
F (fix(F )) ⊆ C = fix(F ) (1.3)

Moreover, by monotonicity again, we have

F (F (fix(F ))) ⊆ F (fix(F ))

therefore, F (fix(F )) ∈ C, and thus by (1.1)

fix(F ) ⊆ F (fix(F )) (1.4)

From (1.3) and (1.4), we deduce that fix(F ) is a fixpoint of F . An arbitrary

fixpoint X of F necessarily belongs to C and, by (1.2), we have

fix(F ) = F (fix(F )) ⊆ X

fix(F ) is thus the smallest fixpoint of F .

Remark 1.3.3.2. The attentive reader will have noticed that all we really used
in the course of the proof was the fact that P(U) is a complete semilattice,
i.e. we can compute arbitrary intersections. Under the more subtle hypothesis
of the Kleene fixpoint theorem (P(U) is a directed complete partial order and F
is Scott-continuous), one can even show that
[
fix(F ) = F n (∅)
n∈N

i.e. the fixpoint can be obtained by iterating F from the empty set. In the case
of trees,

F 0 (∅) = ∅
F 1 (∅) = {Leaf(n) | n ∈ N}
F 2 (∅) = {Leaf(n) | n ∈ N} ∪ {Nodes(n,t1 ,t2 ) | n ∈ N and t1 , t2 ∈ F 1 (∅)}

and more generally, F n (∅) is the set of trees of height strictly below n. The
theorem states that any tree is a tree of some (finite) height.
Remark 1.3.3.3. In general, there are multiple fixpoints. For instance, for the
function F corresponding to trees, the set of all “trees” where we allow to have
an infinite number of nodes is also a fixpoint of F .
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 28

As a direct corollary of theorem 1.3.3.1, we obtain the following induction prin-

ciple:
Corollary 1.3.3.4. Given a set X such that F (X) ⊆ X, we have fix(F ) ⊆ X.
Example 1.3.3.5. With the type nat of natural numbers, we have

F (X) = {Zero} ∪ {Suc(n) | n ∈ X}

We have

fix(F ) = {Sucn (Zero) | n ∈ N} = {Zero, Suc(Zero), Suc(Suc(Zero)), . . .}

In the following, we write 0 (resp. S n) instead of Zero (resp. Succ(n)), and

fix(F ) = N. The induction principle states that if X contains 0 and is closed
under successor, then it contains all natural numbers. Given a property P (n)
on natural numbers, consider the set

X = {n ∈ N | P (n)}

The requirement F (X) ⊆ X translates as P (0) holds and P (n) implies P (S n).
The induction principle is thus the classical induction principle for natural num-
bers:
P (0) ⇒ (∀n ∈ N.P (n) ⇒ P (S n)) ⇒ (∀n ∈ N.P (n))
Example 1.3.3.6. Consider the type empty. We have F (X) = ∅ and thus
fix(F ) = ∅. The induction principle states that any property is necessarily
valid on all the elements of the empty set:

∀x ∈ ∅.P (x)

Exercise 1.3.3.7. Define the function F associated to the type of lists. Show that
it also has a greatest fixpoint, distinct from the smallest fixpoint, and provide
a concrete description of it.

1.3.4 Option types and exceptions. Another quite useful recursive type
defined in the standard library is the option type
type 'a option =
| Some of 'a
| None
A value of this type is either of the form Some x for some x of type ’a or None.
It can be thought of as the type ’a extended with the default value None and
can be used for functions that, in some cases, do not return a value (in other
languages such as C or Java, one would return a NULL pointer in this case).
For instance, the function returning the head of a list is almost always defined,
except when the argument is the empty list. It thus makes sense to implement
it as the function of type 'a list -> 'a option defined by

let hd l =
match l with
| x::l -> Some x
| [] -> None
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 29

It is however quite cumbersome to use, because each time we want to use the
result of this function, we have to match it in order to decide whether the result
is None or not. For instance, in order to double the head of a list l of integers
known to be non-empty, we still have to write something like
match head l with
| Some n -> 2*n
| None -> 0 (* This case cannot happen *)

See figure 1.2 for a more representative example.

Exceptions. In order to address this, OCaml provides the mechanism of excep-

tions, which are kinds of errors that can be raised and caught. For instance, in
the standard library, the exception Not_found is defined by
exception Not_found
and the head function by
let hd l =
match l with
| x::l -> x
| [] -> raise Not_found
It now has type 'a list -> 'a, meaning that we can write

2 * (hd l)
to double the head of a list l. In the case where we take the head of the empty
list, the exception Not_found is raised. We can catch it with the following
construction if we need to:
try
...
with
| Not_found -> ...

1.4 The typing system

We have already explained in section 1.1.3 that OCaml is a strongly typed
language. We detail here some of the advantages and properties of such a
typing system.

1.4.1 Usefulness of typing. One of the main advantages of typed languages is

that typing ensures their safety: if the program passes the typechecking phase,
we are guaranteed that we will not have errors during execution caused by
unexpected data provided to a function, see section 1.4.3. But there are other
advantages too.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 30

Documentation. Knowing the type of a function is very useful for documenting

it: from the type we can generally deduce the order of the arguments of the
functions, what it is returning and so on. For instance, the function Queue.add
of the module implementing queues in OCaml has type
'a -> 'a queue -> unit
This allows us to conclude that the function takes two arguments: the first
argument must be the element we want to add and the second one the queue in
which we want to add it. Finally, the function does not return anything (to be
more precise it returns the only value of the type unit): this must mean that
the structure of queue is modified in place (otherwise, we would have had the
modified queue as return value).

Abstraction. Having a typing system is also good for abstraction: we can use a
data structure without knowing the details of implementation or even having
access to them. Taking the Queue.add function as example again, we only know
that the second argument is of type 'a queue, without any more details on
this type. This means that we cannot mess up with the internals of the data
structure, and that the implementation of queues can be radically modified
without us having to change our code.

Efficiency. Static typing can also be used to improve efficiency of compiled pro-
grams. Namely, since we know in advance the type of the values we are going to
handle, our code can be specific to the corresponding data structure, and avoid
performing some security checks. For instance, in OCaml, the concatenation
function on strings can simply put the two strings together; in contrast, in a
dynamically typed programming language such as Python, the concatenation
function on strings has first to ensure that the arguments are strings, if they are
not we will try to convert them as strings, and then we can put them together.

1.4.2 Properties of typing. There are various flavors of typing systems.

Dynamic vs static. The types of programs can either be checked during the ex-
ecution (the typing is dynamic) or during the compilation (the typing is static):
OCaml is using the latter. Static typing has many advantages: potential er-
rors are found very early, without having to perform tests, it can help to op-
timize programs, and provides very strong guarantees on the execution of the
program. The dynamic approach also has some advantages though: the code is
more flexible, the runtime can automatically perform conversions between types
if necessary, etc.

Weak vs strong. The typing system of OCaml is strong which means that it
ensures that the values in a type are actually of that type: there is no implicit
or dynamic type conversion, no NULL pointers, no explicit manipulation of
pointers, and so on. By opposition, when those requirements are not met, the
typing system is said to be weak.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 31

Decidability of typing. A basic requirement of a typing system is that we should

be able to decide whether a given term has a given type, i.e. we should have a
type checking algorithm. For OCaml (and all decent programming languages)
this is the case, and type checking is performed during each compilation of a
program.

Type inference. It is often cumbersome to have to specify the type of all the
terms (or even to give many type annotations). In OCaml, the compiler per-
forms type inference, which means that it automatically finds a type for the
program, when there is one.

Polymorphism. The types in OCaml are polymorphic, which means that they
can contain variables which are treated as universally quantified. For instance,
the identity function
let id x = x
has the type 'a -> 'a, which can also be read as the universally quantified type
∀A.A → A. This means that we can substitute ’a for any type and still get a
valid type for the identity.

Principal types. A program can admit multiple types. For instance, the identity
function admits the following types
'a -> 'a or int -> int or ('a -> 'b) -> ('a -> 'b)
and infinitely many others. The first one 'a -> 'a is however “more general”
than the others because all the other types can be obtained by substituting 'a
by some type. Such a most general type is called a principal type. The type
inference of OCaml has the property that it always produces a principal type.

1.4.3 Safety. The programs which are well-typed in OCaml are safe in the
sense that types are preserved during execution and programs do not get stuck.
In order to formalize these properties, we first need to introduce a notion of
reduction, which formalizes the way programs are executed. We will first do this
on a very small (but representative) subset of the language. Most of the concepts
used here, such as reduction or typing derivation, will be further detailed in
subsequent chapters.

A small language. We first introduce a small programming language, which can

be considered as a very restricted subset of OCaml, that we will implement in
OCaml itself. In this language, the values we use are either integers or booleans.
We define a program as being either a value, an addition (p + p’), a comparison
of integers (p < p’), or a conditional branching (if p then p’ else p”):
type prog =
| Bool of bool
| Int of int
| Add of prog * prog
| Lt of prog * prog
| If of prog * prog * prog
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 32

n1 + n2 −→ n1 + n2

p1 −→ p′1 p2 −→ p′2
p1 + p2 −→ p′1 + p2 p1 + p2 −→ p1 + p′2

n1 < n2 n1 ⩾ n2
n1 < n2 −→ true n1 < n2 −→ false

p1 −→ p′1 p2 −→ p′2
p1 < p2 −→ p′1 < p2 p1 < p2 −→ p1 < p′2

if true then p1 else p2 −→ p1 if false then p1 else p2 −→ p2

p −→ p′
if p then p1 else p2 −→ if p′ then p1 else p2

Figure 1.1: Reduction rules.

A typical program would thus be

if 3 < 2 then 5 else 1 (1.5)

which would be encoded as the term

If (Lt (Int 3 , Int 2) , Int 5 , Int 1)

Reduction. Given programs p and p′ , we write p −→ p′ when p reduces to p′ .

This reduction relation is defined as the smallest one such that, for each of
the rules listed in figure 1.1, if the relation above the horizontal bar holds, the
relation below it also holds. In these rules, we write ni for an arbitrary integer
and the first rule indicates that the formal sum of two integers reduces to their
sum (e.g. 3 + 2 −→ 5).
An implementation of the reduction in OCaml is given in figure 1.2: given a
program p, the function red either returns Some p′ if there exists a program p′
with p −→ p′ or None otherwise. Note that the reduction is not deterministic,
i.e. a program can reduce to distinct programs:

5 + (5 + 4) ←− (3 + 2) + (5 + 4) −→ (3 + 2) + 9

The implementation provided in figure 1.2 chooses a particular reduction when

there are multiple possibilities: we say that it implements a reduction strategy.
A program is irreducible when it does not reduce to another program. It can
be remarked that
– values are irreducible,
– there are irreducible programs which are not values, e.g. 3 + true.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 33

(** Perform one reduction step. *)

let rec red : prog -> prog option = function
| Bool _ | Int _ -> None
| Add (Int n1 , Int n2) -> Some (Int (n1 + n2))
| Add (p1 , p2) ->
(
match red p1 with
| Some p1' -> Some (Add (p1' , p2))
| None ->
match red p2 with
| Some p2' -> Some (Add (p1 , p2'))
| None -> None
)
| Lt (Int n1 , Int n2) -> Some (Bool (n1 < n2))
| Lt (p1 , p2) ->
(
match red p1 with
| Some p1' -> Some (Lt (p1' , p2))
| None ->
match red p2 with
| Some p2' -> Some (Lt (p1 , p2'))
| None -> None
)
| If (Bool true , p1 , p2) -> Some p1
| If (Bool false , p1 , p2) -> Some p2
| If (p , p1 , p2) ->
match red p with
| Some p' -> Some (If (p' , p1 , p2))
| None -> None

Figure 1.2: Implementation of reduction.

CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 34

n∈N
⊢ true : bool ⊢ false : bool ⊢ n : int

⊢ p1 : int ⊢ p2 : int ⊢ p1 : int ⊢ p2 : int

⊢ p1 + p2 : int ⊢ p1 < p2 : bool

⊢ p : bool ⊢ p1 : A ⊢ p2 : A
⊢ if p then p1 else p2 : A

Figure 1.3: Typing rules.

In the second case, the reason why the program 3 + true cannot be further
reduced is that an unexpected value was provided to the sum: we were hoping
for an integer instead of the value true. We will see that the typing system
precisely prevents such situations from arising.

Typing. A type in our language is either an integer (int) or a boolean (bool),

which can be represented by the type
type t = TInt | TBool
We write ⊢ p : A to indicate that the program p has the type A and call it a
typing judgment. This relation is defined inductively by the rules of figure 1.3.
This means that a program p has type A when ⊢ p : A can be derived using the
above rules. For instance, the program (1.5) has type int:

⊢ 3 : int ⊢ 2 : int
⊢ 3 < 2 : bool ⊢ 5 : int ⊢ 1 : int
⊢ if 3 < 2 then 5 else 1 : int
Such a tree showing that a typing judgment is derivable is called a derivation
tree. The principle of type checking and type inference algorithms of OCaml
is to try to construct such a derivation of a typing judgment, using the above
rules. In our small toy language, this is quite easy and is presented in figure 1.4.
For a language with much more features as OCaml (where we have functions
and polymorphism, not to mention objects or generalized algebraic data types)
this is much more subtle, but still follows the same general principle.
It can be observed that a term can have at most one type. We can thus
speak of the type of a typable program:
Theorem 1.4.3.1 (Uniqueness of types). Given a program p, if p is both of
types A and A′ then A = A′ .
Proof. By induction on p: depending on the form of p, at most one rule applies.
For instance, if p is of the form if p0 then p1 else p2 , the only rule which
allows typing p is
⊢ p0 : bool ⊢ p1 : A ⊢ p2 : A
⊢ if p0 then p1 else p2 : A
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 35

exception Type_error

(** Infer the type of a program. *)

let rec infer = function
| Bool _ -> TBool
| Int _ -> TInt
| Add (p1 , p2) ->
check p1 TInt;
check p2 TInt;
TInt
| Lt (p1 , p2) ->
check p1 TInt;
check p2 TInt;
TBool
| If (p , p1 , p2) ->
check p TBool;
let t = infer p1 in
check p2 t;
t

(** Check that a program has a given type. *)

and check p t =
if infer p <> t then raise Type_error

Figure 1.4: Type inference and type checking.

CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 36

Since p1 and p2 admit at most one type A by induction hypothesis, p also does.
Other cases are similar.
As explained in section 1.4.2, full-fledged languages such as OCaml do not gen-
erally satisfy such a strong property. The type of a program is not generally
unique, but in good typing systems there exists instead a type which is “the
most general”.

Safety. We are now ready to formally state the safety properties guaranteed for
typed programs. The first one, called subject reduction, states that the reduction
preserves typing:
Theorem 1.4.3.2 (Subject reduction). Given programs p and p′ such that p −→ p′ ,
if p has type A then p′ also has type A.
Proof. By hypothesis, we have both a derivation of p −→ p′ and ⊢ p : A. We
reason by induction on the former. For instance, suppose that the last rule is

p1 −→ p′1
p1 + p2 −→ p′1 + p2

The derivation of ⊢ p : A necessarily ends with

⊢ p1 : int ⊢ p2 : int
⊢ p1 + p2 : int

In particular, we have ⊢ p1 : int and thus, by induction hypothesis, ⊢ p′1 : int

is derivable. We conclude using the derivation

⊢ p′1 : int ⊢ p2 : int

⊢ p′1 + p2 : int

Other cases are similar.

The second important property is called progress, and states that the program
either is a value or reduces.
Theorem 1.4.3.3 (Progress). Given a program p of type A, either p is a value or
there exists a program p′ such that p −→ p′ .
Proof. By induction on the derivation of ⊢ p : A. For instance, suppose that
the last rule is
⊢ p1 : int ⊢ p2 : int
⊢ p1 + p2 : int
By induction hypothesis, the following cases can happen:
– p1 −→ p′1 : in this case, we have p1 + p2 −→ p′1 + p2 ,
– p2 −→ p′2 : in this case, we have p1 + p2 −→ p1 + p′2 ,
– p1 and p2 are values: in this case, they are necessarily integers and p1 + p2
reduces to their sum.
Other cases are similar.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 37

The safety property finally states that typable programs never encounter errors,
in the sense that their execution is never stuck: for instance, we will never try
to evaluate a program such as 3 + true during the reduction.
Theorem 1.4.3.4 (Safety). A program p of type A is safe: either
– p reduces to a value v in finitely many steps

p −→ p1 −→ p2 −→ · · · −→ pn −→ v

– or p loops: there is an infinite sequence of reductions

p −→ p1 −→ p2 −→ · · ·

Proof. Consider a maximal sequence of reductions from p. If this sequence is

finite, by maximality, its last element p′ is an irreducible program. Since p is of
type A and reduces to p′ , by the subject reduction theorem 1.4.3.2 p′ also has
type A. We can thus apply the progress theorem 1.4.3.3 and deduce that either
p′ is a value or there exists p′′ such that p′ −→ p′′ . The second case is impossible
since it would contradict the maximality of the sequence of reductions.
Of course, in our small language, a program cannot give rise to an infinite
sequence of reductions, but the formulation and proof of the previous theorem
will generalize to languages in which this is not the case. The previous properties
of subject reduction and progress are entirely formalized in section 7.1.

Limitations of typing. The typing systems (such as the one described above or
the one of OCaml) reject legit programs such as
(if true then 3 else false) + 1
which reduces to a value. Namely, the system imposes the requirement that the
two branches of a conditional branching should have the same type, which is
not the case here, even though we know that only the first branch will be taken,
because the condition is the constant boolean true. We thus ensure that typable
programs are safe, but not that all safe programs are typable. In fact, this has
to be this way since an easy reduction from the halting problem shows that the
safety of programs is undecidable as soon as the language is rich enough.
Also, the typing system does not prevent all errors from occurring during
the execution, such as dividing by zero or accessing an array out of its bounds.
This is because the typing system is not expressive enough. For instance, the
function
let f x = 1 / (x - 2)
should intuitively be given the type

{n : int | n ̸= 2} → int

which states this function is correct as long as its input is an integer different
from 2, but this is of course not a valid type in OCaml. We will see in chapters 6
and 8 that some languages do allow such rich typing, at the cost of losing type
inference (but type checking is still decidable).
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 38

1.5 Typing as proving

We would now like to give the intuition for the main idea of this course, that
programs correspond to proofs. Understanding in details this correspondence
will allow us to design very rich typing systems which allow to formally prove
fine theorems and reason about programs.

1.5.1 Arrow as implication. As a first illustration of this, we will see here

that simple types (such as the ones used in OCaml) can be read as propositional
formulas. The translation is simply a matter of slightly changing the way we
read types: a type variable ’a can be read as a propositional variable A and the
arrow -> can be read as an implication ⇒. Now, we can observe that there is a
program of a given type (in a reasonable subset of OCaml, see below) precisely
when the corresponding formula is true (for a reasonable notion of true formula).
For instance, we expect that the formula

A⇒A corresponding to the type ’a -> ’a

is provable. And indeed, there is a program of this type, the identity:

let id : 'a -> 'a = fun x -> x
We have specified here the type of this function for clarity. We can give many
other such examples. For instance, A ⇒ B ⇒ A is proved by
let k : 'a -> 'b -> 'a = fun x y -> x
The formula (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C) can be proved by the composi-
tion

let comp : ('a -> 'b) -> ('b -> 'c) -> ('a -> 'c) =
fun f g x -> g (f x)
The formula (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ (A ⇒ C) is proved by
let s : ('a -> 'b -> 'c) -> ('a -> 'b) -> ('a -> 'c) =
fun f g x -> f x (g x)
and so on.
Remark 1.5.1.1. In general, there is not a unique proof of a given formula. For
instance, A ⇒ A can also be proved by

fun x -> k x 3
where k is the function defined above.

1.5.2 Other connectives. For now, the fragment of the logic we have is very
poor (we only have implication as connective), but other usual connectives also
have counterparts in types.
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 39

Conjunction. A conjunction proposition A ∧ B means that both A and B hold.

In terms of types, the counterpart is a product:

A∧B corresponds to ’a * ’b

and we have programs implementing usual propositions such as A ∧ B ⇒ A:

let proj1 : ('a * 'b) -> 'a = fun (a , b) -> a
or the commutativity of conjunction A ∧ B ⇒ B ∧ A:

let comm : ('a * 'b) -> ('b * 'a) = fun (a , b) -> b , a

Truth. The formula ⊤ corresponding to truth is always provable and we expect

that there is exactly one reason for which it should be true. Thus

⊤ corresponds to unit

and we can prove A ⇒ ⊤:

let unit_intro : 'a -> unit = fun x -> ()

Falsity. The formula ⊥ corresponds to falsity and we do not expect that it can
be proved (because false is never true). We can make it correspond to the empty
type, which can be defined as a type with no constructor:
type empty = |
The formula ⊥ ⇒ A is then shown by
let empty_elim : empty -> 'a = fun x -> match x with _ -> .

(the “.” is a “refutation case” meaning that the compiler should ensure that
this case should never happen, it is almost never used in OCaml unless you are
doing tricky stuff such as the above).

Negation. The negation can then be defined as usual by ¬A being a notation

for A ⇒ ⊥, and we can prove the reasoning by contraposition

(A ⇒ B) ⇒ (¬B ⇒ ¬A)

by
let contr : ('a -> 'b) -> (('b -> empty) -> ('a -> empty)) =
fun f g a -> g (f a)
or A ⇒ ¬¬A by

let nni : 'a -> (('a -> empty) -> empty) = fun a f -> f a
CHAPTER 1. TYPED FUNCTIONAL PROGRAMMING 40

Disjunction. A disjunction formula A ∨ B can be thought of as being either A

or B. We can implement it as a coproduct type, which is an inductive type
where a value is either a value of type ’a or a value of type ’b, see section 1.3.2:
type ('a , 'b) coprod = Left of 'a | Right of 'b
We can then prove the formula A ∨ B ⇒ B ∨ A, stating that disjunction is
commutative, by
let comm : ('a , 'b) coprod -> ('b , 'a) coprod = fun x ->
match x with
| Left a -> Right a
| Right b -> Left b
or the distributivity A ∧ (B ∨ C) ⇒ (A ∧ B) ∨ (A ∧ C) of conjunction over
disjunction by
let dist : ('a * ('b , 'c) coprod) -> ('a * 'b , 'a * 'c) coprod =
fun (a , x) ->
match x with
| Left b -> Left (a , b)
| Right c -> Right (a , c)
or the de Morgan formula (¬A ∨ B) ⇒ (A ⇒ B) by
let de_Morgan : ('a -> empty, 'b) coprod -> ('a -> 'b) = fun x a ->
match x with
| Left f -> empty_elim (f a)
| Right b -> b

1.5.3 Limitations of the correspondence. This correspondence has some

limitations due to the fact that OCaml is, after all, a language designed to do
programming, not logic. It is easy to prove formulas which are not true if we
use “advanced” features of the language such as exceptions. For instance, the
following “proves” A ⇒ B:
let absurd : 'a -> 'b = fun x -> raise Not_found
More annoying counter-examples come from functions which are not terminating
(i.e. looping). For instance, we can also “prove” A ⇒ B by
let rec absurd : 'a -> 'b = fun x -> absurd x
Note that, in particular, both allow to “prove” ⊥:
let fake : empty = absurd ()
Finally, we can notice that there does not seem to be any reasonable way to
implement the classical formula ¬A ∨ A (apart from using the above tricks),
which would correspond to a program of the type
('a -> empty , 'a) coprod
In next chapters, we will see that it is indeed possible to design languages in
which a formula is provable precisely when there is a program of the corre-
sponding type. Such languages do not have functions with “side-effects” (such
as raising an exception) and enforce that all the programs are terminating.
 Chapter 2

Propositional logic

In this chapter, we present propositional logic: this is the fragment of logic

consisting of propositions (very roughly, something which can either be true or
false) joined by connectives. We will see various ways of formalizing the proofs
in propositional logic – with a particular focus on natural deduction – and study
the properties of those. We begin with the formalism of natural deduction in
section 2.2, show that it enjoys the cut elimination property in section 2.3 and
discuss strategies for searching for proofs in section 2.4. The classical variant
of logic is presented in section 2.5. We then present two alternative logical
formalisms: sequent calculus (section 2.6) and Hilbert calculus (section 2.7).
Finally, we introduce Kripke semantics in section 2.8, which can be considered
as an intuitionistic counterpart of boolean models for classical logic.

2.1 Introduction
2.1.1 From provability to proofs. Most of you are acquainted with boolean
logic based on the booleans, which we write here as 0 for false, and 1 for true.
In this setting, every propositional formula can be interpreted as a boolean,
provided that we have an interpretation for the variables. The truth tables for
usual connectives are
A∧B 0 1 A∨B 0 1 A⇒B 0 1
0 0 0 0 0 1 0 1 1
1 0 1 1 1 1 1 0 1
For instance, we know that the formula A ⇒ A is valid because, for whichever
interpretation of A as a boolean, the induced interpretation of the formula is 1.
We have this idea that propositions should correspond to types. Therefore,
rather than booleans, propositions should be interpreted as sets of values and
implications as functions between the corresponding values. For instance, if
we write N for a proposition interpreted as the set of natural numbers, the
type N ⇒ N would correspond to the set of functions from natural numbers to
themselves. We now see that the boolean interpretation is very weak: it only
cares about whether sets are empty or not. For instance, depending on whether
X is empty (∅) or non-empty (¬∅), the following table indicates whether the set
X → X of functions from X to X is empty or not:
A→B ∅ ¬∅
∅ ¬∅ ¬∅
¬∅ ∅ ¬∅

Reading ∅ as “false” and ¬∅ as “true”, we see that we recover the usual truth
table for implication. In this sense, the fact that the formula N ⇒ N is true only
shows that there exists such a function, but in fact there are many such func-
tions, and we would be able to reason about the various functions themselves.
CHAPTER 2. PROPOSITIONAL LOGIC 42

Actually, the interpretation of implications as sets of functions is still not

entirely satisfactory because, given a function of type N → N, there are many
ways to implement it. We could have programs of different complexities, using
their arguments in different ways, and so on. For instance, the constant function
x 7→ 0 can be implemented as
let f x = 0
or
let f x = x - x
or
let rec f x = if x = 0 then x else f (x - 1)
respectively in constant, logarithmic and linear complexity (if we assume the
predecessor to be computed in constant time). We thus want to shift from
an extensional perspective, where two functions are equal when they have the
same values on the same inputs, to an intentional one where the way the re-
sult is computed matters. This means that we should be serious about what
is a program, or equivalently a proof, and define it precisely so that we can
reason about the proofs of a proposition instead of its provability: we want to
know what the proofs are and not only whether there exist one or not. This
is the reason why Girard advocates that there are three levels for interpreting
proofs [Gir11, section 7.1]:
0. the boolean level: propositions are interpreted as booleans and we are
interested in whether a proposition is provable or not,
1. the extensional level: propositions are interpreted as sets and we are in-
terested in which functions can be implemented,
2. the intentional level: we are interested in the proofs themselves (and how
they evolve via cut elimination).

2.1.2 Intuitionism. This shift from provability to proofs was started by the
philosophical position of Brouwer starting in the early twentieth century, called
intuitionism. According to this point of view, mathematics does not consist
in discovering the properties of a preexisting objective reality, but is rather a
mental subjective construction, which is independent of the reality and has an
existence on its own, whose validity follows from the intuition of the mathe-
matician. From this point of view
– the conjunction A ∧ B of two propositions should be seen as having both
a proof of A and a proof of B: if we interpret propositions as sets, A ∧ B
should not be interpreted as the intersection A ∩ B, but rather are the
product A × B,
– a disjunction A∨B should be interpreted as having a proof of A or a proof
of B, i.e. it does not correspond to the union A ∪ B, but rather to the
disjoint union A ⊔ B,
– an implication A ⇒ B should be interpreted as having a way to construct
a proof of B from a proof of A,
CHAPTER 2. PROPOSITIONAL LOGIC 43

– a negation ¬A = A ⇒ ⊥ should be interpreted as having a counter-

example to A, i.e. a way to produce an absurdity from a proof of A.
Interestingly, this led Brouwer to reject principles which are classically valid.
For instance, according to this point of view ¬¬A should not be considered as
equivalent to A because the implication

¬¬A ⇒ A

should not hold: if we can show that there is no counter-example to A, this

does not mean that we actually have a proof of A. For instance, suppose that
I cannot find my key inside my apartment and my door is locked: I must have
locked my door so that I know that my key is somewhere in the apartment and
it is not lost, but I still cannot find it. Not having lost my key (i.e. not not
having my key) does not mean that I have my key; in other words,

¬¬Key ⇒ Key

does not hold (explanation borrowed from Ingo Blechschmidt). For similar
reasons, Brouwer also rejected the excluded middle

¬A ∨ A

given an arbitrary proposition A: in order to have a proof for it, we should

have a way, whichever the proposition A is, to produce a counter-example to it
or a proof of it. Logic rejecting these principles is called intuitionistic and, by
opposition, we speak of classical logic when they are admitted.

2.1.3 Formalizing proofs. Our goal is to give a precise definition of what a

proof is. This will be done by formalizing the rules using which we usually
construct our reasoning. For instance, suppose that we want to prove that the
function x 7→ 2 × x is continuous in 0: we have to prove the formula

∀ε.(ε > 0 ⇒ ∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε))

This is done in the following steps, resulting in the following transformed for-
mulas to be proved.
– Suppose given ε, we have to show:

ε > 0 ⇒ ∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε)

– Suppose that ε > 0 holds, we have to show:

∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε)

– Take η = ε/2, we have to show:

ε/2 > 0 ∧ ∀x.|x| < ε/2 ⇒ |2x| < ε

– We have to show both

ε/2 > 0 and ∀x.|x| < ε/2 ⇒ |2x| < ε

CHAPTER 2. PROPOSITIONAL LOGIC 44

– For ε/2 > 0:

– because 2 > 0, this amounts to showing (ε/2) × 2 > 0 × 2,
– which, by usual identities, amounts to showing ε > 0,
– which is an hypothesis.
– For ∀x.|x| < ε/2 ⇒ |2x| < ε:
– suppose given x, we have to show: |x| < ε/2 ⇒ |2x| < ε,
– suppose that |x| < ε/2 holds, we have to show: |2x| < ε,
– since 2 > 0, this amounts to showing: |2x|/2 < ε/2,
– which, by usual identities, amounts to showing: |x| < ε/2,
– which is an hypothesis.

Now that we have decomposed the proof into very small steps, it seems possible
to give a list of all the generic rules that we are allowed to apply in a reasoning.
We will do so and will introduce a convenient formalism and notations, so that
the above proof will be written as:

ε > 0, |x| < ε/2 ⊢ |x| < ε/2

ε > 0, |x| < ε/2 ⊢ |2x|/2 < ε/2
ε>0⊢ε>0 ε > 0, |x| < ε/2 ⊢ |2x| < ε
ε > 0 ⊢ (ε/2) × 2 > 0 × 2 ε > 0 ⊢ |x| < ε/2 ⇒ |2x| < ε
ε > 0 ⊢ ε/2 > 0 ε > 0 ⊢ ∀x.|x| < ε/2 ⇒ |2x| < ε
ε > 0 ⊢ ε/2 > 0 ∧ ∀x.|x| < ε/2 ⇒ |2x| < ε
ε > 0 ⊢ ∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε)
⊢ ε > 0 ⇒ ∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε)
⊢ ∀ε.(ε > 0 ⇒ ∃η.(η > 0 ∧ ∀x.|x| < η ⇒ |2x| < ε))

(when read from bottom to top, you should be able to see the precise corre-
spondence with the previous description of the proof).

2.1.4 Properties of the logical system. Once we have formalized our log-
ical system we should do some sanity checks. The first requirement is that it
should be consistent: there is at least one formula A which is not provable (oth-
erwise, the system would be entirely pointless). The second requirement is that
typechecking should be decidable: there should be an algorithm which checks
whether a proof is valid or not. In contrast, the question of whether a formula
is provable or not will not be decidable in general and we do not expect to have
an algorithm for that.

2.2 Natural deduction

Natural deduction is the first formalism for proofs that we will study. It was
introduced by Gentzen [Gen35]. We first present the intuitionistic version.
CHAPTER 2. PROPOSITIONAL LOGIC 45

2.2.1 Formulas. We suppose fixed a countably infinite set X of propositional

variables. The set A of formulas or propositions is generated by the following
grammar
A, B ::= X | A ⇒ B | A ∧ B | ⊤ | A ∨ B | ⊥ | ¬A
where X is a propositional variable (in X ) and A and B are propositions. They
are respectively read as a propositional variable, implication, conjunction, truth,
disjunction, falsity and negation. By convention, ¬ binds the most tightly, then
∧, then ∨, then ⇒:
¬A ∨ B ∧ C ⇒ D reads as ((¬A) ∨ (B ∧ C)) ⇒ D
Moreover, all binary connectives are implicitly bracketed to the right:
A1 ∧ A2 ∧ A3 ⇒ B ⇒ C reads as (A1 ∧ (A2 ∧ A3 )) ⇒ (B ⇒ C)
This is particularly important for ⇒, for the connectives ∧ and ∨ the other
convention could be chosen with almost no impact. We sometimes write A ⇔ B
for (A ⇒ B) ∧ (B ⇒ A).
A subformula of a formula A is a formula occurring in A. The set of subfor-
mulas of A can formally be defined by induction on A by
Sub(X) = {X} Sub(A ⇒ B) = {A ⇒ B} ∪ Sub(A) ∪ Sub(B)
Sub(⊤) = {⊤} Sub(A ∧ B) = {A ∧ B} ∪ Sub(A) ∪ Sub(B)
Sub(⊥) = {⊥} Sub(A ∨ B) = {A ∨ B} ∪ Sub(A) ∪ Sub(B)
Sub(¬A) = {¬A} ∪ Sub(A)

2.2.2 Sequents. A context

Γ = A1 , . . . , A n
is a list of propositions. A sequent, or judgment, is a pair
Γ⊢A
consisting of a context Γ and a variable A. Such a sequent should be read as
“under the hypothesis in Γ, I can prove A” or “supposing that I can prove the
propositions in Γ, I can prove A”. The comma in a context can thus be read
as a “meta” conjunction (the logical conjunction being ∧) and the sign ⊢ as a
“meta” implication (the logical implication being ⇒).
Remark 2.2.2.1. The notation derives from Frege’s Begriffsschrift [Fre79], an
axiomatization of first-order logic based on a graphical notation, in which logical
connectives are drawn by using wires of particular shapes: the formulas ¬A,
A ⇒ B and ∀x.A are respectively drawn as
A A x A
B
In this system, given a proposition drawn A , the notation A means
that A is provable. The assertion that (∀x.A) ⇒ (∃x.B) is provable would for
instance be written
x A
x B
(in classical logic, the formula ∃x.B is equivalent to ¬∀x.¬B). The symbol ⊢
used in sequents, as well as the symbol ¬ for negation, originate from there.
CHAPTER 2. PROPOSITIONAL LOGIC 46

(ax)
Γ, A, Γ0 ` A

Γ`A⇒B Γ`A Γ, A ` B
(⇒E ) (⇒I )
Γ`B Γ`A⇒B

Γ`A∧B l Γ`A∧B r Γ`A Γ`B

(∧E ) (∧E ) (∧I )
Γ`A Γ`B Γ`A∧B

(>I )
Γ`>

Γ`A∨B Γ, A ` C Γ, B ` C Γ`A Γ`B

(∨E ) (∨l ) (∨r )
Γ`C Γ`A∨B I Γ`A∨B I

Γ`⊥
(⊥E )
Γ`A

Γ ` ¬A Γ`A Γ, A ` ⊥
(¬E ) (¬I )
Γ`⊥ Γ ` ¬A

Figure 2.1: NJ: rules of intuitionistic natural deduction.

2.2.3 Inference rules. An inference rule, written

Γ 1 ⊢ A1 ... Γn ⊢ An
(2.1)
Γ⊢A

consists of n sequents Γi ⊢ Ai , called the premises of the rule, and a sequent

Γ ⊢ A, called the conclusion of the rule. We sometimes identify the rules by a
name given to them, which is written on the right of the rule. Some rules also
come with external hypothesis on the formulas occurring in the premises: those
are called side conditions. There are two ways to read an inference rule:
– the deductive way, from top to bottom: from a proof for each of the
premises Γi ⊢ Ai we can deduce Γ ⊢ A,
– the inductive or proof search way, from bottom to top: if we want to prove
Γ ⊢ A by that inference rule we need to prove all the premises Γi ⊢ Ai .
Both are valid ways of thinking about proofs, but one might be more natural
than the other one depending on the application.

2.2.4 Intuitionistic natural deduction. The rules for intuitionistic natural

deductions are shown in figure 2.1, the resulting system often being called NJ (N
for natural deduction and J for intuitionistic). Apart from the axiom rule (ax),
each rule is specific to a connective and the rules can be classified in two fam-
ilies depending on whether this connective appears in the conclusion or in the
premises:
CHAPTER 2. PROPOSITIONAL LOGIC 47

– the elimination rules allow the use of a formula with a given connec-
tive (which is in the formula in the leftmost premise, called the principal
premise),
– the introduction rules construct a formula with a given connective.
In figure 2.1, the elimination (resp. introduction) rules are displayed on the left
(resp. right) and bear names of the form (. . .E ) (resp. (. . .I )).
The axiom rule allows the use of a formula in the context Γ: supposing that
a formula A holds, we can certainly prove it. This rule is the only one to really
make use of the context: when read from the bottom to top, all the other rules
either propagate the context or add hypothesis to it, but never inspect it.
The introduction rules are the most easy to understand: they allow proving
a formula with a given logical connective from the proofs of the immediate
subformulas. For instance, (∧I ) states that from a proof of A and a proof of B,
we can construct a proof of A ∧ B. Similarly, the rule (⇒I ) follows the usual
reasoning principle for implication: if, after supposing that A holds, we can
show B, then A ⇒ B holds.
In contrast, the elimination rules allow the use of a connective. For instance,
the rule (⇒E ), which is traditionally called modus ponens or detachment rule,
says that if A implies B and A holds then certainly B must hold. The rule
(∨E ) is more subtle and corresponds to a case analysis: if we can prove A ∨ B
then, intuitively, we can prove A or we can prove B. If in both cases we can
deduce C then C must hold. The elimination rule (⊥E ) is sometimes called ex
falso quodlibet or the explosion principle: it states that if we can prove false
then the whole logic collapses, and we can prove anything.
We can notice that there is no elimination rule for ⊤ (knowing that ⊤ is
true does not bring any new information), and no introduction rule for ⊥ (we
do not expect that there is a way to prove falsity). There are two elimination
rules for ∧ which are respectively called left and right rules, and similarly there
are two introduction rules for ∨.

2.2.5 Proofs. The set of proofs (or derivations) is the smallest set such that
given proofs πi of the sequent Γi ⊢ Ai , for 1 ⩽ i ⩽ n, and an inference rule of
the form (2.1), there is a proof of Γ ⊢ A, often written in the form of a tree as

π1 πn
...
Γ 1 ⊢ A1 Γ n ⊢ An
Γ⊢A

A sequent Γ ⊢ A is provable (or derivable) when it is the conclusion of a proof.

A formula A is provable when it is provable without hypothesis, i.e. when the
sequent ⊢ A is provable.
Example 2.2.5.1. The formula (A∧B) ⇒ (A∨B) is provable (for any formulas A
and B):
(ax)
A∧B ⊢A∧B
(∧E )
A∧B ⊢A
(∨lI )
A∧B ⊢A∨B
(⇒I )
⊢A∧B ⇒A∨B
CHAPTER 2. PROPOSITIONAL LOGIC 48

Example 2.2.5.2. The formula (A ∨ B) ⇒ (B ∨ A) is provable:

(ax) (ax)
A ∨ B, A ` A A ∨ B, B ` B
(ax) (∨rI ) (∨lI )
A∨B `A∨B A ∨ B, A ` B ∨ A A ∨ B, B ` B ∨ A
(∨E )
A∨B `B∨A
(⇒I )
`A∨B ⇒B∨A

Example 2.2.5.3. The formula A ⇒ ¬¬A is provable:

(ax) (ax)
A, ¬A ⊢ ¬A A, ¬A ⊢ A
(¬E )
A, ¬A ⊢ ⊥
(¬I )
A ⊢ ¬¬A
(⇒I )
⊢ A ⇒ ¬¬A

Example 2.2.5.4. The formula (A ⇒ B) ⇒ (¬B ⇒ ¬A) is provable:

(ax) (ax)
A ⇒ B, ¬B, A ` A ⇒ B A ⇒ B, ¬B, A ` A
(ax) (⇒E )
A ⇒ B, ¬B, A ` ¬B A ⇒ B, ¬B, A ` B
(¬E )
A ⇒ B, ¬B, A ` ⊥
(¬I )
A ⇒ B, ¬B ` ¬A
(⇒I )
A ⇒ B ` ¬B ⇒ ¬A
(⇒I )
` (A ⇒ B) ⇒ ¬B ⇒ ¬A

Example 2.2.5.5. The formula (¬A ∨ B) ⇒ (A ⇒ B) is provable:

(ax) (ax)
¬A ∨ B, A, ¬A ⊢ ¬A ¬A ∨ B, A, ¬A ⊢ A
(¬E )
¬A ∨ B, A, ¬A ⊢ ⊥
(ax) (⊥E ) (ax)
¬A ∨ B, A ⊢ ¬A ∨ B ¬A ∨ B, A, ¬A ⊢ B ¬A ∨ B, A, B ⊢ B
(∨E )
¬A ∨ B, A ⊢ B
(⇒I )
¬A ∨ B ⊢ A ⇒ B
(⇒I )
⊢ (¬A ∨ B) ⇒ (A ⇒ B)

Other typical provable formulas are

– ∧ and ⊤ satisfy the axioms of idempotent commutative monoids:

(A ∧ B) ∧ C ⇔ A ∧ (B ∧ C) A∧B ⇔B∧A
⊤∧A⇔A⇔A∧⊤ A∧A⇔A

– ∨ and ⊥ satisfy the axioms of idempotent commutative monoids

– ∧ distributes over ∨ and conversely:

A ∧ (B ∨ C) ⇔ (A ∧ B) ∨ (A ∧ C)
A ∨ (B ∧ C) ⇔ (A ∨ B) ∧ (A ∨ C)

– ⇒ is reflexive and transitive

A⇒A (A ⇒ B) ⇒ (B ⇒ C) ⇒ (A ⇒ C)
CHAPTER 2. PROPOSITIONAL LOGIC 49

– currying:
((A ∧ B) ⇒ C) ⇔ (A ⇒ (B ⇒ C))

– usual reasoning structures with latin names, such as

(A ⇒ B) ⇒ (¬B ⇒ ¬A) (modus tollens)

(A ∨ B) ⇒ (¬A ⇒ B) (modus tollendo ponens)
¬(A ∧ B) ⇒ (A ⇒ ¬B) (modus ponendo tollens)

Reasoning on proofs. In this formalism, the proofs are defined inductively and
therefore we can reason by induction on them, which is often useful. Precisely,
the induction principle on proofs is the following one:
Theorem 2.2.5.6 (Induction on proofs). Suppose given a predicate P (π) on
proofs π. Suppose moreover that for every rule of figure 2.1 and every proof π
ending with this rule

π1 πn
...
Γ 1 ⊢ A1 Γn ⊢ An
π =
Γ⊢A

if P (πi ) holds for every index i, with 1 ⩽ i ⩽ n, then P (π) also holds. Then
P (π) holds for every proof π.

2.2.6 Fragments. A fragment of intuitionistic logic is a system obtained by

restricting to formulas containing only certain connectives and the rules con-
cerning these connectives. By convention, the axiom rule (ax) is present in
every fragment. For instance, the implicational fragment of intuitionistic logic
is obtained by restricting to implication: formulas are generated by the grammar

A, B ::= X | A ⇒ B

and the rules are

Γ⊢A⇒B Γ⊢A Γ, A ⊢ B
′ (ax) (⇒E ) (⇒I )
Γ, A, Γ ⊢ A Γ⊢B Γ⊢A⇒B

The cartesian fragment is obtained by restricting to product and implication.

Another useful fragment is minimal logic obtained by considering formulas with-
out ⊥, and thus removing the rule (⊥E ).

2.2.7 Admissible rules. A rule is admissible when, whenever the premises are
provable, the conclusion is also provable. An important point here is that the
way the proof of the conclusion is constructed might depend on the proofs of the
premises, and not only on the fact that we know that the premises are provable.

Structural rules. We begin by showing that the structural rules are admissible.
Those rules are named in this way because they concern the structure of the
logical proofs, as opposed to the particular connectives we are considering for
formulas. They express some resource management possibilities for the hypothe-
ses in sequents: we can permute, merge and weaken them, see section 2.2.10.
CHAPTER 2. PROPOSITIONAL LOGIC 50

A first admissible rule is the weakening rule, which states that whenever
one can prove a formula with some hypotheses, we can still prove it with more
hypotheses. The proof with more hypotheses is “weaker” in the sense that it
apply in less cases (since more hypotheses have to be satisfied).
Proposition 2.2.7.1 (Weakening). The weakening rule
Γ, Γ′ ⊢ B
(wk)
Γ, A, Γ′ ⊢ B
is admissible.
Proof. By induction on the proof of the hypothesis Γ, Γ′ ⊢ B.
– If the proof is of the form
(ax)
Γ, Γ′ ⊢ B
with B occurring in Γ or Γ′ , then we conclude with
(ax)
Γ, A, Γ′ ⊢ B

– If the proof is of the form

π1 π2
Γ, Γ′ ⊢ B ⇒ C Γ, Γ′ ⊢ B
(⇒E )
Γ, Γ′ ⊢ C
then we conclude with
π1′ π2′
Γ, A, Γ′ ⊢ B ⇒ C Γ, A, Γ′ ⊢ B
′ (⇒E )
Γ, A, Γ ⊢ C
where π1′ and π2′ are respectively obtained from π1 and π2 by induction
hypothesis:
π1 π2
′
Γ, Γ ⊢ B ⇒ C Γ, Γ′ ⊢ B
π1′ = (wk) π2′ = (wk)
Γ, A, Γ′ ⊢ B ⇒ C Γ, A, Γ′ ⊢ B

– If the proof is of the from

π
′
Γ, Γ , B ⊢ C
(⇒I )
Γ, Γ′ ⊢ B ⇒ C
then we conclude with
π′
Γ, A, Γ′ , B ⊢ C
(⇒I )
Γ, A, Γ′ ⊢ B ⇒ C
where π ′ is obtained from π by induction hypothesis.
CHAPTER 2. PROPOSITIONAL LOGIC 51

– Other cases are similar.

Also admissible is the exchange rule, which states that we can reorder hypothesis
in the contexts:
Proposition 2.2.7.2 (Exchange). The exchange rule

Γ, A, B, Γ′ ⊢ C
(xch)
Γ, B, A, Γ′ ⊢ C

is admissible.
Proof. By induction on the proof of the hypothesis Γ, A, B, Γ′ ⊢ C.
Given a proof π of some sequent, we often write w(π) for a proof obtained by
weakening. Another admissible rule is contraction, which states that if we can
prove a formula with two occurrences of a hypothesis, we can also prove it with
one occurrence.
Proposition 2.2.7.3 (Contraction). The contraction rule

Γ, A, A, Γ′ ⊢ B
(contr)
Γ, A, Γ′ ⊢ B

is admissible.
Proof. By induction on the proof of the hypothesis Γ, A, A, Γ′ ⊢ B.
We can also formalize the fact that knowing ⊤ does not bring information, what
we call here truth strengthening (we are not aware of a standard terminology
for this one):
Proposition 2.2.7.4 (Truth strengthening). The following rule is admissible:

Γ, ⊤, Γ′ ⊢ A
(tstr)
Γ, Γ′ ⊢ A

Proof. By induction on the proof of the hypothesis Γ, ⊤, Γ′ ⊢ A, the only “sub-

tle” case being that we have to transform
(ax) (⊤I )
Γ, ⊤, Γ′ ⊢ ⊤ into Γ, Γ′ ⊢ ⊤

Alternatively, the admissibility of the rule can also be deduced from the admis-
sibility of the cut rule (see theorem 2.2.7.5 below).

The cut rule. A most important admissible rule is the cut rule, which states
that if we can prove a formula B using a hypothesis A (thought of as a lemma
used in the proof) and we can prove the hypothesis A, then we can directly
prove the formula B.
Theorem 2.2.7.5 (Cut). The cut rule

Γ⊢A Γ, A, Γ′ ⊢ B
(cut)
Γ, Γ′ ⊢ B

is admissible.
CHAPTER 2. PROPOSITIONAL LOGIC 52

Proof. For simplicity, we restrict ourselves to the case where the context Γ′
is empty, which is not an important limitation because the exchange rule is
admissible. The cut rule can be derived from the rules of implication by
Γ, A ⊢ B
(⇒I )
Γ⊢A Γ⊢A⇒B
(⇒E )
Γ⊢B
We will see in section 2.3.2 that the above proof is not satisfactory and will
provide another one, which brings much more information about the dynamics
of the proofs.

Admissible rules via implication. Many rules can be proved to be admissible by

eliminating provable implications:
Lemma 2.2.7.6. Suppose that the formula A ⇒ B is provable. Then the rule
Γ⊢A
Γ⊢B
is admissible.
Proof. We have
..
.
⊢A⇒B
(wk)
Γ⊢A Γ⊢A⇒B
(⇒E )
Γ⊢B
For instance, we have seen in theorem 2.2.5.4 that the implication
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
is provable. We immediately deduce:
Lemma 2.2.7.7 (Modus tollens). The following two variants of the modus tollens
rule
Γ⊢A⇒B Γ⊢A⇒B Γ ⊢ ¬B
Γ ⊢ ¬B ⇒ ¬A Γ ⊢ ¬A
are admissible.

2.2.8 Definable connectives. A logical connective is definable when it can be

expressed from other connectives in such a way that replacing the connective by
its expression and removing the associated logical rules preserves provability.
Lemma 2.2.8.1. Negation is definable as ¬A = A ⇒ ⊥.
Proof. The introduction and elimination rules of ¬ are derivable by
Γ, A ⊢ ⊥ Γ, A ⊢ ⊥
(¬I ) ⇝ (⇒I )
Γ ⊢ ¬A Γ⊢A⇒⊥
Γ ⊢ ¬A Γ⊢A Γ⊢A⇒⊥ Γ⊢A
(¬E ) ⇝ (⇒E )
Γ⊢⊥ Γ⊢⊥
CHAPTER 2. PROPOSITIONAL LOGIC 53

from which it follows that, given a provable formula A, the formula A′ ob-
tained from A by changing all connectives ¬− into − ⇒ ⊥ is provable, without
using (¬E ) and (¬I ). Conversely, suppose given a formula A, such that the
transformed formula A′ is provable. We have to show that A is also provable,
which is more subtle. In the proof of A′ , for each subproof of the form

π
Γ⊢B⇒⊥

where the conclusion B ⇒ ⊥ corresponds to the presence of ¬B as a subformula

of A, we can transform the proof as follows:

π
Γ⊢B⇒⊥
(wk) (ax)
Γ, B ⊢ B ⇒ ⊥ Γ, B ⊢ B
(⇒E )
Γ, B ⊢ ⊥
(¬I )
Γ ⊢ ¬B

Applying this transformation enough times, we can transform the proof of A′

into a proof of A. A variant of this proof is given in theorem 2.2.9.2.
Lemma 2.2.8.2. Truth is definable as A ⇒ A, for any provable formula A not
involving ⊤. For instance: ⊤ = (⊥ ⇒ ⊥).
Remark 2.2.8.3. In intuitionistic logic, contrarily to what we expect from the
usual de Morgan formulas, the implication is not definable as

A ⇒ B = ¬A ∨ B

see sections 2.3.5 and 2.5.1.

2.2.9 Equivalence. We could have added to the syntax of our formulas an

equivalence connective ⇔ with associated rules

Γ⊢A⇔B Γ⊢A⇔B Γ⊢A⇒B Γ⊢B⇒A

(⇔lE ) (⇔rE ) (⇔I )
Γ⊢A⇒B Γ⊢B⇒A Γ⊢A⇔B

It would have been definable as

A ⇔ B = (A ⇒ B) ∧ (B ⇒ A)

Two formulas A and B are equivalent when A ⇔ B is provable. This notion of

equivalence relates in the expected way to provability:
Lemma 2.2.9.1. If A and B are equivalent then, for every context Γ, Γ ⊢ A is
provable if and only if Γ ⊢ B is provable.

Proof. Immediate application of theorem 2.2.7.6.

In this way, we can give a variant of the proof of theorem 2.2.8.1:
Corollary 2.2.9.2. Negation is definable as ¬A = (A ⇒ ⊥).
CHAPTER 2. PROPOSITIONAL LOGIC 54

Proof. We have ¬A ⇔ (A ⇒ ⊥):

(ax) (ax) (ax) (ax)
¬A, A ` ¬A ¬A, A ` A A ⇒ ⊥, A ` A ⇒ ⊥ A ⇒ ⊥, A ` A
(¬E ) (⇒E )
¬A, A ` ⊥ A ⇒ ⊥, A ` ⊥
(⇒I ) (¬I )
¬A ` A ⇒ ⊥ A ⇒ ⊥ ` ¬A
(⇒I ) (⇒I )
` ¬A ⇒ A ⇒ ⊥ ` (A ⇒ ⊥) ⇒ ¬A
(⇔E )
` ¬A ⇔ (A ⇒ ⊥)

and we conclude using theorem 2.2.9.1.

2.2.10 Structural rules. The rules of exchange, contraction, weakening and

truth strengthening are often called structural rules:
Γ, A, B, Γ′ ⊢ C Γ, A, A, Γ′ ⊢ B
(xch) (contr)
Γ, B, A, Γ′ ⊢ C Γ, A, Γ′ ⊢ B

Γ, Γ′ ⊢ B Γ, ⊤, Γ′ ⊢ A
(wk) (tstr)
Γ, A, Γ′ ⊢ B Γ, Γ′ ⊢ A
We have seen in section 2.2.7 that they are admissible in our system.

Contexts as sets. The rules of exchange and contraction allow to think of con-
texts as sets (rather than lists) of formulas, because a set is a list “up to permu-
tation and duplication of its elements”. More precisely, given a set A, we write
P(A) for the set of subsets of A, and A∗ for the set of lists of elements of A.
We define an equivalence relation ∼ on A∗ as the smallest equivalence relation
such that
Γ, A, B, ∆ ∼ Γ, B, A, ∆ Γ, A, A, ∆ ∼ Γ, A, ∆
Lemma 2.2.10.1. The function f : A∗ → P(A) which to a list associates its set
of elements is surjective. Moreover, given Γ, ∆ ∈ A∗ , we have f (Γ) = f (∆) if
and only if Γ ∼ ∆.
We could therefore have directly defined contexts to be sets of formulas, as is
sometimes done, but this would be really unsatisfactory. Namely, a formula A
in a context can be thought of as some kind of hypothesis which is to be proved
by an auxiliary lemma and we might have twice the same formula A, but proved
by different means: in this case, we would like to be able to refer to a particular
instance of A (which is proved in a particular way), and we cannot do this
if we have a set of hypothesis. For instance, there are intuitively two proofs
of A ⇒ A ⇒ A: the one which uses the left A to prove A and the one which
uses the right one (this will become even more striking with the Curry-Howard
correspondence, see theorem 4.1.7.2). However, with contexts as sets, both are
the same:
(ax)
A⊢A
(⇒I )
A⊢A⇒A
(⇒I )
⊢A⇒A⇒A
A less harmful simplification which is sometimes done is to quotient by exchange
only (and not contraction), in which case the contexts become multisets, see
section A.3.5. We will refrain from doing that here as well.
CHAPTER 2. PROPOSITIONAL LOGIC 55

Variants of the proof system. The structural rules are usually taken as “real”
(as opposed to admissible) rules of the proof system. Here, we have carefully
chosen the formulation of rules, so that they are admissible, but it would not
hold anymore if we had used subtle variants instead. For instance, if we replace
the axiom rule by

(ax) or (ax)
Γ, A ⊢ A A⊢A

or replace the introduction rule for conjunction by

Γ⊢A ∆⊢B
(∧I )
Γ, ∆ ⊢ A ∧ B

the structural rules are not all admissible anymore. The study of the fine struc-
ture behind this lead Girard to introduce linear logic [Gir87].

2.2.11 Substitution. Given formulas A and B and a variable X, we write

A[B/X]

for the substitution of X by B in A, i.e. the formula A where all the occurrences
of X have been replaced by B. More generally, a substitution for A is a function
which to every variable X occurring in A assigns a formula σ(X), and we also
write
A[σ]
for the formula A where every variable X has been replaced by σ(X). Similarly,
given a context Γ = A1 , . . . , An , we define

Γ[σ] = A1 [σ], . . . , An [σ]

We often write
[A1 /X1 , . . . , An /Xn ]
for the substitution σ such that σ(Xi ) = Ai and σ(X) = X for X different from
each Xi . It satisfies

A[A1 /X1 , . . . , An /Xn ] = A[A1 /X1 ] . . . [An /Xn ]

We always suppose that, for a substitution σ, the set

{X ∈ X | σ(X) ̸= X}

is finite so that the substitution can be represented as the list of images of

elements of this set. Provable formulas are closed under substitution:
Proposition 2.2.11.1. Given a provable sequent Γ ⊢ A and a substitution σ, the
sequent Γ[σ] ⊢ A[σ] is also provable.
Proof. By induction on the proof of Γ ⊢ A.
CHAPTER 2. PROPOSITIONAL LOGIC 56

2.3 Cut elimination

In mathematics, one often uses lemmas to show results. For instance, suppose
that we want to show that 6 admits a half, i.e. there exists a number n such
that n + n = 6. We could proceed in this way by observing that
– every even number admits a half, and
– 6 is even.
In this proof, we have used a lemma (even numbers can be halved) that we have
supposed to be already proved. Of course, there was another, much shorter,
proof of the fact that 6 admits a half: simply observe that 3 + 3 = 6. We should
be able to extract the second proof (giving directly 3 as a half) from the first
one, by looking in details at the proof of the lemma: this process of extracting
a direct proof from a proof using a lemma is called cut elimination. We will
see that is has a number of applications and will allow us to take a “dynamic”
point of view on proofs: removing cuts corresponds to “executing” proofs.
Let us illustrate how this process works in more details on the above example.
We first need to make precise the notions we are using here, see section 6.6.3
for a full formalization. We say that a number m is a half of a number n when
m + m = n, and the set of even numbers is defined here to be the smallest set
containing 0 and such that n + 2 is even when n is. Moreover, our lemma is
proved in this way:
Lemma 2.3.0.1. Every even number admits a half.
Proof. Suppose given an even number n. By definition of evenness, it can be of
the two following forms and we can reason by induction.
– If n = 0 then it admits 0 as half, since 0 + 0 = 0.
– If n = n′ + 2 with n′ even, then by induction n′ admits a half m,
i.e. m + m = n′ , and therefore n admits m + 1 as half since
n = n′ + 2 = (m + m) + 2 = (m + 1) + (m + 1)

In our reasoning to prove that 6 can be halved, we have used the fact that 6 is
even, which we must have proved in this way:
– 6 is even because 6 = 4 + 2 and 4 is even, where
– 4 is even because 4 = 2 + 2 and 2 is even, where
– 2 is even because 2 = 0 + 2 and 0 is even, where
– 0 is even by definition.
From the proof of the lemma, we know that the half of 6 is the successor of the
half of 4, which is the successor of the half of 2 which is the successor of the half
of 0, which is 0. Writing, as usual, n/2 for a half of n, we have
6/2 = (4/2) + 1 = (2/2) + 1 + 1 = (0/2) + 1 + 1 + 1 = 0 + 1 + 1 + 1 = 3
Therefore the half of 6 is 3: we have managed to extract the actual value of the
half of 6 from the proofs the 6 is even and the above lemma. This example is
further formalized in section 6.6.3.
CHAPTER 2. PROPOSITIONAL LOGIC 57

2.3.1 Cuts. In logic, the use of a lemma to show a result is called a “cut”. This
must not be confused with the (cut) rule presented in theorem 2.2.7.5, although
they are closely related. Formally, a cut in a proof is an elimination rule whose
principal premise is proved by an introduction rule of the same connective. For
instance, the following are cuts:

π π′ π
Γ⊢A Γ⊢B Γ, A ⊢ B π′
(∧I ) (⇒I )
Γ⊢A∧B Γ⊢A⇒B Γ⊢A
(∧lE ) (⇒E )
Γ⊢A Γ⊢B

The formula in the principal premise is called the cut formula: above, the cut
formulas are respectively A∧B and A ⇒ B. A proof containing a cut intuitively
does “useless work”. Namely, the one on the left starts from a proof π of A in
the context Γ, which it uses to prove A ∧ B, from which it deduces A: in order
to prove A, the proof π was already enough and the proof π ′ of B was entirely
superfluous. Similarly, for the proof on the right, we show in π that supposing A
we can prove B, and also in π ′ that we can prove A: we could certainly directly
prove B, replacing in π all the places where the hypothesis A is used (say by an
axiom) by the proof π ′ . For this reason, cuts are sometimes also called detours.
From a proof-theoretic point of view, it might seem a bit strange that some-
one would use such a kind of proof structure, but this is actually common in
mathematics: when we want to prove a result, we often prove a lemma which
is more general than the result we want to show and then deduce the result we
were aiming at. One of the reasons for proceeding in this way is that we can
use the same lemma to cover multiple cases, and thus have shorter proofs (not
to mention that they are generally more conceptual and modular, since we can
reuse the lemmas for other proofs). We will see that, however, we can always
avoid using cuts in order to prove formulas. Before doing so, we first need to
introduce the main technical result which allows this.

2.3.2 Proof substitution. A different kind of substitution than the one of

section 2.2.11 consists in replacing some axioms in a proof by another proof.
For instance, consider two proofs

(ax) (ax)
Γ, A ⊢ A Γ, A ⊢ A
(∧I ) ..
Γ, A, B ⊢ A ∧ A ′ .
π= (⇒I ) π =
Γ, A ⊢ B ⇒ A ∧ A Γ⊢A

The proof π ′ allows to deduce A from the hypothesis in Γ. Therefore, in the

proof π, each time the hypothesis A of the context is used (by an axiom rule),
we can instead use the proof π ′ and reprove A. Doing so, the hypothesis A
in the context becomes superfluous and we can remove it. The proof resulting
from this transformation is thus obtained by “re-proving” A each time we need
CHAPTER 2. PROPOSITIONAL LOGIC 58

it instead of having it as an hypothesis:

π′ π′
Γ⊢A Γ⊢A
(wk) (wk)
Γ, B ⊢ A Γ, B ⊢ A
(∧I )
Γ, B ⊢ A ∧ A
(⇒I )
Γ⊢B ⇒A∧A

This process generalizes as follows:

Proposition 2.3.2.1. Given provable sequents

π π′
and
Γ, A, Γ′ ⊢ B Γ⊢A

the sequent Γ, Γ′ ⊢ B is also provable, by a proof that we write as π[π ′ /A]:

π[π ′ /A]
Γ, Γ′ ⊢ B

In other words, the (cut) rule

Γ⊢A Γ, A, Γ′ ⊢ B
(cut)
Γ, Γ′ ⊢ B

is admissible.
Proof. By induction on π.
We will see that the admissibility of this rule is the main ingredient to prove
cut elimination, thus its name.

2.3.3 Cut elimination. A logic has the cut elimination property when when-
ever a formula is provable then it is also provable with a proof which does not
involve cuts: we can always avoid doing unnecessary things. This procedure was
introduced by Gentzen under the name Hauptsatz [Gen35]. In general, we not
only want to know that such a proof exists, but also to have an effective cut elim-
ination procedure which transforms a proof into one without cuts. The reason
for this is that we will see in section 4.1.8 that this corresponds to “executing”
the proof (or the program corresponding to it): this is why Girard [Gir87] claims
that
A logic without cut elimination is like a car without an engine.
Although the proof obtained after eliminating cuts is “simpler” in the sense that
it does not contain unnecessary steps (cuts), it cannot always be considered as
“better”: it is generally much bigger than the original one. The quote above
explains it: think of a program computing the factorial of 1000. We see that a
result can be much bigger than the program computing it [Boo84], and it can
take much time to compute [Ore82].
Theorem 2.3.3.1. Intuitionistic natural deduction has the cut elimination prop-
erty.
CHAPTER 2. PROPOSITIONAL LOGIC 59

π
Γ, A ` B π0
(⇒I )
Γ`A⇒B Γ`A π[π 0 /A]
(⇒E )
Γ`B Γ`B

π π0
Γ`A Γ`B
(∧I )
Γ`A∧B π
(∧lE )
Γ`A Γ`A

π π0
Γ`A Γ`B
(∧I )
Γ`A∧B π0
(∧rE )
Γ`B Γ`B

π
Γ`A π0 π 00
(∨lI )
Γ`A∨B Γ, A ` C Γ, B ` C π 0 [π/A]
(∨E )
Γ`C Γ`C

π
Γ`B π0 π 00
(∨rI )
Γ`A∨B Γ, A ` C Γ, B ` C π 00 [π/B]
(∨E )
Γ`C Γ`C

Figure 2.2: Transforming proofs in NJ in order to eliminate cuts.

Proof. Suppose given a proof which contains a cut. This means that at some
point in the proof we encounter one of the following situations (i.e. we have a
subproof of one of the following forms), in which case we transform the proof
as indicated by ⇝ in figure 2.2 (we do not handle the cut on ¬ since ¬A can be
coded as A ⇒ ⊥). For instance,
(ax) (ax)
Γ, A ⊢ A Γ, A ⊢ A
(∧I )
Γ, A ⊢ A ∧ A π
(⇒I )
Γ⊢A⇒A∧A Γ⊢A
(⇒E )
Γ⊢A∧A

is transformed into
π π
Γ⊢A Γ⊢A
(∧I )
Γ⊢A∧A
We iterate the process on the resulting proof until all the cuts have been re-
CHAPTER 2. PROPOSITIONAL LOGIC 60

moved.
As it can be noticed on the above example, applying the transformation ⇝
might duplicate cuts: if the above proof π contained cuts, then the transformed
proof contains twice the cuts of π. It is therefore not clear that the process
actually terminates, whichever order we choose to eliminate cuts. We will see
in section 4.2 that it indeed does, but the proof will be quite involved. It
is sufficient for now to show that a particular strategy for eliminating cuts is
terminating: at each step, we suppose that we eliminate a cut of highest depth,
i.e. there is no cut “closer to the axioms” (for instance, we could apply the above
transformation only if π has not cuts). We define the size |A| of a formula A as
its number of connectives and variables:

|X| = |⊤| = |⊥| = 1 |A ⇒ B| = |A ∧ B| = |A ∨ B| = 1 + |A| + |B|

The degree of a cut is the size of the cut formula (e.g. of A ⇒ A ∧ A in the above
example, whose size is 2 + 3|A|), and the degree of a proof is then defined as the
multiset (see section A.3.5) of the degrees of the cuts it contains. It can then
be checked that whenever we apply ⇝, the newly created cuts are of strictly
lower degree than the cut we eliminated and therefore the degree of the proof
decreases according to the multiset order, see section A.3.5. For instance, if we
apply a transformation
π
Γ, A ⊢ B π′
(⇒I )
Γ⊢A⇒B Γ⊢A π[π ′ /A]
(⇒E ) ⇝
Γ⊢B Γ⊢B

we suppose that π ′ has no cuts (otherwise the eliminated cut would not be
of highest depth). The degree of the cut is |A ⇒ B|. All the cuts present
in the resulting proof where already present in the original proof, except for
the new cuts on A which might be created by the substitution of π ′ in π,
which are of degree |A| < |A ⇒ B|. Since the multiset order is well-founded,
see theorem A.3.5.1, the process will eventually come to an end: we cannot have
an infinite sequence of ⇝ transformations, chosen according to our strategy.
The previous theorem states that, as long as we are interested in provability,
we can restrict ourselves to cut-free proofs. This is of interest because we often
have a good idea of which rules can be used in those. In particular, we have the
following useful result:
Proposition 2.3.3.2. For any formula A, a cut-free proof of ⊢ A necessarily ends
with an introduction rule.
Proof. Consider the a cut-free proof π of ⊢ A. We reason by induction on it.
This proof cannot be an axiom because the context is empty. Suppose that π
ends with an elimination rule:
..
.
π= (?E )
⊢A
For each of the elimination rules, we observe that the principal premise is nec-
essarily of the form ⊢ A′ , and therefore ends with an introduction rule, by
CHAPTER 2. PROPOSITIONAL LOGIC 61

induction hypothesis. The proof is then of the form

..
.
(?I )
⊢ A′ ...
(?E )
⊢A

and thus contains a cut, which is impossible since we have supposed π to be cut-
free. Since π cannot end with an axiom nor an elimination rule, it necessarily
ends with an introduction rule.
In the above proposition, it is crucial that we consider a formula in an empty
context: a cut-free proof of Γ ⊢ A does not necessarily end with an introduction
rule if Γ is arbitrary.

2.3.4 Consistency. The least one can expect from a non-trivial logical system
is that not every formula is provable, otherwise the system is of no use. A logical
system is consistent when there is at least one formula which cannot be proved
in the system. Since, by (⊥E ), one can deduce any formula from ⊥, we have:
Lemma 2.3.4.1. The following are equivalent:
(i) the logical system is consistent,
(ii) the formula ⊥ cannot be proved,

(iii) the principle of non-contradiction holds: there is no formula A such that

both A and ¬A can be proved.
Theorem 2.3.4.2. The system NJ is consistent.
Proof. Suppose that it is inconsistent, i.e. by theorem 2.3.4.1 that it can prove ⊢ ⊥.
By theorem 2.3.3.1, there is a cut-free proof of ⊢ ⊥ and, by theorem 2.3.3.2,
this proof necessarily ends with an introduction rule. However, there is no
introduction rule for ⊥, contradiction.
Remark 2.3.4.3. As a side note, we would like to point out that if we naively
allowed proofs to be infinite or cyclic (i.e. contain themselves as subproofs), then
the system would not be consistent anymore. For instance, we could prove ⊥
by
(ax)
⊥⊢⊥ π
(⇒I )
⊢⊥⇒⊥ ⊢⊥
π = (⇒E )
⊢⊥
(this proof is infinite in the sense that we should replace π by the proof it-
self above). Also, for such a proof, the cut elimination procedure would not
terminate...
CHAPTER 2. PROPOSITIONAL LOGIC 62

2.3.5 Intuitionism. We have explained in the introduction that the intuition-

istic point of view on proofs is that they should be “accessible to intuition” or
“constructive”. This entails in particular that a proof of a disjunction A ∨ B
should imply that one of the two formulas A or B is provable: we not only know
that the disjunction is true, but we can explicitly say which one of A or B is
true. This property is satisfied by the system NJ we have defined above, and
this explains why we have said that it is intuitionistic:
Proposition 2.3.5.1. If a formula A ∨ B is provable in NJ then either A or B is
provable.
Proof. Suppose that we have a proof of A ∨ B. By theorem 2.3.3.1, we can
suppose that this proof is cut-free and thus ends with an introduction rule by
theorem 2.3.3.2. The proof is thus of one of the following two forms
π π
⊢A ⊢B
(∨l ) (∨r )
⊢A∨B I ⊢A∨B I
which means that we either have a proof of A or a proof of B.
While quite satisfactory, this property means that truth in our logical sys-
tems behaves differently from the usual systems (e.g. validity in boolean models),
which are called classical by contrast. Every formula provable in NJ is true in
classical systems, but the converse is not true. One of the most striking example
is the so-called principle of excluded middle stating that, for any formula A, the
formula
¬A ∨ A
should hold. While this is certainly classically true, this cannot be proved
intuitionistically for a general formula A:
Lemma 2.3.5.2. Given a propositional variable X, the formula ¬X ∨ X cannot
be proved in NJ.
Proof. Suppose that it is provable. By theorem 2.3.5.1, either ¬X or X is
provable and by theorem 2.3.3.1 and theorem 2.3.3.2, we can assume that this
proof is cut-free and ends with an introduction rule. Clearly, ⊢ X is not provable
(because there is no corresponding introduction rule), so that we must have a
cut-free proof of the form
π
X⊢⊥
(¬I )
⊢ ¬X
By theorem 2.2.11.1, if we had such a proof, we would in particular have one
where X is replaced by ⊤:
π′
⊤⊢⊥
but, by theorem 2.2.7.4, we could remove ⊤ from the hypothesis and obtain a
proof
π ′′
⊢⊥
which is impossible by the consistency of NJ, see theorem 2.3.4.2.
CHAPTER 2. PROPOSITIONAL LOGIC 63

Of course, the above theorem does not state that, for a particular given
formula A, the formula ¬A ∨ A is not provable. For instance, with A = ⊤, we
have
(⊤I )
⊢⊤
(∨rI )
⊢ ¬⊤ ∨ ⊤
It however states that we cannot prove ¬A ∨ A without knowing the details
of A. This will be studied in more detail in section 2.5, where other examples
of non-provable formulas are given.
Since the excluded-middle is not provable, maybe it is false in our logic? That
is not the case because we can show that the excluded-middle is not falsifiable
either, since we can prove the formula ¬¬(¬A ∨ A) as follows:

(ax)
¬(¬A ∨ A), A ` A
(ax) (∨rI )
¬(¬A ∨ A), A ` ¬(¬A ∨ A) ¬(¬A ∨ A), A ` ¬A ∨ A
(¬E )
¬(¬A ∨ A), A ` ⊥
(¬I )
¬(¬A ∨ A) ` ¬A
(ax) (∨lI )
¬(¬A ∨ A) ` ¬(¬A ∨ A) ¬(¬A ∨ A) ` ¬A ∨ A
(¬E )
¬(¬A ∨ A) ` ⊥
(¬I )
` ¬¬(¬A ∨ A)

This proof will be analyzed in more details in section 2.5.2.

A variant of the above lemma which is sometimes useful is the following one:
Lemma 2.3.5.3. Given a propositional variable X, the formula ¬X ∨¬¬X cannot
be proved in NJ.

Proof. Let us prove this in a slightly different way than in theorem 2.3.5.2. It
can be proved in NJ that ¬⊤ ⇒ ⊥:
(ax) (⊤I )
¬⊤ ⊢ ¬⊤ ¬⊤ ⊢ ⊤
(¬E )
¬⊤ ⊢ ⊥
(⇒I )
⊢ ¬⊤ ⇒ ⊥

and that ¬¬⊥ ⇒ ⊥:

(ax)
¬¬⊥, ⊥ ⊢ ⊥
(ax) (¬I )
¬¬⊥ ⊢ ¬¬⊥ ¬¬⊥ ⊢ ¬⊥
(¬E )
¬¬⊥ ⊢ ⊥
(⇒I )
⊢ ¬¬⊥ ⇒ ⊥

Now, suppose that we have a proof of ¬X ∨ ¬¬X. By theorem 2.3.5.1, either

¬X or ¬¬X is provable. By theorem 2.2.11.1, either ¬⊤ or ¬¬⊥ is provable.
In both cases, by (⇒E ), using the above proof, ⊥ is provable, which we know is
not the case by consistency, see theorem 2.3.4.2

2.3.6 Commutative cuts. Are the cuts the only situations where one is doing
useless work in proofs? No. It turns out that falsity and disjunction induce some
CHAPTER 2. PROPOSITIONAL LOGIC 64

Γ⊢⊥
(⊥E ) ...
Γ⊢A Γ⊢⊥
(?E ) ⇝ (⊥E )
Γ⊢B Γ⊢B

π π′ π ′′
Γ⊢A∨B Γ, A ⊢ C Γ, B ⊢ C
(∨E ) ...
Γ⊢C
(?E )
Γ⊢D

⇝
π′ π ′′
... ...
π Γ, A ⊢ C Γ, B ⊢ C
(?E ) (?E )
Γ⊢A∨B Γ, A ⊢ D Γ, B ⊢ D
(∨E )
Γ⊢D

Figure 2.3: Elimination of commutative cuts.

more situations where we would like to eliminate “useless work”. For instance,
consider the following proof:
(ax)
⊥⊢⊥
(⊥E ) (ax) (ax)
⊥⊢A∨A ⊥, A ⊢ A ⊥, A ⊢ A
(∨E )
⊥⊢A

For the hypothesis ⊥, we deduce the “general” statement that A ∨ A holds, from
which we deduce that A holds. Clearly, we ought to be able to simplify this
proof by into
(ax)
⊥⊢⊥
(⊥E )
⊥⊢A
where we directly prove A instead of using the “lemma” A∨A as an intermediate
step. Another example of such a situation is the following one:
(ax) (ax) (ax) (ax)
A, B ∨ C, B ` A A, B ∨ C, B ` A A, B ∨ C, C ` A A, B ∨ C, C ` A
(ax) (∧I ) (∧I )
A, B ∨ C ` B ∨ C A, B ∨ C, B ` A ∧ A A, B ∨ C, C ` A ∧ A
(∨E )
A, B ∨ C ` A ∧ A
(∧lE )
A, B ∨ C ` A

Here, in a context containing A, we prove A ∧ A, from which we deduce A,

whereas we could have directly proved A instead. This is almost a typical
cut situation between the rule (∧I ) and (∧lE ), except that we cannot eliminate
the cut because the two rules are separated by the intermediate rule (∨E ). In
order for the system to have nice properties, we should thus add to the usual
cut-elimination rules the rules of figure 2.3, where (?E ) stands for an arbitrary
elimination rule. Those rules eliminate what we call commutative cuts, see
[Gir89, section 10.3].
CHAPTER 2. PROPOSITIONAL LOGIC 65

2.4 Proof search

An important question is whether there is an automated procedure in order to
perform proof-search in NJ, i.e. answer the question:
Is a given sequent Γ ⊢ A provable?
In general, the answer is yes, but the complexity is hard. In order to do so,
the basic idea of course consists in trying to construct a proof derivation whose
conclusion is our sequent, from bottom up.

2.4.1 Reversible rules. A rule is reversible when, if its conclusion is provable,

then its hypothesis are provable. Such rules are particularly convenient in order
to search for proofs since we know that we can always apply them: if the
conclusion sequent was provable then the hypothesis still are. For instance, the
rule
Γ⊢A
(∨lI )
Γ⊢A∨B
is not reversible: if, while searching for a proof of Γ ⊢ A ∨ B, we apply it,
we might have to backtrack in the case where Γ ⊢ A is not provable, since
maybe Γ ⊢ B was provable instead, the most extreme example being
..
.
⊢⊥
(∨lI )
⊢⊥∨⊤
where we have picked the wrong branch of the disjunction and try to prove ⊥,
whereas ⊤ was directly provable. On the contrary, the rule
Γ⊢A Γ⊢B
(∧I )
Γ⊢A∧B
is reversible: during proof search, we can apply it without regretting our choice.
Proposition 2.4.1.1. In NJ, the reversible rules are (ax), (⇒I ), (∧I ), (⊤I ) and
(¬I ).
Proof. Consider the case of (⇒I ), the other cases being similar. In order to
show that this rule (recalled on the left) is reversible, we have to show that if
the conclusion is provable then the premise also is, i.e. that the rule on the right
is admissible:
Γ, A ⊢ B Γ⊢A⇒B
(⇒I )
Γ⊢A⇒B Γ, A ⊢ B
Suppose that we have a proof π of the conclusion Γ ⊢ A ⇒ B. We can construct
a proof of Γ, A ⊢ B by
π
Γ⊢A⇒B
(wk) (ax)
Γ, A ⊢ A ⇒ B Γ, A ⊢ A
(⇒E )
Γ, A ⊢ B
CHAPTER 2. PROPOSITIONAL LOGIC 66

For instance, we want to prove the formula X ⇒ Y ⇒ X ∧ Y . We can try

to apply the reversible rules as long as we can, and indeed, we end up with a
proof:
(ax) (ax)
X, Y ⊢ X X, Y ⊢ Y
(∧I )
X, Y ⊢ X ∧ Y
(⇒I )
X ⊢Y ⇒X ∧Y
(⇒I )
⊢X ⇒Y ⇒X ∧Y

2.4.2 Proof search. Proof search can be automated in NJ: there is an algo-
rithm which, given a sequent, determines whether it is provable or not. We
describe here such an algorithm where, for simplicity, we restrict ourselves here
to the implicational fragment (formulas are built out of variables and implica-
tion, and the rules are (ax), (⇒E ) and (⇒I )).
Suppose that we are trying to determine whether a given sequent Γ ⊢ A
is provable. It can be observed that, depending on the formula A (which is
either of the form B ⇒ C or a variable X), we can always look for proofs of the
following form:
(a) Γ ⊢ B ⇒ C: the last rule is

Γ, B ⊢ C
(⇒I )
Γ⊢B⇒C

and we look for a proof of Γ, B ⊢ C,

(b) Γ ⊢ X: the proof ends with
..
.
(ax) ..
Γ ⊢ A1 ⇒ A2 ⇒ . . . ⇒ An ⇒ X Γ ⊢ A1 .
(⇒E )
Γ ⊢ A2 ⇒ . . . ⇒ An ⇒ X Γ ⊢ A2
(⇒E )
.. ..
. .
(⇒E )
Γ ⊢ An ⇒ X Γ ⊢ An
(⇒E )
Γ⊢X

where the particular case n = 0 is

(ax)
Γ⊢X

and we thus try to find in the context a formula of the form

A1 ⇒ . . . ⇒ An ⇒ X

such that all the Γ ⊢ Ai are provable.

Namely, the first case is justified by the fact that (⇒I ) is reversible so that it
can always be applied first, and the second one by the fact that we can look for
cut-free proofs (theorem 2.3.3.1) so that we can restrict to the cases where the
rules (⇒E ) have a principal premise which is a rule (ax) or (⇒E ), but not (⇒I ).
This suggests the following procedure to determine the provability of a given
sequent Γ ⊢ A:
CHAPTER 2. PROPOSITIONAL LOGIC 67

– if A is of the form B ⇒ C, we recursively try to prove the sequent Γ, B ⊢ C,

– if A is a variable X, we try to find in the context Γ a formula of the form
A1 ⇒ . . . ⇒ An ⇒ X such that all the sequents Γ ⊢ Ai are provable,
which can be tested recursively.
The problem with this procedure is that it might not terminate. For instance,
given the sequent X ⇒ X ⊢ X, the procedure will loop, trying to construct an
infinite proof tree of the form
..
.
(ax) (⇒E )
Γ`X⇒X Γ`X
(ax) (⇒E )
Γ`X⇒X Γ`X
(ax) (⇒E )
Γ`X⇒X Γ`X
(⇒E )
Γ`X

In order to prevent this kind of loops, we should ensure that, whenever we are
trying to construct a proof of a sequent Γ ⊢ A, we never try to construct again
a proof of Γ ⊢ A at a later stage, and this is easily done by remembering all
the sequents encountered during proof search. An actual implementation is
provided in figure 2.4, where we use a list seen to remember the sequents that
we have already seen, a sequent being encoded as a pair consisting of a context
(a list of formulas) and a formula.
Writing Γ for the context X ⇒ Y, (X ⇒ Y ) ⇒ X, our algorithm will find
that Γ ⊢ Y is provable because there is the proof
(ax) (ax)
Γ, X ⊢ X ⇒ Y Γ, X ⊢ X
(⇒E )
Γ, X ⊢ Y
(ax) (⇒I )
Γ ⊢ (X ⇒ Y ) ⇒ X Γ⊢X⇒Y
(ax) (⇒E )
Γ⊢X⇒Y Γ⊢X
(⇒E )
Γ⊢Y

Note that we are trying to prove Y twice during the proof search, but this is
authorized because this is done in different contexts (respectively in the contexts
Γ and Γ, X). As it can be observed in the above example, when looking for a
proof a sequent Γ ⊢ A, the contexts can grow during proof search. Termination
is however still guaranteed because it can be shown that all the formulas that
we add to the context are strict subformulas of the original formula A, and
there are only a finite number of those. The algorithm can be shown to be in
PSPACE (i.e. it requires an amount of memory which is polynomial in the size
of its input) and the problem is actually PSPACE-complete (it is harder than
any other problem in PSPACE, which in particular implies that it is harder
than any problem in NP), see [Sta79] and [SU06, section 6.6]. Other methods
for performing proof search in intuitionistic logic are presented in section 2.6.5.

2.5 Classical logic

As we have seen in section 2.3.5, not all the formulas that we might expect to
hold in logic are provable in intuitionistic logic, such as the excluded middle
CHAPTER 2. PROPOSITIONAL LOGIC 68

(** Formulas. *)
type t =
| Var of string
| Imp of t * t

(** Split arguments and target of implications. *)

let rec split_imp = function
| Var x -> [], Var x
| Imp (a, b) ->
let args, tgt = split_imp b in
a::args, tgt

(** Determine whether a sequent is provable in a given context. *)

let rec provable seen env a =
not (List.mem (env,a) seen) &&
let seen = (env,a)::seen in
match a with
| Var x ->
List.exists (fun a ->
let args, b = split_imp a in
b = Var x && List.for_all (provable seen env) args
) env
| Imp (a, b) -> provable seen (a::env) b

let provable = provable []

Figure 2.4: Deciding provability in intuitionistic logic.

CHAPTER 2. PROPOSITIONAL LOGIC 69

(theorem 2.3.5.2), which states that ¬A ∨ A holds. In contrast, the usual notion
of validity (e.g. coming from boolean models) is called classical logic. If classical
logic is closer to the usual intuition of validity, the main drawback for us is that
this logic is not constructive, in the sense that we cannot necessarily extract
witnesses from proofs: if we have proved A ∨ B in classical logic, we do not
necessarily know which one of A or B actually holds. For instance, a well-
known typical classical reasoning is the following:
Proposition 2.5.0.1. There exist two irrational numbers a and b such that ab is
rational.
√ √
Proof. We know that 2 is irrational: if 2 = p/q then p2 = 2q 2 , but the
number of prime factors is even on the left and odd on√the right. Reasoning
√ 2
using the excluded middle, we know that the number 2 is either rational or
irrational:
√
– if it is rational, we conclude with a = b = 2,
√
√ 2 √
– otherwise, we take a = 2 and b = 2, and we have ab = 2 which
concludes the proof.
While we could prove the property, we are not able, from the proof, to exhibit
a concrete value for a and b.
Another principle which is inherently classical is the double negation prin-
ciple, which states that ¬¬A ⇒ A. We can see it in action in the following
proof:
Proposition 2.5.0.2. Either (π + e) or (π − e) is irrational.
Proof. By contradiction. Suppose that both (π + e) and (π − e) are rational.
Then 2π would also be rational, since it can be obtained as their sum, and we
reach a contradiction, since it is well-known that π is irrational.
In the above reasoning, writing A for the proposition, we have shown that we
have ¬A ⇒ ⊥, from which we deduced A, i.e. we have implicitly used ¬¬A ⇒ A.
Again, we can see that the proof is not constructive: we cannot exact from it
which of the two numbers is irrational (and, in fact, this is currently an open
problem).
From the proof-as-program correspondence, the excluded middle is also quite
puzzling. Suppose that we are in a logic rich enough to encode Turing machines
(or, equivalently, execute a program in a usual programming language) and that
we have a predicate Halts(M ) which holds when M is halting (you should find
this quite plausible after having read chapter 6). In classical logic, the formula

¬ Halts(M ) ∨ Halts(M )

holds for every Turing machine M , which seems to mean that we should be able
to decide whether a Turing machine is halting or not, but there is no hope of
finding such an algorithm since Turing has shown that the halting problem is
undecidable [Tur37b].
CHAPTER 2. PROPOSITIONAL LOGIC 70

2.5.1 Axioms for classical logic. A logical system for classical logic, called
NK (for K lassical N atural deduction), can be obtained from NJ (figure 2.1) by
adding a new rule corresponding to the excluded middle
(lem)
Γ ⊢ ¬A ∨ A

In this sense, the excluded middle is the only thing which is missing in intu-
itionistic logic to be classical. This is shown in theorems 2.5.6.1 and 2.5.6.5.
In fact, excluded middle is not the only possible choice, and other equiva-
lent axioms can be added instead. Most of those axioms correspond to usual
reasoning patterns, which have been known for a long time, and thus bear latin
names.
Theorem 2.5.1.1. The following principles are equivalent in NJ:
(i) excluded middle, also called tertium non datur:

¬A ∨ A

(ii) double-negation elimination or reductio ad absurdum:

¬¬A ⇒ A

(iii) contraposition:
(¬B ⇒ ¬A) ⇒ (A ⇒ B)

(iv) counter-example principle:

¬(A ⇒ B) ⇒ A ∧ ¬B

(v) Peirce’s law:

((A ⇒ B) ⇒ A) ⇒ A

(vi) Clavius’ law or consequentia mirabilis:

(¬A ⇒ A) ⇒ A

(vii) Tarski’s formula:

A ∨ (A ⇒ B)

(viii) one of the following de Morgan laws:

¬(¬A ∧ ¬B) ⇒ A ∨ B
¬(¬A ∨ ¬B) ⇒ A ∧ B

(ix) material implication:

(A ⇒ B) ⇒ (¬A ∨ B)

(x) ⇒/∨ distributivity:

(A ⇒ (B ∨ C)) ⇒ ((A ⇒ B) ∨ C)
CHAPTER 2. PROPOSITIONAL LOGIC 71

By “equivalent” we mean here that if we suppose that one holds for every
formulas A, B and C then the other one also holds for every formulas A, B
and C, and conversely.
Proof. We only show here the equivalence between the first two, the other ones
being left as an exercise. Supposing that the excluded middle holds, we can
show reductio ad absurdum by
(ax) (ax)
¬¬A, ¬A ` ¬¬A ¬¬A, ¬A ` ¬A
(¬E ) (ax)
¬¬A ` ¬A ∨ A ¬¬A, ¬A ` A ¬¬A, A ` A
(∨E )
¬¬A ` A
(⇒I )
` ¬¬A ⇒ A
(2.2)
Supposing that reductio ad absurdum holds, we can show the excluded middle
by
π
⊢ ¬¬(¬A ∨ A) ⇒ (¬A ∨ A) ⊢ ¬¬(¬A ∨ A)
(⇒E )
⊢ ¬A ∨ A (2.3)
where π is the proof of ¬¬(¬A ∨ A) given on page 63.
Remark 2.5.1.2. One should be careful about the quantifications over formu-
las involved in theorem 2.5.1.1. In order to illustrate this, let us detail the
equivalence between excluded middle and reductio ad absurdum. We say that
a formula A is decidable when ¬A ∨ A holds and stable when ¬¬A ⇒ A holds.
The derivation (2.2) shows that every decidable formula is stable, but the con-
verse does not hold: the derivation (2.3) only shows that A is decidable when
¬A ∨ A (as opposed to A) is stable. In fact a concrete example of a formula
which is stable but not decidable can be given by taking A = ¬X: the for-
mula ¬¬¬X ⇒ ¬X holds (theorem 2.5.9.4), but ¬¬X ∨ ¬X cannot be proved
(theorem 2.3.5.3). Thus, it is important to note that theorem 2.5.1.1 does not
say that a formula is stable if and only if it is decidable, but rather that every
formula is stable if and only if every formula is decidable.
Among those axioms, Pierce’s law is less natural than others but has the ad-
vantage of requiring only implication, so that it still makes sense in some small
fragments of logic such as implicational logic. Also note that the fact that ma-
terial implication occurs in this list means that A ⇒ B is not equivalent to
¬A ∨ B in NJ, in contrast to NK. For each of these axioms, we could add more
or less natural forms of rules. For instance, the law of the excluded middle can
also be implemented by the nicer looking rule
Γ, ¬A ⊢ B Γ, A ⊢ B
(lem)
Γ⊢B
similarly, reductio ad absurdum can be implemented by one of the following
rules
Γ ⊢ ¬¬A Γ, ¬A ⊢ ⊥ Γ, ¬A ⊢ A
(¬¬E )
Γ ⊢ ¬¬A ⇒ A Γ⊢A Γ⊢A Γ⊢A
Since classical logic is obtained from intuitionistic by adding axioms, it is
obvious that
CHAPTER 2. PROPOSITIONAL LOGIC 72

Lemma 2.5.1.3. An intuitionistic proof is a valid classical proof.

We have seen that the converse does not hold (theorem 2.3.5.2), but we will see
in section 2.5.9 that we can still embed classical proofs in intuitionistic logic.

2.5.2 The intuition behind classical logic. Let us try to give some proof
theoretic intuition about how classical logic works.

Proof irrelevance. We have already mentioned that we can interpret a formula

as a set JAK, intuitively corresponding to all the proofs of A, and implications
as function spaces: JA ⇒ BK = JAK → JBK. In this interpretation, ⊥ of course
corresponds to the empty set since we do not expect to have a proof of it:
J⊥K = ∅. Now, given a formula A, its negation ¬A = (A ⇒ ⊥) is interpreted as
the set of functions from JAK to ∅:
– if JAK is non-empty, the set J¬AK = JAK → ∅ is empty,

– if JAK is empty, the set J¬AK = ∅ → ∅ contains exactly one element.

The last point might seem surprising, but if we think hard about it it makes
sense. For instance, in set theory, a function f : JAK → JBK is usually defined as
a relation f ⊆ JAK × JBK which satisfies some properties, expressing that each
element of JAK should have exactly one image in JBK. Now, when both the sets
are empty, we are looking for a relation f ⊆ ∅ × ∅ and there is exactly one such
relation: the empty set (which trivially satisfies the axioms for functions).
Applying twice the reasoning above, we get that
– if JAK is non-empty, J¬¬AK contains exactly one element,
– if JAK is empty, J¬¬AK is empty.

In other words, ¬¬A can be seen as the formula A where the only thing which
matters is not all the proofs of A (i.e. the elements of JAK), but only whether
there exists a proof of A or not, since we have reduced its contents to at most
one point. For this reason, doubly negated formulas are sometimes said to be
proof irrelevant: again, the actual proof does not matter, only its existence. For
instance, we now understand why

¬¬(¬A ∨ A)

is provable intuitionistically (see page 63): it states that it is true that there
exists a proof of ¬A or a proof of A, as opposed to ¬A ∨ A which states that we
have a proof of ¬A or a proof of A. From this point of view, the classical axiom

¬¬A ⇒ A

now seems like deep magic: it means that if we know that there exists a proof
of A, we can actually extract a proof of A. This can only be true if we assume
that there can be at most one proof for a formula, i.e. formulas are interpreted
as booleans and not sets (see section 2.5.4 for a logical point of view on this).
This also explains why we can actually embed classical logic into intuitionistic
logic by double-negating formulas, see section 2.5.9: if we are only interested in
their existence, intuitionistic proofs behave classically.
CHAPTER 2. PROPOSITIONAL LOGIC 73

Resetting proofs. Let us give another, more operational, point of view on the
axiom ¬¬A ⇒ A. We have mentioned that it is equivalent to having the rule

Γ ⊢ ¬¬A
(¬¬E )
Γ⊢A

so that when searching for a proof of A, we can instead prove ¬¬A. What do
we gain in doing so? At first it does not seem much, since we can go back to
proving A:
..
.
(ax)
Γ, ¬A ⊢ ¬A Γ, ¬A ⊢ A
(¬E )
Γ, ¬A ⊢ ⊥
(¬I )
Γ ⊢ ¬¬A
But there is one difference: we now have the additional hypothesis ¬A in our
context, and we can use it at any point in the proof to go back to proving A
instead of the current goal B, while keeping the current context:
..
.
(ax)
Γ′ , ¬A ⊢ ¬A ′
Γ , ¬A ⊢ A
(¬E )
Γ′ , ¬A ⊢ ⊥
(⊥E )
Γ′ , ¬A ⊢ B

In other words, we can “reset proofs” during proof search, i.e. we can implement
the following behavior (up to minor details such as weakening):

..
.
′
Γ ⊢A
(reset)
Γ′ ⊢ B
..
.
Γ⊢A

Note that we keep the context Γ′ after the reset.

Now, let us show how we can use this to prove ¬A ∨ A. When faced with the
disjunction, we choose the left branch, i.e. prove ¬A, which by (¬I ) amounts
to proving ⊥, supposing A as hypothesis. Instead of going on and proving ⊥,
which is quite hopeless, we use our reset mechanism and go back to proving
¬A ∨ A: while doing so we have kept A as hypothesis! So, this time we chose to
prove A, which can be done by an axiom. If we think of reset as the possibility
of “going back in time” and changing one’s mind, this proof implements the
following conversation between us, trying to build the proof, and an opponent
trying to prove us wrong:
— Show me the formula ¬A ∨ A.
— Ok, I will show that ¬A holds.
— Here is a proof π of A, show me how to deduce ⊥.
CHAPTER 2. PROPOSITIONAL LOGIC 74

— Actually, I changed my mind, I will prove A, here is the proof: π.

The formal proof goes like this
(ax)
A⊢A
(∨rI )
A ⊢ ¬A ∨ A
(reset)
A⊢⊥
(¬I )
⊢ ¬A
(∨lI )
⊢ ¬A ∨ A

In more details, the proof begins by proving ¬¬(¬A ∨ A) instead of ¬A ∨ A and

then proceeds as in the proof given on page 63. This idea of resetting will be
explored again, in a different form, in section 4.6.

2.5.3 A variant of natural deduction. The presentation given in section 2.5.1

is not very “canonical” in the sense that it amounts to randomly add an axiom
from the list given in theorem 2.5.1.1. We would like to present another ap-
proach which consists in slightly changing the calculus, and allows for a much
more pleasant proof system. We now consider sequents of the form

Γ⊢∆

where both Γ and ∆ are contexts. Such a sequent should be read as “supposing
all the formula in Γ, I can prove some formula in ∆”. This is a generalization of
previous sequents, where ∆ was restricted to exactly one formula. The rules for
this sequent calculus are given in figure 2.5. In order to simplify the presentation,
we consider here that the formulas of ∆ can be explicitly permuted, duplicated,
and so on, using the structural rules (xchR ), (wkR ), (contrR ) and (⊥R ), which
we generally leave implicit in examples. Those rules are essentially the same as
those for NJ, with contexts added on the right, except for the rules (∨lI ) and
(∨rI ), which are now combined into the rule

Γ ⊢ A, B, ∆
(∨I )
Γ ⊢ A ∨ B, ∆

In order to prove a disjunction A ∨ B, we do not have to choose anymore if we

want to prove A or B: we can try to prove both at the same time. This means
that there can be some “exchange of information” between the proofs of A and
of B (via the context Γ). For instance, we have that the excluded middle can
be proved by
(ax)
A ⊢ A, ⊥
(xchR )
A ⊢ ⊥, A
(¬I )
⊢ ¬A, A
(∨I )
⊢ ¬A ∨ A
Note that the formula A in the context, obtained from the ¬A, is used in the
axiom in order to prove the other A. Similarly, double negation elimination is
CHAPTER 2. PROPOSITIONAL LOGIC 75

(ax)
Γ, A, Γ′ ⊢ A, ∆

Γ ⊢ A ⇒ B, ∆ Γ ⊢ A, ∆ Γ, A ⊢ B, ∆
(⇒E ) (⇒I )
Γ ⊢ B, ∆ Γ ⊢ A ⇒ B, ∆

Γ ⊢ A ∧ B, ∆ l Γ ⊢ A ∧ B, ∆ r Γ ⊢ A, ∆ Γ ⊢ B, ∆
(∧E ) (∧E ) (∧I )
Γ ⊢ A, ∆ Γ ⊢ B, ∆ Γ ⊢ A ∧ B, ∆

(⊤I )
Γ ⊢ ⊤, ∆

Γ ⊢ A ∨ B, ∆ Γ, A ⊢ C, ∆ Γ, B ⊢ C, ∆ Γ ⊢ A, B, ∆
(∨E ) (∨I )
Γ ⊢ C, ∆ Γ ⊢ A ∨ B, ∆

Γ⊢∆
(⊥I )
Γ ⊢ ⊥, ∆

Γ ⊢ ¬A, ∆ Γ ⊢ A, ∆ Γ, A ⊢ ⊥, ∆
(¬E ) (¬I )
Γ ⊢ ⊥, ∆ Γ ⊢ ¬A, ∆

structural rules:

Γ ⊢ ∆, A, B, ∆′ Γ ⊢ ∆, ∆′
(xchR ) (wkR )
Γ ⊢ ∆, B, A, ∆′ Γ ⊢ ∆, A, ∆′

Γ ⊢ ∆, A, A, ∆′ Γ ⊢ ∆, ⊥, ∆′
(contrR ) (⊥R )
Γ ⊢ ∆, A, ∆′ Γ ⊢ ∆, ∆′

Figure 2.5: NK: rules of classical natural deduction.

CHAPTER 2. PROPOSITIONAL LOGIC 76

proved by
(ax)
¬¬A, A ⊢ A
(wkR )
¬¬A, A ⊢ ⊥, A
(ax) (¬I )
¬¬A ⊢ ¬¬A, A ¬¬A ⊢ ¬A, A
(¬E )
¬¬A ⊢ ⊥, A
(⊥E )
¬¬A ⊢ A, A
(contrR )
¬¬A ⊢ A
(⇒I )
⊢ ¬¬A ⇒ A

Again, instead of proving A, we decide to either prove ⊥ or A.

The expected elimination rule for the constant ⊥ (shown on the left) is not
present, but it can be derived (as shown on the right):

Γ ⊢ ⊥, ∆
(⊥R )
Γ ⊢ ⊥, ∆ Γ⊢∆
(⊥E ) (wkR )
Γ ⊢ A, ∆ Γ ⊢ A, ∆

In fact the constant ⊥ is now superfluous, since one can convince himself that
proving ⊥ amounts to proving the empty sequent ∆.

2.5.4 Cut-elimination in classical logic. Classical logic also does have the
cut-elimination property, see section 2.3.3, although this is more subtle to show
than in the case of intuitionistic logic due to the presence of structural rules. In
particular, in addition to the usual cut elimination steps, we need to add rules
making elimination rules “commute” with structural rules: namely, an intro-
duction and the corresponding elimination rules can be separated by structural
rules. For instance, suppose that we want to eliminate the following “cut”:

π π′
Γ⊢A Γ⊢B
(∧I )
Γ⊢A∧B
(wkR )
Γ ⊢ A ∧ B, C
(∧lE )
Γ ⊢ A, C

We first need to make the elimination rule for conjunction commute with the
weakening:
π π′
Γ⊢A Γ⊢B
(∧I )
Γ⊢A∧B
(∧lE )
Γ⊢A
(wkR )
Γ ⊢ A, C
and then we can finally properly eliminate the cut:

π
(∧lE )
Γ⊢A
(wkR )
Γ ⊢ A, C
CHAPTER 2. PROPOSITIONAL LOGIC 77

Another surprising phenomenon was observed by Lafont [Gir89, section B.1].

Depending on the order in which we eliminate cuts, the following proof
π π′
Γ⊢A Γ⊢B
(wkR ) (wkR )
Γ ⊢ ¬C, A Γ ⊢ C, B
(¬E )
Γ ⊢ ⊥, A, B
(⊥R )
Γ ⊢ A, B
both cut-eliminates to
π π′
Γ⊢A Γ⊢B
(wkR ) and (wkR )
Γ ⊢ A, B Γ ⊢ A, B
This is sometimes called Lafont’s critical pair. We like to identify proofs up to
cut elimination (much more on this in chapter 4) and therefore those two proofs
should be considered as being “the same”. In particular, when both π and π ′
are proofs of Γ ⊢ A, i.e. A = B, this forces us to identify the two proofs
π π′
Γ⊢A Γ⊢A
(wkR ) (wkR )
Γ ⊢ A, A Γ ⊢ A, A
(contrR ) and (contrR )
Γ⊢A Γ⊢A
and thus to identify the two proofs π and π ′ . More generally, by similar rea-
soning, any two proofs of a same sequent Γ ⊢ ∆ should be identified. Cuts can
hurt! This gives another, purely logical, explanation of why classical logic is
“proof irrelevant”, as already mentioned in section 2.5.2: up to cut-elimination,
there is at most one proof of a given sequent.

2.5.5 De Morgan laws. In classical logic, the well-known de Morgan laws

hold:
¬(A ∧ B) ⇔ ¬A ∨ ¬B ¬⊤ ⇔ ⊥ A ⇒ B ⇔ ¬A ∨ B
¬(A ∨ B) ⇔ ¬A ∧ ¬B ¬⊥ ⇔ ⊤ ¬¬A ⇔ A

Definable connectives. Because of these laws, many connectives are superfluous.

For instance, classical logic can be axiomatized with ⇒ and ⊥ as the only
connectives, since we can define
A ∨ B = ¬A ⇒ B A ∧ B = ¬(A ⇒ ¬B) ¬A = A ⇒ ⊥ ⊤=⊥⇒⊥
and the logical system can be reduced to the following four rules:
Γ⊢∆
′ (ax) (⊥I )
Γ, A, Γ ⊢ A, ∆ Γ ⊢ ⊥, ∆

Γ ⊢ A ⇒ B, ∆ Γ ⊢ A, ∆ Γ, A ⊢ B, ∆
(⇒E ) (⇒I )
Γ ⊢ B, ∆ Γ ⊢ A ⇒ B, ∆
together with the four structural rules. Several other choices of connectives are
possible.
CHAPTER 2. PROPOSITIONAL LOGIC 78

Clausal form. It is natural to consider the equivalence relation on formulas which

identifies any two formulas A and B such that A ⇔ B. The de Morgan laws can
be used to rewrite every formula into a canonical representative of its equivalence
class induced by this equivalence relation. We first need to introduce some
classes of formulas.
A literal L is either a variable or a negated variable:
L ::= X | ¬X
A clause C is a disjunction of literals:
C ::= L | C ∨ C | ⊥
A formula A is in clausal form or in conjunctive normal form when it is a
conjunction of clauses:
A ::= C | A ∧ A | ⊤
Proposition 2.5.5.1. Every formula is equivalent to one in clausal form.
One way to show this result is to use the de Morgan laws, as well as usual
intuitionistic laws (section 2.2.5), in order to push negations toward variables
and disjunctions below conjunctions, i.e. we replace subformulas according to
the following rules, until no rule applies:
¬(A ∧ B) ⇝ ¬A ∨ ¬B ¬⊤ ⇝ ⊥
¬(A ∨ B) ⇝ ¬A ∧ ¬B ¬⊥ ⇝ ⊤
(A ∧ B) ∨ C ⇝ (A ∨ C) ∧ (B ∨ C) ⊤∨C ⇝⊤
A ∨ (B ∧ C) ⇝ (A ∨ B) ∧ (A ∨ C) A∨⊤⇝⊤
A ⇒ B ⇝ ¬A ∨ B ¬¬A ⇝ A
Those rules rewrite formulas into classically equivalent ones, since those are
instances of de Morgan laws. However, it is not clear that the process terminates.
It does, but it is not efficient, and we will see below a better way to rewrite a
formula in clausal form.
Example 2.5.5.2. A clausal form of (X ⇒ Y ) ⇒ (Y ⇒ Z) can be computed by
¬(¬X ∨ Y ) ∨ (¬Y ∨ Z) ⇝ (¬¬X ∧ ¬Y ) ∨ (¬Y ∨ Z)
⇝ (X ∧ ¬Y ) ∨ (¬Y ∨ Z)
⇝ (X ∨ ¬Y ∨ Z) ∧ (¬Y ∨ ¬Y ∨ Z)

Efficient computation of the clausal form. Given a clause C, we write L(C) for
the set of literals occurring in it:
L(X) = {X} L(¬X) = {¬X} L(C ∨ D) = L(C) ∪ L(D) L(⊥) = ∅
A variable X occurs positively (resp. negatively) in A if we have X ∈ L(C)
(resp. ¬X ∈ L(C)). Up to equivalence, formulas satisfy the laws of commutative
idempotent monoids with respect to ∨ and ⊥:
(A ∨ B) ∨ C ⇔ A ∨ (B ∨ C) ⊥∨A⇔A B∨A⇔A∨B
A∨⊥⇔A A∨A⇔A
Because of this, a clause is characterized by the set of literals occurring in it,
see section A.2:
CHAPTER 2. PROPOSITIONAL LOGIC 79

Lemma 2.5.5.3. Given clauses C and D, if L(C) = L(D) then C ⇔ D.

Similarly, a formula in clausal form is characterized by the set of clauses occur-
ring in it. A formula in clausal form A can thus be encoded as a set of sets of
literals:
A = {{L11 , . . . , L1k1 }, . . . , {Ln1 , . . . , Lnkn }}
Note that the empty set ∅ corresponds to the formula ⊤ whereas the set {∅}
corresponds to the formula ⊥. In practice, we can represent a formula as a list
of lists of clauses (where the order or repetitions of the elements of the lists do
not matter). Based on this, an algorithm for putting a formula in clausal form is
provided in figure 2.6. A literal is encoded as a pair consisting of a variable and
a boolean indicating whether it is negated or not (by convention, false means
negated), a clause as a list of literals, and clausal form as a list of clauses. Given
a formula A, the functions pos and neg compute the clausal form of A and ¬A,
respectively. They are using the function merge, which, given two formulas in
clausal form

A = {C1 , . . . , Cm } and B = {D1 , . . . , Dn }

computes the clausal form of A ∨ B, which is

A ∨ B = {Ci ∪ Dj | 1 ⩽ i ⩽ m, 1 ⩽ j ⩽ n}

The notion of clausal form can be further improved as follows. We say that
a formula is in canonical clausal form when
1. it is in clausal form,
2. it does not contain twice the same clause or ⊤ (this is automatic if it is
represented as a set of clauses),
3. no clause contains twice the same literal or ⊥ (this is automatic if they
are represented as sets of literals),
4. no clause contains both a literal and its negation.
For the last point, given a clause C containing both X and ¬X, the equivalences
¬X ∨ X ⇔ ⊤ and ⊤ ∨ A ⇔ ⊤ imply that the whole clause is equivalent to ⊤ and
can thus be removed from the formula. For instance, the clausal form computed
in theorem 2.5.5.2 is not canonical because it does not satisfy the second point
above.
Exercise 2.5.5.4. Modify the algorithm of figure 2.6 so that it computes canonical
clausal forms.

De Morgan laws in intuitionistic logic. Let us insist once again on the fact that
the de Morgan laws do not hold in intuitionistic logic. Namely, the following
implications are intuitionistically true, but not their converse:

A ∨ B ⇒ ¬(¬A ∧ ¬B) ¬A ∨ ¬B ⇒ ¬(A ∧ B)

A ∧ B ⇒ ¬(¬A ∨ ¬B) ¬A ∨ B ⇒ A ⇒ B

However, the following equivalence does hold intuitionistically:

¬A ∧ ¬B ⇔ ¬(A ∨ B)
CHAPTER 2. PROPOSITIONAL LOGIC 80

type var = int

(** Formulas. *)
type t =
| Var of var
| And of t * t
| Or of t * t
| Imp of t * t
| Not of t
| True | False

type literal = bool * var (** Literal. *) (* false = negated *)

type clause = literal list (** Clause. *)
type cnf = clause list (** Clausal formula. *)

let clausal a : cnf =

let merge a b =
List.flatten (List.map (fun c -> List.map (fun d -> c@d) b) a)
in
let rec pos = function
| Var x -> [[true, x]]
| And (a, b) -> let a = pos a in let b = pos b in a@b
| Or (a, b) -> let a = pos a in let b = pos b in merge a b
| Imp (a, b) -> let a = neg a in let b = pos b in merge a b
| Not a -> neg a
| True -> []
| False -> [[]]
and neg = function
| Var x -> [[false, x]]
| And (a, b) -> let a = neg a in let b = neg b in merge a b
| Or (a, b) -> let a = neg a in let b = neg b in a@b
| Imp (a, b) -> let a = pos a in let b = neg b in a@b
| Not a -> pos a
| True -> [[]]
| False -> []
in
pos a

(* The clausal form of (x y) (¬x ∧ y) is (¬x ∨ ¬y) ∧ (x ∨ y) *)

let f =
let x = Var 0 in
let y = Var 1 in
clausal (Or (Not (Or (Not x, y)), And (Not x, y)))

Figure 2.6: Rewriting a formula to a clausal form.

CHAPTER 2. PROPOSITIONAL LOGIC 81

2.5.6 Boolean models. Classical natural deduction matches exactly the no-
tion of truth one would get from usual boolean models. Let us detail this. We
write B = {0, 1} for the set of booleans. A valuation ρ is a function X → B,
assigning booleans to variables. Such a valuation can be extended to a function
ρ : Prop → B, from propositions to booleans, by induction over the propositions
by

ρ(X) = 1 iff ρ(X) = 1

ρ(A ⇒ B) = 1 iff ρ(A) = 0 or ρ(B) = 1
ρ(A ∧ B) = 1 iff ρ(A) = 1 and ρ(B) = 1
ρ(⊤) = 1
ρ(A ∨ B) = 1 iff ρ(A) = 1 or ρ(B) = 1
ρ(⊥) = 0

Given a formula A and a valuation ρ, we write ⊨ρ A whenever ρ(A) = 1

and say that the formula A is satisfied in the valuation ρ. Given a context
Γ = A1 , . . . , An , we write Γ ⊨ρ A whenever ⊨ρ ( i=1 Ai ) ⇒ A. Finally, we
Vn
write Γ ⊨ A whenever Γ ⊨ρ A for every valuation ρ and, in this case, say that
A is valid in the context Γ or that the sequent Γ ⊢ A is valid.
The system NK is correct in the sense that it only allows the derivation of
valid sequents.
Theorem 2.5.6.1 (Soundness). If Γ ⊢ A is derivable then Γ ⊨ A.
Proof. By induction on the proof of Γ ⊢ A.
Since NJ is a subsystem of NK, it thus also allows only the derivation of valid
sequents. As simple as it may seem, the above theorem allows proving the
consistency of intuitionistic and classical logic (which was already demonstrated
in theorem 2.3.4.2 for intuitionistic logic):
Corollary 2.5.6.2. The system NK (and thus also NJ) is consistent.
Proof. Suppose that NK is not consistent. By theorem 2.3.4.1, we would have
a proof of ⊢ ⊥. By theorem 2.5.6.1, we would have ρ(⊥) = 1. But ρ(⊥) = 0 by
definition, contradiction.

Conversely, we can show that the system NK is complete, meaning that if a

sequent Γ ⊢ A is valid, i.e. we have Γ ⊨ A, then it is derivable. As a particular
case, we will have that if a formula A is valid then it is provable, i.e. ⊢ A is
derivable. We first need the following lemmas.
Lemma 2.5.6.3. For any formulas A and B, variable X and valuation ρ, we have
ρ(A[B/X]) = ρ′ (A), where ρ′ (X) = ρ(B) and ρ′ (Y ) = ρ(Y ) for X ̸= Y .
Proof. By induction on A.
Lemma 2.5.6.4. For any formula A, the formula

((X ⇒ A[⊤/X]) ∧ (¬X ⇒ A[⊥/X])) ⇒ A

is derivable in NK.
CHAPTER 2. PROPOSITIONAL LOGIC 82

Proof. For conciseness, we write

δX A = (X ⇒ A[⊤/X]) ∧ (¬X ⇒ A[⊥/X])

We reason by induction on the formula A. If A = X then

δX X = (X ⇒ ⊤) ∧ (¬X ⇒ ⊥)

and we have
(ax)
δX X, ¬X ⊢ (X ⇒ ⊤) ∧ (¬X ⇒ ⊥)
(∧rE ) (ax)
δX X, ¬X ⊢ ¬X ⇒ ⊥ δX X, ¬X ⊢ ¬X
(⇒E )
δX X, ¬X ⊢ ⊥
(¬I )
δX X ⊢ ¬¬X
(¬¬E )
δX X ⊢ X
(⇒I )
⊢ δX X ⇒ X

If A = Y with Y ̸= X, we have

δX Y = (X ⇒ Y ) ∧ (¬X ⇒ Y )

and, using the fact that X ∨ ¬X is derivable,

(ax)
δX Y, X ` (X ⇒ Y ) ∧ (¬X ⇒ Y )
(∧lE ) (ax) ..
δX Y, X ` X ⇒ Y δX Y, X ` X .
(⇒E )
δX Y ` X ∨ ¬X δX Y, X ` Y δX Y, ¬X ` Y
(∨E )
δX Y ` Y

Other cases are left to the reader.

Theorem 2.5.6.5 (Completeness). If Γ ⊨ A holds then Γ ⊢ A is derivable.

Proof. We proceed by induction on the number of free variables of A. If
FV(A) = ∅ then we easily show that Γ ⊢ A by induction on A. Otherwise,
pick a variable X ∈ FV(A). By theorem 2.5.6.3, the sequents Γ, X ⊢ A[⊤/X]
and Γ, ¬X ⊢ A[⊥/X] are valid, and thus derivable by induction hypothesis.
Moreover, theorem 2.5.6.4 states that δX A ⇒ A is derivable. We thus have the
derivation
.. ..
. .
Γ, X ` A[>/X] Γ, ¬X ` A[⊥/X]
.. (⇒I ) (⇒I )
. Γ ` X ⇒ A[>/X] Γ ` ¬X ⇒ A[⊥/X]
(∧I )
Γ ` δX A ⇒ A Γ ` δX A
(⇒E )
Γ`A

which allows us to conclude.

A detailed and formalized version of this proof can be found in [CKA15].

Of course, intuitionistic natural deduction is not complete with respect to
boolean models since there are formulas, such as ¬X ∨ X, which evaluate to
CHAPTER 2. PROPOSITIONAL LOGIC 83

true under any valuation but are not derivable (theorem 2.3.5.2). One way to
understand this is that there are “not enough boolean models” in order to detect
that such formulas are not valid. A natural question is thus: is there a way to
generalize the notion of boolean model, so that intuitionistic natural deduction
is complete with respect to this generalized notion of model, i.e. a formula which
is valid in any such a model is necessarily intuitionistically provable? We will
see in section 2.8 that such a notion of model exists: Kripke models.

2.5.7 DPLL. As an aside, we would like to present the usual algorithm to

decide the satisfiability of boolean formulas, which is based on the previous
observations. A propositional formula A is satisfiable when there exists a val-
uation ρ making it true, i.e. such that ⊨ρ A. An efficient way to test whether
this is the case or not is the DPLL algorithm, due to Davis, Putnam, Logemann
and Loveland [DLL62]. The basic idea here is the one we have already seen in
theorem 2.5.6.4: if the formula A is satisfiable by a valuation ρ then, given a
variable X occurring in A, we have either ρ(X) = 0 or ρ(X) = 1 and we can test
whether A is satisfiable in both cases recursively since this makes the number
of variables decrease in the formula (we call this splitting on the variable X):
Lemma 2.5.7.1. Given a variable X, a formula A is satisfiable if and only if the
formula A[⊥/X] or A[⊤/X] is satisfiable.
Proof. If A is satisfiable, then there is a valuation ρ such that ρ(A) = 1. If
ρ(X) = 0 (resp. ρ(X) = 1) then, by theorem 2.5.6.3, ρ(A[⊥/X]) = ρ(A) = 1
(resp. ρ(A[⊤/X]) = ρ(A) = 1) and therefore A[⊥/X] (resp. A[⊤/X]) is sat-
isfiable. Conversely, if A[⊥/X] (resp. A[⊤/X]) is satisfiable by a valuation ρ
then, writing ρ′ for the valuation such that ρ′ (X) = 0 (resp. ρ′ (X) = 1) and
ρ′ (Y ) = ρ(Y ) for Y ̸= X, by theorem 2.5.6.3 we have ρ(A[⊥/X]) = ρ′ (A) = 1
(resp. ρ(A[⊤/X]) = ρ′ (A) = 1).
In the base case, the formula A has no variable and it thus evaluates to the
same value in any environment, and we can easily compute this value: it is
satisfiable if and only if this value is true. This directly leads to a very simple
implementation of a satisfiability algorithm, see figure 2.7: the function subst
computes the substitution of a formula into another one, the function var finds
a free variable, and finally the function sat tests the satisfiability of a formula.
As is, this algorithm is not very efficient: some subformulas get evaluated
many times during the search. It can however be much improved by using formu-
las in canonical clausal form, as described in theorem 2.5.5.1. First, substitution
can be implemented on those as follows:
Lemma 2.5.7.2. Given a canonical clausal formula A and a variable X, a canon-
ical clausal formula for A[⊤/X] (resp. A[⊥/X]) can be obtained from A by

– removing all clauses containing X (resp. ¬X),

– removing ¬X (resp. X) from all remaining clauses.
The computation can be further improved by carefully choosing the variables
we are going to split on first. A unitary clause in a clausal formula A is a
clause containing exactly one literal L. If L is X (resp. ¬X) then, if we split
on X, the branch A[⊥/X] (resp. A[⊤/X]) will fail. Therefore,
CHAPTER 2. PROPOSITIONAL LOGIC 84

(** Formulas. *)
type t =
| Var of int
| And of t * t
| Or of t * t
| Not of t
| True | False

(** Substitute a variable by a formula in a formula. *)

let rec subst x c = function
| Var y -> if x = y then c else Var y
| And (a, b) -> And (subst x c a, subst x c b)
| Or (a, b) -> Or (subst x c a, subst x c b)
| Not a -> Not (subst x c a)
| True -> True | False -> False

(** Find a free variable in a formula. *)

let var a =
let exception Found of int in
let rec aux = function
| Var x -> raise (Found x)
| And (a, b) | Or (a, b) -> aux a; aux b
| Not a -> aux a
| True | False -> ()
in
try aux a; raise Not_found
with Found x -> x

(** Evaluate a closed formula. *)

let rec eval = function
| Var _ -> assert false
| And (a, b) -> eval a && eval b
| Or (a, b) -> eval a || eval b
| Not a -> not (eval a)
| True -> true | False -> false

(** Simple-minded satisfiability. *)

let rec sat a =
try
let x = var a in
sat (subst x True a) || sat (subst x False a)
with Not_found -> eval a

Figure 2.7: Naive implementation of the satisfiability algorithm.

CHAPTER 2. PROPOSITIONAL LOGIC 85

Lemma 2.5.7.3. Consider a clausal formula A containing a unitary clause which

is a literal X (resp. ¬X). Then the formula A is satisfiable if and only if the
formula A[⊤/X] (resp. A[⊥/X]) is.
A literal X (resp. ¬X) is pure in a clausal formula A if ¬X (resp. X) does not
occur in any clause of A: the variable X always occurs with the same polarity
(positive or negative) in the formula.
Lemma 2.5.7.4. A clausal formula A containing a pure literal X (resp. ¬X) is
satisfiable if and only if the formula A[⊤/X] (resp. A[⊥/X]) is satisfiable.
Another way to state the above lemma is that the clauses containing the pure
literal can be removed from the formula without changing its satisfiability.
The DPLL algorithm exploits these optimizations in order to test the satis-
fiability of formula A:
1. it first tries to see if A is obviously satisfiable (if it is ⊤) or unsatisfiable
(if it contains the clause ⊥),
2. otherwise it tries to find a unitary clause and apply theorem 2.5.7.3,
3. otherwise it tries to find a pure clause and apply theorem 2.5.7.4,
4. otherwise it splits on an arbitrary variable by theorem 2.5.7.1.

For the last step, various heuristics have been proposed for choosing the split-
ting variable such as MOM (a variable with Maximal number of Occurrences
in the clauses
P of Minimum size) or Jeroslow-Wang (a variable with maximum
−|C|
J(X) = C 2 where C ranges over clauses containing X and |C| is the
number of literals), and so on.
A concrete implementation is provided in figure 2.8. The function sub im-
plements substitution as described in theorem 2.5.7.2, the function unit finds a
unitary clause (or raises Not_found if there is none), the function pure finds a
pure literal (or raises Not_found) and finally the function dpll implements the
above algorithm. The function pure uses an auxiliary list vars of pairs X,b
where X is a variable and b is either Some true or Some false if the variable X
occurs only positively or negatively, or None if it occurs both positively and
negatively.

2.5.8 Resolution. The resolution procedure is a generalization of the previous

DPLL algorithm which was introduced by Davis and Putnam [DP60]. It is not
the most efficient algorithm, but one of the main interesting points about it is
that it generalizes well to first-order logic, see section 5.4.6. It stems from the
following observation.
Lemma 2.5.8.1 (Correctness). Suppose given two clauses of the form C ∨ X
and ¬X ∨ D, containing a variable X and its negation ¬X, respectively. Then
the formula C ∨ D is a consequence of them.
Proof. Given a valuation ρ such that ρ(C ∨ X) = ρ(¬X ∨ D) = 1,
– if ρ(X) = 1 then necessarily ρ(D) = 1 and thus ρ(C ∨ D) = 1,

– if ρ(X) = 0 then necessarily ρ(C) = 1 and thus ρ(C ∨ D) = 1.

CHAPTER 2. PROPOSITIONAL LOGIC 86

type var = int (** Variable. *)

type literal = bool * var (** Literal. *) (* false means negated *)
type clause = literal list (** Clause. *)
type cnf = clause list (** Clausal formula. *)

(** Substitution a[v/x]. *)

let subst (a:cnf) (v:bool) (x:var) : cnf =
let a = List.filter (fun c -> not (List.mem (v,x) c)) a in
List.map (fun c -> List.filter (fun l -> l <> (not v, x)) c) a

(** Find a unitary clause. *)

let rec unit : cnf -> literal = function
| [n,x]::a -> n,x
| _::a -> unit a
| [] -> raise Not_found

(** Find a pure literal in a clausal formula. *)

let pure (a : cnf) : literal =
let rec clause vars = function
| [] -> vars
| (n,x)::c ->
try
match List.assoc x vars with
| Some n' ->
if n' = n then clause vars c else
let vars = List.filter (fun (y,_) -> y <> x) vars in
clause ((x,None)::vars) c
| None -> clause vars c
with Not_found -> clause ((x,Some n)::vars) c
in
let vars = List.fold_left clause [] a in
let x, n = List.find (function (x,Some s) -> true | _ -> false) vars in
Option.get n, x

(** DPLL procedure. *)

let rec dpll a =
if a = [] then true
else if List.mem [] a then false
else
try let n,x = unit a in dpll (subst a n x)
with Not_found ->
try let n,x = pure a in dpll (subst a n x)
with Not_found ->
let x = snd (List.hd (List.hd a)) in
dpll (subst a false x) || dpll (subst a true x)

Figure 2.8: Implementation of the DPLL algorithm.

CHAPTER 2. PROPOSITIONAL LOGIC 87

From a logical point of view, this deduction corresponds to the following reso-
lution rule:
Γ⊢C ∨X Γ ⊢ ¬X ∨ D
(res)
Γ⊢C ∨D
In the following, we implicitly consider formulas up to commutativity of dis-
junction, i.e. identify the formulas A ∨ B and B ∨ A, so that the above rule also
applies to clauses containing X and its negation:

Γ ⊢ C1 ∨ X ∨ C2 Γ ⊢ D1 ∨ ¬X ∨ D2
(res)
Γ ⊢ C1 ∨ C2 ∨ D1 ∨ D2

The previous lemma can be reformulated in classical logic as follows:

Lemma 2.5.8.2. The resolution rule is admissible in classical natural deduction.
Proof. We have

Γ ⊢ C′ ∨ X Γ ⊢ ¬X ∨ D′
Γ ⊢ C ′, X Γ ⊢ ¬X, D′
(wk R ) (wkR )
Γ ⊢ C ′ , X, D′ Γ ⊢ C ′ , ¬X, D′
(¬E )
Γ ⊢ C ′ , ⊥, D′
(⊥R )
Γ ⊢ C ′ , D′

where the rule

Γ⊢A∨B
Γ ⊢ A, B
is derivable by
(ax) (ax)
Γ⊢A∨B Γ, A ⊢ A, B Γ, B ⊢ A, B
(∨E )
Γ ⊢ A, B

(in other words, the rule (∨I ) is reversible).

Remark 2.5.8.3. If we recall that in classical logic implication can be defined as
A ⇒ B = ¬A ∨ B, the resolution rule simply corresponds to the transitivity of
implication:
Γ ⊢ ¬C ⇒ X Γ⊢X⇒D
Γ ⊢ ¬C ⇒ D
For simplicity, in the following a context Γ will be seen as a set of clauses (as
opposed to a list of clauses, see section 2.2.10) and will also be interpreted as a
clausal form (the conjunction of its clauses, see section 2.5.5). We will always
implicitly suppose that it is canonical (see section 2.5.5): a clause cannot contain
the same literal twice or a literal and its negation. Previous lemmas entail that
we can prove the sequent Γ ⊢ ⊥ using axiom and resolution rules only when
Γ is not satisfiable: otherwise, ⊥ would also be satisfiable, which it is not by
definition. We are going to show in theorem 2.5.8.7 that this observation admits
a converse.
CHAPTER 2. PROPOSITIONAL LOGIC 88

Resolvent. Given clauses C ∨ X and ¬X ∨ D, the clause C ∨ D does not con-

tain the variable X, which gives us the idea of using resolution to remove the
variable X from a set of formulas by performing all the possible deductions we
can. Suppose given a set Γ of clauses and X a variable. We write

ΓX = {C | C ∨ X ∈ Γ} Γ¬X = {D | ¬X ∨ D ∈ Γ}

and Γ′ for the set of clauses in Γ which contain neither X nor ¬X. We supposed
that the clauses are in canonical form, so that we have the following partition
of Γ:
Γ = Γ′ ⊎ {C ∨ X | C ∈ ΓX } ⊎ {¬X ∨ D | D ∈ Γ¬X }
The resolvent Γ \ X of Γ with respect to X is

Γ \ X = Γ′ ∪ {C ∨ D | C ∈ ΓX , D ∈ Γ¬X }

Remark 2.5.8.4. As defined above, the resolvent might contain clauses not in
canonical form, even if C and D are. In order to keep this invariant, we should
remove all clauses of the form C ∨ D such that C contains a literal and D its
negation, which we will implicitly do; in clauses, we should also remove duplicate
literals.
As indicated above, computing the resolvent reduces the number of free variables
of Γ:
Lemma 2.5.8.5. Given Γ in clausal form and a variable X, we have

FV(Γ \ X) = FV(Γ) \ {X}

Its main interest lies in the fact that it preserves satisfiability:

Lemma 2.5.8.6. Given a clausal form Γ and a variable X, Γ is satisfiable if and
only if Γ \ X is satisfiable.
Proof. The left-to-right implication follows from the correctness of the resolution
rule (theorem 2.5.8.1). For the right-to-left implication, suppose that Γ \ X is
satisfied under a valuation ρ. We are going to show that Γ is satisfied under
either ρ0 or ρ1 , where ρi is defined, for i = 0 or i = 1, by ρi (X) = i and
ρi (Y ) = ρ(Y ) whenever Y ̸= X. We distinguish two cases.
– Suppose that we have ρ(C ′ ) = 1 for every clause C = C ′ ∨ X in ΓX . Then
we can take i = 0. Namely, given a clause C ∈ Γ = Γ′ ⊎ ΓX ⊎ Γ¬X :
– if C ∈ Γ′ then ρ0 (C) = ρ(C) = 1 because C does not contain the
literal X,
– if C ∈ ΓX then C = C ′ ∨ X and ρ0 (C) = 1 because, by hypothesis,
ρ0 (C ′ ) = ρ(C ′ ) = 1,
– if C ∈ Γ¬X then C = C ′ ∨ ¬X and ρ0 (C) = 1 because ρ0 (¬X) = 1
since ρ0 (X) = 0 by definition of ρ0 .
– Otherwise, there exists a clause C = C ′ ∨ X ∈ ΓX such that ρ(C ′ ) = 0.
Then we can take i = 1. Namely, given a clause D ∈ Γ = Γ′ ⊎ ΓX ⊎ Γ¬X :
– if D ∈ Γ′ then ρ1 (D) = ρ(D) = 1 because D does not contain the
literal X,
CHAPTER 2. PROPOSITIONAL LOGIC 89

– if D ∈ ΓX then D = D′ ∨ X and ρ1 (D) = 1 because ρ1 (X) = 1,

– if D ∈ Γ¬X then D = D′ ∨¬X and ρ(C ′ ∨D′ ) = 1 by hypothesis, thus
ρ1 (D′ ) = ρ(D′ ) = 1 because ρ(C ′ ) = 0, thus ρ1 (D) = ρ1 (D′ ∨X) = 1.

The previous lemma implies that resolution is refutation complete in the sense
that it can always be used to show that a set of clauses cannot be satisfied (by
whichever valuation):
Theorem 2.5.8.7 (Refutation completeness). A set Γ of clauses is unsatisfiable
if and only if Γ ⊢ ⊥ can be proved using the axiom and resolution rules only.
Proof. Writing FV(Γ) = {X1 , . . . , Xn } for the free variables of Γ, define the
sequence of sets of clauses Γ0⩽i⩽n by Γ0 = Γ and Γi+1 = Γi \ Xi :
– the clauses of Γ0 can be deduced from those of Γ using the axiom rule,
– the clauses of Γi+1 can be deduced from those in Γi using the resolution
rule.
Theorem 2.5.8.6 ensures that Γi is satisfiable if and only if Γi+1 is satisfiable, and
thus, by induction, Γ0 is satisfiable if and only if Γn is satisfiable. Moreover,
by theorem 2.5.8.5, we have FV(Γn ) = ∅, thus Γn = ∅ or Γn = {⊥}, and
therefore Γn is unsatisfiable if and only if Γn = {⊥}. Finally, Γ is unsatisfiable
if and only if Γn = {⊥}, i.e. ⊥ can be deduced from Γ using axiom and resolution
rules.

Completeness. Resolution is not complete: given a context Γ, there are clauses

that can be deduced which cannot using resolution only. For instance, from
Γ = X we cannot deduce X ∨ Y using resolution only. However, resolution can
be used in order to decide whether a formula A is a consequence of a context Γ,
in the following way:
Lemma 2.5.8.8. A formula A is a consequence of a context Γ if and only if
Γ ∪ {¬A} is unsatisfiable.
Proof. Given a clausal form Γ, we have Γ ⇒ A equivalent to ¬¬(Γ ⇒ A)
equivalent to ¬(Γ ∧ ¬A), i.e. Γ ∪ {¬A} not satisfiable.
This lemma is the usual way we use resolution.
Example 2.5.8.9. We can show that given
X⇒Y Y ⇒Z X
we can deduce Z. Rewriting those in normal form and using the previous lemma,
this amounts to showing that Γ consisting of
¬X ∨ Y ¬Y ∨ Z X ¬Z
is not satisfiable. Indeed, we have
(ax) (ax)
Γ ` ¬X ∨ Y Γ ` ¬Y ∨ Z
(res) (ax)
Γ ` ¬X ∨ Z Γ`X
(res) (ax)
Γ`Z Γ ` ¬Z
(res)
Γ`⊥
CHAPTER 2. PROPOSITIONAL LOGIC 90

Implementation. We implement clausal forms using lists as in section 2.5.7. Us-

ing this representation, the resolvent of a clausal form Γ (written g) with respect
to a variable X (written x) can be computed using the following function:
let resolve x g =
let gx = List.filter (List.mem (true ,x)) g in
let gx = List.map (List.remove (true ,x)) gx in
let gx' = List.filter (List.mem (false,x)) g in
let gx' = List.map (List.remove (false,x)) gx' in
let g' = List.filter (List.for_all (fun (_,y) -> y <> x)) g in
let disjunction c d =
let union c d =
List.fold_left
(fun d l -> if List.mem l d then d else l::d)
d c
in
if c = [] && d = [] then raise False
else
if List.exists (fun (n,x) -> List.mem (not n,x) d) c then None
else Some (union c d)
in
g'@(List.filter_map_pairs disjunction gx gx')
Here, g’ is Γ′ and gx is ΓX and gx’ is Γ¬X and we return the resolvent computed
following the definition
Γ \ X = Γ′ ∪ {C ∨ D | C ∈ ΓX , D ∈ Γ¬X }
The function List.filter_map_pairs, which is of type
('a -> 'b -> 'c option) -> 'a list -> 'b list -> 'c list
takes a function and two lists as arguments, applies the functions to every pair
of elements of one list and the other, and returns the list of results which are
not None. It is used to compute the clauses C ∨ D in the definition of Γ \ X.
The disjunction is computed by disjunction, with some subtleties. Firstly, as
noted in theorem 2.5.8.4, we should be careful in order to produce formulas in
canonical form:
– a disjunction C ∨ D containing both a literal and its negation should not
be added,
– in a disjunction C ∨ D, if a literal occurs twice (once in C and once D),
we should only keep one instance.
Secondly, since we want to detect as early as possible when ⊥ can be deduced, we
raise an exception False when we find one. We can then see whether a clausal
form Γ is inconsistent by repeatedly eliminating free variables using resolution.
We use the auxiliary function free_var in order to find a free variable (it raises
Not_found if there is none), its implementation being left to the reader. By
theorem 2.5.8.7, if Γ is inconsistent then ⊥ will be produced during the process
(in which case the exception False is raised); otherwise the free variables will
be exhausted (in which case the exception Not_found is raised). This can thus
be computed with the following function:
CHAPTER 2. PROPOSITIONAL LOGIC 91

let rec inconsistent g =

try inconsistent (resolve (free_var g) g)
with
| False -> true
| Not_found -> false
We can then decide whether a clause is a consequence of a set of other clauses
by applying theorem 2.5.8.8:

let prove g c =
inconsistent ((neg c)::g)
As an application, we can prove theorem 2.5.8.9 with
let () =
let g = [
[false,0;true,1];
[false,1;true,2];
[true,0]
] in
let c = [true,2] in
assert (prove g c)

2.5.9 Double-negation translation. We have seen in section 2.3.5 that some

formulas are not provable in intuitionistic logic, whereas they are valid in clas-
sical logic, a typical example being excluded middle ¬A ∨ A. But can we really
prove less in intuitionistic logic than in classical logic? A starting observation
is that, even though ¬A ∨ A is not provable, its double negation ¬¬(¬A ∨ A)
becomes provable, as first seen on page 63:

(ax)
¬(¬A ∨ A), A ` A
(ax) (∨rI )
¬(¬A ∨ A), A ` ¬(¬A ∨ A) ¬(¬A ∨ A), A ` ¬A ∨ A
(¬E )
¬(¬A ∨ A), A ` ⊥
(¬I )
¬(¬A ∨ A) ` ¬A
(ax) (∨lI )
¬(¬A ∨ A) ` ¬(¬A ∨ A) ¬(¬A ∨ A) ` ¬A ∨ A
(¬E )
¬(¬A ∨ A) ` ⊥
(¬I )
` ¬¬(¬A ∨ A)

One of the main ingredients behind this proof is that having ¬(¬A ∨ A) as
hypothesis in a context Γ allows to discard the current proof goal B and go
back to proving ¬A ∨ A:

..
.
(ax)
Γ ⊢ ¬(¬A ∨ A) Γ ⊢ ¬A ∨ A
(¬E )
Γ⊢⊥
(⊥E )
Γ⊢B

How is this better than proving ¬A ∨ A directly? The fact that, during the
proof, we can reset our proof goal to ¬A ∨ A! We thus start by proving ¬A ∨ A
by proving ¬A, which requires proving ⊥ from A. At this point, we change our
CHAPTER 2. PROPOSITIONAL LOGIC 92

mind and start again the proof of ¬A ∨ A, but this time we prove A, which we
can because we gained this information from the previously “aborted” proof.
A more detailed explanation of this kind of behavior was already developed
in section 2.5.2. This actually generalizes to any formula, by a result due to
Glivenko [Gli29]. Given a context Γ, we write ¬¬Γ for the context obtained
from Γ by double-negating every formula.
Theorem 2.5.9.1 (Glivenko’s theorem). Given a context Γ and propositional
formula A, the sequent Γ ⊢ A is provable in classical logic if and only if the
sequent ¬¬Γ ⊢ ¬¬A is provable in intuitionistic logic.
Proof. By induction on A (left as an exercise to the reader).
This result allows us to relate the consistency of classical and intuitionistic
logic in the following way.
Theorem 2.5.9.2. Intuitionistic logic is consistent if and only if classical logic is
consistent.
Proof. Suppose that intuitionistic logic is inconsistent: there is an intuitionistic
proof of ⊥. This proof is also a valid classical proof and thus classical logic is
inconsistent. Conversely, suppose that classical logic is inconsistent. There is
a classical proof of ⊥ and thus, by theorem 2.5.9.1, an intuitionistic proof π of
¬¬⊥. However, the implication ¬¬⊥ ⇒ ⊥ holds intuitionistically:
(ax)
¬¬⊥, ⊥ ⊢ ⊥
(ax) (¬I )
¬¬⊥ ⊢ ¬¬⊥ ¬¬⊥ ⊢ ¬⊥
(¬E )
¬¬⊥ ⊢ ⊥
(⇒I )
⊢ ¬¬⊥ ⇒ ⊥

We thus have an intuitionistic proof of ⊥:

..
. π
⊢ ¬¬⊥ ⇒ ⊥ ⊢ ¬¬⊥
(⇒E )
⊢⊥

and intuitionistic logic is inconsistent.

Remark 2.5.9.3. The theorem 2.5.9.1 does not generalize as is to first-order
logic, but some other translations of classical formulas into intuitionistic logic
do. The most brutal one is due to Kolmogorov and consists in adding ¬¬
in front of every subformula. Interestingly, it corresponds to the call-by-name
continuation-passing style translation of functional programming languages. A
more economical translation is due to Gödel, transforming a formula A into the
formula A∗ defined by induction:

X∗ = X
(A ∧ B)∗ = A∗ ∧ B ∗ (A ∨ B)∗ = ¬(¬A∗ ∧ ¬B ∗ )
⊤∗ = ⊤ ⊥∗ = ⊥
(A ⇒ B)∗ = A∗ ⇒ B ∗ (¬A)∗ = ¬A∗
CHAPTER 2. PROPOSITIONAL LOGIC 93

Finally, one can wonder if, by adding four negations to a formula, we could
gain even more proof power, but this is not the case: the process stabilizes after
the first iteration.
Lemma 2.5.9.4. For every natural number n > 0, we have ¬n+2 A ⇔ ¬n A.
Proof. The implication A ⇒ ¬¬A is intuitionistically provable, as already shown
in theorem 2.2.5.3, as well as the implication ¬¬¬A ⇒ ¬A:
(ax) (ax)
¬¬¬A, A, ¬A ` ¬A ¬¬¬A, A, ¬A ` A
(¬E )
¬¬¬A, A, ¬A ` ⊥
(ax) (¬I )
¬¬¬A, A ` ¬¬¬A ¬¬¬A, A ` ¬¬A
(¬E )
¬¬¬A, A ` ⊥
(¬I )
¬¬¬A ` ¬A
(⇒I )
` ¬¬¬A ⇒ ¬A

We conclude by induction on n.
In particular, ¬¬¬¬A ⇔ ¬¬A, so that we gain nothing by performing the
double-negation translation twice.

2.5.10 Intermediate logics. Once again, classical logic is obtained by adding

the excluded middle ¬A∨A (or any of the equivalent axioms, see theorem 2.5.1.1)
to intuitionistic logic, so that new formulas are provable. A natural question is:
are there intermediate logics between intuitionistic and classical? This means:
can we add axioms to intuitionistic logic so that we get strictly more than intu-
itionistic logic, but strictly less than classical logic? In more details: are there
families of formulas, which are provable classically but not intuitionistically,
such that, by adding those as axioms to intuitionistic logic we obtain a logic in
which some classical formulas are not provable?
The answer is yes. A typical such family of axioms is the weak excluded
middle:
¬¬A ∨ ¬A
Namely, the formula ¬¬X ∨ ¬X is not provable in intuitionistic logic (see theo-
rem 2.3.5.3), so that assuming the weak excluded middle (for every formula A)
allows proving new formulas. However, the formula ¬X ∨ X does not follow
from the weak excluded middle (theorem 2.8.1.4). There are many other possi-
ble families of axioms giving rise to intermediate logics such as
– linearity (or Gödel-Dummett) axiom [God32, Dum59]:

(A ⇒ B) ∨ (B ⇒ A)

– Kreisel-Putnam axiom [KP57]:

(¬A ⇒ (B ∨ C)) ⇒ ((¬A ⇒ B) ∨ (¬A ⇒ C))

– Scott’s axiom [KP57]:

((¬¬A ⇒ A) ⇒ (A ∨ ¬A)) ⇒ (¬¬A ∨ ¬A)

CHAPTER 2. PROPOSITIONAL LOGIC 94

– Smetanich’s axiom [WZ07]:

(¬B ⇒ A) ⇒ (((A ⇒ B) ⇒ A) ⇒ A)

– and many more [DMJ20].

Exercise 2.5.10.1. Show that the above linearity principle
(A ⇒ B) ∨ (B ⇒ A)
is equivalent to the following global choice principle for disjunctions
(A ⇒ B ∨ C) ⇒ (A ⇒ B) ∨ (A ⇒ C)

2.6 Sequent calculus

Natural deduction is “natural” in the sense that it allows for a precise corre-
spondence between logic and computation, see chapter 4. However, it has some
flaws. From an aesthetic point of view, the rules for ∧ and ∨ are not entirely
dual, contrarily to what one would expect: if they were the same, we could think
of reducing the work during proofs or implementations by handling them in the
same way. More annoyingly, proof search is quite difficult. Namely, suppose
that we are trying to prove
A∨B ⊢B∨A
The proof cannot begin with an introduction rule because we have no hope of
filling the dots:
.. ..
. .
A∨B ⊢B A∨B ⊢A
(∨l ) (∨r )
A∨B ⊢B∨A I A∨B ⊢B∨A I
This means that we have to use another rule such as (∨E )
Γ⊢A∨B Γ, A ⊢ C Γ, B ⊢ C
(∨E )
Γ⊢C
which requires us to come up with a formula A∨B which is not directly indicated
in the conclusion Γ ⊢ C and it is not clear how to automatically generate such
formulas. Starting in this way, the proof can be ended as in theorem 2.2.5.2.
In order to overcome this problem, Gentzen has invented sequent calculus,
which is another presentation of logic. In natural deduction, all rules operate on
the formula on the right of ⊢ and there are introduction and elimination rules.
In sequent calculus, there are only introduction rules, but those can operate
either on formulas on the left or on the right of ⊢. This results in a highly
symmetrical calculus.

2.6.1 Sequents. In sequent calculus, sequents are of the form

Γ⊢∆
where Γ and ∆ are contexts: the intuition is that we have the conjunction
of formulas in Γ as hypothesis, from which we can deduce the disjunction of
formulas in ∆.
CHAPTER 2. PROPOSITIONAL LOGIC 95

Γ, B, A, Γ′ ⊢ ∆ Γ ⊢ ∆, B, A, ∆′
(xchL ) (xchR )
Γ, A, B, Γ′ ⊢ ∆ Γ ⊢ ∆, A, B, ∆

Γ, A, A, Γ′ ⊢ ∆ Γ ⊢ ∆, A, A, ∆′
(contrL ) (contrR )
Γ, A, Γ′ ⊢ ∆ Γ ⊢ ∆, A, ∆′

Γ, Γ′ ⊢ ∆ Γ ⊢ ∆, ∆′
(wkL ) (wkR )
Γ, A, Γ′ ⊢ ∆ Γ ⊢ ∆, A, ∆′

Γ, ⊤, Γ′ ⊢ ∆ Γ ⊢ ∆, ⊥, ∆′
(⊤L ) (⊥R )
Γ, Γ′ ⊢ ∆ Γ ⊢ ∆, ∆′

Figure 2.9: Structural rules for sequent calculus

2.6.2 Rules. In all the systems we consider, unless otherwise stated, we always
suppose that we can permute, duplicate and erase formulas in context, i.e. that
the structural rules of figure 2.9 are always present. The additional rules for
sequent calculus are shown in figure 2.10 and the resulting system is called LK.
In sequent calculus, as opposed to natural deduction, the symmetry between
disjunction and conjunction has been restored: except for the axiom and cut, all
rules come in a left and right flavor. Although the presentation is quite different,
the provability power of this system is the same as the one for classical natural
deduction presented in section 2.5:
Theorem 2.6.2.1. A sequent Γ ⊢ ∆ is provable in NK (figure 2.5) if and only if
it is provable in LK (figure 2.10).

Proof. The idea is that, by induction, we can translate a proof in NK into a

proof in LK, and back. The introduction rules in NK correspond to right rules
in LK, the axiom rules match in both systems, the cut rule is admissible in NK
(the proof is similar to the one for NJ in theorem 2.3.2.1), as well as various
structural rules (shown as in section 2.2.7), so that we only have to show that
the elimination rules of NK are admissible in LK and the left rules of LK are
admissible in NK. We only handle the case of conjunction here:
– the rule (∧lE ) is admissible in LK:

..
.
(ax)
Γ ⊢ A ∧ B, ∆ Γ, A, B ⊢ A, ∆
(wkR ) (∧L )
Γ ⊢ A ∧ B, A, ∆ Γ, A ∧ B ⊢ A, ∆
(cut)
Γ ⊢ A, ∆

and admissibility of (∧rE ) is similar,

CHAPTER 2. PROPOSITIONAL LOGIC 96

Γ ⊢ A, ∆ Γ, A ⊢ ∆
(ax) (cut)
Γ, A ⊢ A, ∆ Γ⊢∆

Γ, A, B ⊢ ∆ Γ ⊢ A, ∆ Γ ⊢ B, ∆
(∧L ) (∧R )
Γ, A ∧ B ⊢ ∆ Γ ⊢ A ∧ B, ∆

(⊤R )
Γ ⊢ ⊤, ∆

Γ, A ⊢ ∆ Γ, B ⊢ ∆ Γ ⊢ A, B, ∆
(∨L ) (∨R )
Γ, A ∨ B ⊢ ∆ Γ ⊢ A ∨ B, ∆

(⊥L )
Γ, ⊥ ⊢ ∆

Γ ⊢ A, ∆ Γ, B ⊢ ∆ Γ, A ⊢ B, ∆
(⇒L ) (⇒R )
Γ, A ⇒ B ⊢ ∆ Γ ⊢ A ⇒ B, ∆

Γ ⊢ A, ∆ Γ, A ⊢ ∆
(¬L ) (¬R )
Γ, ¬A ⊢ ∆ Γ ⊢ ¬A, ∆

Figure 2.10: LK: rules of classical sequent calculus.

– the rule (∧L ) is admissible in NK:

..
.
(ax)
Γ, A ∧ B, A ` A ∧ B, ∆ r
Γ, A, B ` ∆
(ax) (∧E ) (wkR )
Γ, A ∧ B ` A ∧ B, ∆ Γ, A ∧ B, A ` B, ∆ Γ, A ∧ B, A, B ` ∆
(∧lE ) (cut)
Γ, A ∧ B ` A, ∆ Γ, A ∧ B, A ` ∆
(cut)
Γ, A ∧ B ` ∆

Other cases are similar.

Remark 2.6.2.2. As noted in [Gir89, chapter 5], the correspondence between
proofs in NK and LK is not bijective. For instance, the two proofs in LK
(ax) (ax) (ax) (ax)
A, B ` A A, B ` B A, B ` A A, B ` B
(∧R ) (∧R )
A, B ` A ∧ B A, B ` A ∧ B
(wkL ) (wkL )
A, B, B 0 ` A ∧ B A, B, B 0 ` A ∧ B
0 0 (wkL ) 0 0 (wkL )
A, A , B, B ` A ∧ B A, A , B, B ` A ∧ B
0 0 (∧L ) 0 0 (∧L )
A, A , B ∧ B ` A ∧ B A ∧ A , B, B ` A ∧ B
0 0 (∧L ) 0 0 (∧L )
A ∧ A ,B ∧ B ` A ∧ B A ∧ A ,B ∧ B ` A ∧ B

get mapped to the same proof in NK.

Mutiplicative presentation. An alternative presentation (called multiplicative pre-

sentation) of the rules is given in figure 2.11: instead of supposing that we have
the same context, we can “merge” the contexts of the premises in the conclusion.
CHAPTER 2. PROPOSITIONAL LOGIC 97

Γ ⊢ A, ∆ Γ ′ , A ⊢ ∆′
(ax) (cut)
A⊢A Γ, Γ ⊢ ∆, ∆′
′

Γ, A, B ⊢ ∆ Γ ⊢ A, ∆ Γ′ ⊢ B, ∆′
(∧L ) (∧R )
Γ, A ∧ B ⊢ ∆ Γ, Γ′ ⊢ A ∧ B, ∆, ∆′

(⊤R )
Γ ⊢ ⊤, ∆

Γ, A ⊢ ∆ Γ ′ , B ⊢ ∆′ Γ ⊢ A, B, ∆
(∨L ) (∨R )
Γ, Γ′ , A ∨ B ⊢ ∆, ∆′ Γ ⊢ A ∨ B, ∆

(⊥L )
Γ, ⊥ ⊢ ∆

Γ ⊢ A, ∆ Γ′ , B ⊢ ∆′ Γ, A ⊢ B, ∆
(⇒L ) (⇒R )
Γ, Γ′ , A ⇒ B ⊢ ∆, ∆′ Γ ⊢ A ⇒ B, ∆

Γ ⊢ A, ∆ Γ, A ⊢ ∆
(¬L ) (¬R )
Γ, ¬A ⊢ ∆ Γ ⊢ ¬A, ∆

Figure 2.11: LK: rules of classical sequent calculus (multiplicative presentation).

Single-sided presentation. By de Morgan laws, in classical logic we can suppose

that only the variables are negated, and negated at most once, see section 2.5.5.
For instance, ¬(X ∨ ¬Y ) is equivalent to ¬X ∧ Y , which satisfies this property.
Given a formula A of this form, we write A∗ for a formula of this form equivalent
to ¬A, which can be defined by induction:

X ∗ = ¬X (¬X)∗ = X
∗ ∗ ∗
(A ∧ B) = A ∨ B (A ∨ B)∗ = A∗ ∧ B ∗
⊤∗ = ⊥ ⊥∗ = ⊤

We omit implication here, since it can be defined as A ⇒ B = A∗ ∨ B. Now, it

can be observed that proving a sequent of the form Γ, A ⊢ ∆ is essentially the
same as proving the sequent Γ ⊢ A∗ , ∆, except that all the rules get replaced
by their opposites:
Lemma 2.6.2.3. A sequent Γ, A ⊢ ∆ is provable in LK if and only if Γ ⊢ A∗ , ∆
is.
For instance the proof on the left below corresponds to the proof on the right:
(ax) (ax)
X ⊢ X, ⊥ X ⊢ X, ⊥
(¬L ) (¬R )
X, ¬X ⊢ ⊥ ⊢ ¬X, X, ⊥
(∧L ) (∨R )
X ∧ ¬X ⊢ ⊥ ⊢ ¬X ∨ X, ⊥

Because of this, we can restrict the system to sequents of the form ⊢ ∆, which
are called single-sided. All the rules preserve single-sidedness except for the
CHAPTER 2. PROPOSITIONAL LOGIC 98

(ax) (ax)
⊢ ∆, A∗ , ∆′ , A, ∆′′ ⊢ ∆, A, ∆′ , A∗ , ∆′′

⊢ ∆, A, ∆′ ⊢ ∆, A∗ , ∆′
(cut)
⊢ ∆, ∆′

⊢ ∆, A, ∆′ ⊢ ∆, B, ∆′ ⊢ ∆, A, B, ∆′
(∧) (∨)
⊢ ∆, A ∧ B, ∆′ ⊢ ∆, A ∨ B, ∆′

⊢ ∆, ∆′
(⊤) (⊥)
⊢ ∆, ⊤, ∆′ ⊢ ∆, ⊥, ∆′

Figure 2.12: LK: single-sided presentation.

axiom rule, which is easily modified in order to satisfy this property. With
some extra care, we can even come up with a presentation which does not
require any structural rules (those are admissible): the resulting presentation of
the calculus is given in figure 2.12. If we do not want to consider only formulas
where only variables can be negated, then the de Morgan laws can be added as
the following explicit rules:

⊢ ¬A ∨ ¬B, ∆ ⊢ ¬A ∧ ¬B, ∆ ⊢ ⊥, ∆ ⊢ ⊤, ∆ ⊢ A, ∆
⊢ ¬(A ∧ B), ∆ ⊢ ¬(A ∨ B), ∆ ⊢ ¬⊤, ∆ ⊢ ¬⊥, ∆ ⊢ ¬¬A, ∆

2.6.3 Intuitionistic rules. In order to obtain a sequent calculus adapted to

intuitionistic logic, one should restrict the two-sided proof system to sequents of
the form Γ ⊢ A, i.e. those where the context on the right of ⊢ contains exactly
one formula. We also have to take variants of rules such as (∨R ), which would
otherwise not maintain the invariant of having one formula on the right. With
little more care, one can write rules which do not require adding structural rules
(they are admissible): the resulting calculus is presented in figure 2.13. Note
that in order for contraction to be admissible one has to keep A ⇒ B in the
context of the left premise. Similarly to theorem 2.6.2.1, one shows:
Theorem 2.6.3.1. A sequent Γ ⊢ A is provable in NJ if and only if it is provable
in LJ.

2.6.4 Cut elimination. By a similar argument as in section 2.3.3, it can be

shown:
Theorem 2.6.4.1. A sequent Γ ⊢ ∆ (resp. Γ ⊢ A) is provable in LK (resp. LJ) if
and only if it admits a proof without using the (cut) rule.

2.6.5 Proof search. From a proof-search point of view, sequent calculus is

much more well-behaved than natural deduction since, with the exception of
the cut rule, we do not have to come up with new formulas when searching for
proofs:
CHAPTER 2. PROPOSITIONAL LOGIC 99

Γ`A Γ, A ` B
0 (ax) (cut)
Γ, A, Γ ` A Γ`B

Γ, A, B, Γ0 ` C Γ`A Γ`B
(∧L ) (∧R )
Γ, A ∧ B, Γ0 ` C Γ`A∧B

(>R )
Γ`>

Γ, A, Γ0 ` C Γ, B, Γ0 ` C Γ`A Γ`B
(∨L ) (∨lL ) (∨rL )
Γ, A ∨ B, Γ0 ` C Γ`A∨B Γ`A∨B

(⊥L )
Γ, ⊥, Γ0 ` A

Γ, A ⇒ B, Γ0 ` A Γ, B, Γ0 ` C Γ, A ` B
0 (⇒L ) (⇒R )
Γ, A ⇒ B, Γ ` C Γ`A⇒B

Γ, ¬A, Γ0 ` A Γ, A ` ⊥
(¬L ) (¬R )
Γ, ¬A, Γ0 ` ⊥ Γ ` ¬A

Figure 2.13: Rules of intuitionistic sequent calculus (LJ).

Proposition 2.6.5.1. LK has the subformula property: apart from the (cut) rule,
all the formulas occurring in the premise of a rule are subformulas of the formulas
occurring in the conclusion.
Since, by theorem 2.6.4.1, we can look for proofs without cuts, this means that
we never have to come up with a new formula during proof search! Moreover,
there is no harm in applying a rule whenever it applies thanks to the following
property:
Proposition 2.6.5.2. In LK, all the rules are reversible.

Implementation. We now implement proof search, which is most simple to do

using the single-sided presentation, see figure 2.12. We describe formulas as
type t =
| Var of bool * string (* false means negated variable *)
| Imp of t * t
| And of t * t
| Or of t * t
| True | False
Using this representation, the negation of a formula can be computed with the
function
let rec neg = function
| Var (n, x) -> Var (not n, x)
| Imp (a, b) -> And (a, neg b)
CHAPTER 2. PROPOSITIONAL LOGIC 100

| And (a, b) -> Or (neg a, neg b)

| Or (a, b) -> And (neg a, neg b)
| True -> False
| False -> True
Finally, the following function implements proof search in LK:
let rec prove venv = function
| [] -> false
| a::env ->
match a with
| Var (n, x) ->
List.mem (Var (not n, x)) venv ||
prove ((Var (n, x))::venv) env
| Imp (a, b) -> prove venv ((neg a)::b::env)
| And (a, b) -> prove venv (a::env) && prove venv (b::env)
| Or (a, b) -> prove venv (a::b::env)
| True -> true
| False -> prove venv env
Since we are considering single sided sequents here, those can be encoded as
lists of terms. The above function takes as argument a sequent Γ′ = venv and
the sequent Γ to be proved. It picks a formula A in Γ and applies the rules of
figure 2.12 on it, until A is split into a list of literals: once this is the case, those
literals are put into the sequent Γ′ (of already handled formulas). Initially, the
context Γ′ is empty, and we usually want to prove one formula A, so that we
can define

let prove a = prove [] [a]

Proof search in intuitionistic logic. Proof search can be performed in LJ, but
the situation is more subtle. First note that, similarly to the situation in LK
(theorem 2.6.5.1), we have
Proposition 2.6.5.3. LJ has the subformula property.
As an immediate consequence, we deduce
Theorem 2.6.5.4. We can decide whether a sequent Γ ⊢ A is provable in LJ or
not.
Proof. There is only a finite number of subformulas of Γ ⊢ A. We can restrict
to sequents where a formula occurs at most 3 times in the context [Gir11,
section 4.2.2] and therefore there is a finite number of possible sequents formed
with those subformulas. By testing all the possible rules, we can determine
which of those are provable, and thus determine whether the initial sequent is
provable.
The previous theorem is constructive, but the resulting algorithm is quite inef-
ficient.
The problem of finding proofs is more delicate than for LK because not all
the rules are reversible: (∨lL ), (∨rL ) and (⇒L ) are not reversible. The rules (∨lL ),
CHAPTER 2. PROPOSITIONAL LOGIC 101

Γ, A, Γ′ ⊢ B X ∈ Γ, Γ′
(⇒X )
Γ, X ⇒ A, Γ′ ⊢ B

Γ, B ⇒ C, Γ′ ⊢ A ⇒ B Γ, C ⊢ D
′ (⇒⇒ )
Γ, (A ⇒ B) ⇒ C, Γ ⊢ D

Γ, A ⇒ (B ⇒ C), Γ′ ⊢ D Γ, A ⇒ C, B ⇒ C, Γ′ ⊢ D
(⇒∧ ) (⇒∨ )
Γ, (A ∧ B) ⇒ C, Γ′ ⊢ D Γ, (A ∨ B) ⇒ C, Γ′ ⊢ D

Γ, A, Γ′ ⊢ B Γ, Γ′ ⊢ B
(⇒⊤ ) (⇒⊥ )
Γ, ⊤ ⇒ A, Γ′ ⊢ B Γ, ⊥ ⇒ A, Γ′ ⊢ B

Figure 2.14: Left implication rules in LJT.

(∨rL ) are easy to handle when performing proof search: when trying to prove a
formula A ∨ B, we either try to prove A or to prove B. The rule (⇒L )
Γ, A ⇒ B, Γ′ ⊢ A Γ, B, Γ′ ⊢ C
(⇒L )
Γ, A ⇒ B, Γ′ ⊢ C
is more difficult to handle. If we apply it naively, it can loop for the same
reasons as in section 2.4.2:
.. ..
. .
(⇒L ) ..
Γ, A ⇒ B ⊢ A Γ, B ⊢ B .
(⇒L )
Γ, A ⇒ B ⊢ A Γ, B ⊢ B
(⇒L )
Γ, A ⇒ B ⊢ A
Although we can detect loops by looking at whether we encounter the same
sequent twice during the proof search, this is quite impractical. Also, since the
rule (⇒L ) is not reversible, the order in which we apply it during proof search
is relevant, and we would like to minimize the number of times we have to
backtrack.
The logic LJT was introduced by Dyckoff in order to overcome this prob-
lem [Dyc92]. It is obtained from LJ by replacing the (⇒L ) rule with the six
rules of figure 2.14, which allow proving sequents of the form
Γ, A ⇒ B, Γ′ ⊢ C
depending on the form of A.
Proposition 2.6.5.5. A sequent is provable in LJ if and only if it is provable
in LJT.
The main interest of this variant is that proof search is always terminating (thus
the T in LJT). Moreover, the rules (⇒∧ ), (⇒∨ ), (⇒⊤ ) and (⇒⊥ ) are reversible
and can thus always be applied during proof search. Many variants of this idea
have been explored, such as the SLJ calculus [GLW99].
A proof search procedure based on this sequent calculus can be implemented
as follows. We describe terms as usual as
CHAPTER 2. PROPOSITIONAL LOGIC 102

type t =
| Var of string
| Imp of t * t
| And of t * t
| Or of t * t
| True | False
The procedure which determines whether a formula is provable is then shown
in figure 2.15. This procedure takes as argument two contexts Γ′ and Γ (respec-
tively called env’ and env) and a formula A. Initially, the context Γ′ is empty;
it will be used to store the formulas of Γ which have already been “processed”.
The procedure first applies all the reversible right rules, then all the reversible
left rules; a formula of Γ which does not give rise to a reversible left rule is put
in Γ′ . Once this is done, the procedure tries to apply the axiom rule, handles
disjunctions by trying to apply either (∨lL ) or (∨rL ), and finally successively tries
all the possible applications of the non-reversible rules (⇒X ) and (⇒⇒ ). Here
the function context_formulas returns, given a context Γ, the list of all the
pairs consisting of a formula A and a context Γ′ , Γ′′ such that Γ = Γ′ , A, Γ′′ ,
i.e. the context Γ where some formula A has been removed.

2.7 Hilbert calculus

The Hilbert calculus is another formalism, due to Hilbert [Hil22], which makes
opposite “design choices” than previous formalisms (natural deduction and se-
quent calculus): it has lots of axioms and very few logical rules.

2.7.1 Proofs. In this formalism, sequents are of the form Γ ⊢ A, with Γ a

context and A a formula, and are deduced according to the following two rules
only:

Γ⊢A⇒B Γ⊢A
′ (ax) (⇒E )
Γ, A, Γ ⊢ A Γ⊢B

respectively called axiom and modus ponens. Of course, there is very little that
we can deduce with only these two rules. The other necessary logical principles
are added in the form of axiom schemes, which can be assumed at any time
during the proofs. In the case of the implicational fragment (implication is the
only connective with which the formulas are built), those are
(K) A ⇒ B ⇒ A,

(S) (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C.
By “axiom schemes”, we mean that the above formulas can be assumed for any
given formulas A, B and C. In other words, this amounts to adding the rules
(K) (S)
Γ⊢A⇒B⇒A Γ ⊢ (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C

A sequent is provable when it is the conclusion of a proof built from the above
rules, and a formula A is provable when the sequent ⊢ A is provable.
CHAPTER 2. PROPOSITIONAL LOGIC 103

let rec prove env' env a =

match a with
| True -> true
| And (a, b) -> prove env' env a && prove env' env b
| Imp (a, b) -> prove env' (a::env) b
| _ -> match env with
| b::env -> (match b with
| And (b, c) -> prove env' (b::c::env) a
| Or (b, c) -> prove env' (b::env) a && prove env' (c::env) a
| True -> prove env' env a
| False -> true
| Imp (And (b, c), d) ->
prove env' ((Imp (b, Imp (c,d)))::env) a
| Imp (Or (b, c), d) ->
prove env' ((Imp (b,d))::(Imp (c,d))::env) a
| Imp (True , b) ->
prove env' (b::env) a
| Imp (False, b) ->
prove env' env a
| Var _ | Imp (Var _, _) | Imp (Imp (_,_),_) ->
prove (b::env') env a
)
| [] ->
match a with
| Var _ when List.mem a env' -> true
| Or (a, b) -> prove env' env a || prove env' env b
| a ->
List.exists
(fun (b, env') ->
match b with
| Imp (Var x, b) when List.mem (Var x) env' ->
prove env' [b] a
| Imp (Imp (b, c), d) ->
prove env' [Imp (c, d)] (Imp (b, c)) && prove env' [d] a
| _ -> false
) (context_formulas env')

let prove a = prove [] [] a

Figure 2.15: Proof search in LJT

CHAPTER 2. PROPOSITIONAL LOGIC 104

Example 2.7.1.1. For any formula A, the formula A ⇒ A is provable:

(S) (K)
` (A ⇒ (B ⇒ A) ⇒ A) ⇒ (A ⇒ B ⇒ A) ⇒ A ⇒ A ` A ⇒ (B ⇒ A) ⇒ A
(⇒E ) (K)
` (A ⇒ B ⇒ A) ⇒ A ⇒ A `A⇒B⇒A
(⇒E )
`A⇒A

Note the complexity compared to NJ or LJ.

None of the rules modify the context Γ, so that people generally omit writing
it. Also, traditionally, instead of using proof trees, a proof of A in the context Γ
is formalized instead as a finite sequence of formulas A1 , . . . , An , with An = A
such that either
– Ai belongs to Γ, or
– Ai is an instance of an axiom, or
– there are indices j, k < i such that Ak = Aj ⇒ Ai , i.e. Ai can be deduced
by
Γ ⊢ Aj ⇒ Ai Γ ⊢ Aj
(⇒E )
Γ ⊢ Ai
This corresponds to describing the proof tree by some traversal of it.
Example 2.7.1.2. The proof theorem 2.7.1.1 is generally written as follows:
1. (A ⇒ (B ⇒ A) ⇒ A) ⇒ (A ⇒ B ⇒ A) ⇒ A ⇒ A by (S)
2. A ⇒ (B ⇒ A) ⇒ A by (K)
3. (A ⇒ B ⇒ A) ⇒ A ⇒ A by modus ponens on 1. and 2.
4. A ⇒ B ⇒ A by (K)
5. A ⇒ A by modus ponens on 3. and 4.

2.7.2 Other connectives. In the case where connectives other than implica-
tion are considered, appropriate axioms should be added:
conjunction: A∧B ⇒A A⇒B ⇒A∧B
A∧B ⇒B

truth: A⇒⊤

disjunction: A ∨ B ⇒ (A ⇒ C) ⇒ (B ⇒ C) ⇒ C A⇒A∨B
B ⇒A∨B

falsity: ⊥⇒A

negation: ¬A ⇒ A ⇒ ⊥ A ⇒ ⊥ ⇒ ¬A
It can be observed that the axioms are in correspondence with elimination
and introduction rules in natural deduction (respectively left and right column
above). The classical variants of the system can be obtained by further adding
one of the axioms from theorem 2.5.1.1.
CHAPTER 2. PROPOSITIONAL LOGIC 105

2.7.3 Relationship with natural deduction. In order to show that proofs

in Hilbert calculus correspond to proofs in natural deduction, we first need to
study some of its properties. The usual structural rules are admissible in this
system:
Proposition 2.7.3.1. The rules of exchange, contraction, truth strengthening and
weakening are admissible in Hilbert calculus:

Γ, A, B, Γ′ ⊢ C Γ, A, A ⊢ C Γ, ⊤ ⊢ A Γ⊢C
Γ, B, A, Γ′ ⊢ C Γ, A ⊢ C Γ⊢A Γ, A ⊢ C

Proof. By induction on the proof of the premise.

The introduction rule for implication is also admissible. This is sometimes called
the deduction theorem and is due to Herbrand.
Proposition 2.7.3.2. The introduction rule for implication is admissible:

Γ, A, Γ′ ⊢ B
(⇒I )
Γ, Γ′ ⊢ A ⇒ B

Proof. By induction on the proof of Γ, A, Γ′ ⊢ B.

– If it is of the form
(ax)
Γ, A, Γ′ ⊢ A
then we can show ⊢ A ⇒ A by theorem 2.7.1.1 and thus Γ, Γ′ ⊢ A ⇒ A
by weakening.
– If it is of the form
(ax)
Γ, A, Γ′ ⊢ B
with B different from A which belongs to Γ or Γ′ , then we can show
B ⊢ A ⇒ B by
(K) (ax)
B⊢B⇒A⇒B B⊢B
(⇒E )
B⊢A⇒B

and thus Γ, Γ′ ⊢ A ⇒ B by weakening.

– If it is of the form
Γ, A, Γ′ ⊢ C Γ, A, Γ′ ⊢ C ⇒ B
(⇒E )
Γ, A, Γ′ ⊢ B

then, by induction hypothesis, we have proofs of Γ, Γ′ ⊢ A ⇒ C and of

Γ, Γ′ ⊢ A ⇒ C ⇒ B and the derivation
..
.
(S) ..
Γ, Γ0 ` (A ⇒ C ⇒ B) ⇒ (A ⇒ C) ⇒ A ⇒ B Γ, Γ0 ` A ⇒ C ⇒ B .
(⇒E )
Γ, Γ0 ` (A ⇒ C) ⇒ A ⇒ B 0
Γ, Γ ` A ⇒ C
(⇒E )
Γ, Γ0 ` A ⇒ B

allows us to conclude.
CHAPTER 2. PROPOSITIONAL LOGIC 106

We can thus show that provability in this system is the usual one.
Theorem 2.7.3.3. A sequent Γ ⊢ A is provable in Hilbert calculus if and only if
it is provable in natural deduction.

Proof. For simplicity, we restrict to the case of the implicational fragment. In

order to show that a proof in the Hilbert calculus induces a proof in NJ, we
should show that the rules (ax) and (⇒E ) are admissible in NJ (this is the case
by definition) and that the axioms (S) and (K) can be derived in NJ, which is
easy:
(ax) (ax) (ax) (ax)
A ⇒ B ⇒ C, A ⇒ B, A ` A ⇒ B ⇒ C A ⇒ B ⇒ C, A ⇒ B, A ` A A ⇒ B ⇒ C, A ⇒ B, A ` A ⇒ B A ⇒ B ⇒ C, A ⇒ B, A ` A
(⇒E ) (⇒E )
A ⇒ B ⇒ C, A ⇒ B, A ` B ⇒ C A ⇒ B ⇒ C, A ⇒ B, A ` B
(⇒E )
A ⇒ B ⇒ C, A ⇒ B, A ` C
(⇒I )
A ⇒ B ⇒ C, A ⇒ B ` A ⇒ C
(⇒I )
A ⇒ B ⇒ C ` (A ⇒ B) ⇒ A ⇒ C
(⇒I )
` (A ⇒ B ⇒ C) ⇒ (A ⇒ B) ⇒ A ⇒ C

(this is deliberately too small to read, you should prove this by yourself) and

(ax)
A, B ⊢ A
(⇒I )
A⊢B⇒A
(⇒I )
⊢A⇒B⇒A

Conversely, in order to show that a proof in NJ induces one in Hilbert cal-

culus, we should show that the rules (ax), (⇒E ) and (⇒I ) are admissible in
Hilbert calculus: the first two are by definition, and the third one was proved
in theorem 2.7.3.2.

2.8 Kripke semantics

We have seen in section 2.5.6 that the usual boolean interpretation of formulas is
correct and complete, meaning that a formula is classically provable if and only if
it is valid in every boolean model. One can wonder if there is an analogous notion
of model for proofs in intuitionistic logic – and this is indeed the case: Kripke
models are correct and complete for intuitionistic logic. They were discovered
in the 1960s by Kripke [Kri65] and Joyal for modal logic, and can be thought
of as a semantics of possible worlds evolving through time: as time progresses
more propositions may become true. The moral is thus that intuitionistic logic
is a logic where the notion of truth is “local”, unlike classical logic.

2.8.1 Kripke structures. A Kripke structure (W, ⩽, ρ) consists of a partially

ordered set (W, ⩽) of worlds together with a valuation ρ : W × X → B which
indicates whether in a given world a given propositional variable is true or not.
The valuation is always assumed to be monotonous, i.e. to satisfy ρ(w, X) = 1
implies ρ(w′ , X) = 1 for every worlds such that w ⩽ w′ . We sometimes simply
write W for a Kripke structure (W, ⩽, ρ).
Given a Kripke structure W and a world w ∈ W , we write w ⊨W A (or
simply w ⊨ A when W is clear from the context) when a formula A is satisfied
CHAPTER 2. PROPOSITIONAL LOGIC 107

in w. This relation is defined by induction on A:

w ⊨X iff ρ(w, X)
w ⊨⊤ holds
w ⊨⊥ does not hold
w ⊨A∧B iff w ⊨ A and w ⊨ B
w ⊨A∨B iff w ⊨ A or w ⊨ B
w ⊨A⇒B iff, for every w′ ⩾ w, w′ ⊨ A implies w′ ⊨ B
w ⊨ ¬A iff, for every w′ ⩾ w, w′ ⊨ A does not hold

A Kripke structure is often pictured as a graph whose vertices correspond to

worlds, an edge from w to w′ indicating that w ⩽ w′ , with the variables X
such that ρ(w, X) = 1 being written next to the node w, see theorems 2.8.1.4
and 2.8.1.5.
We can think of a Kripke structure as describing the evolution of a world
through time: given two worlds such that w ⩽ w′ , we think of w′ as being a
possible future for w. Since the order is not necessarily total, a given world
might have different possible futures. In each world, the valuation indicates
which formulas we know are true, and the monotonicity condition ensures that
our knowledge can only grow: if we know that a formula is true then we will
still know it in the future.
Lemma 2.8.1.1. Satisfaction is monotonic: given a formula A, a Kripke structure
W and a world w, if w ⊨ A then w′ ⊨ A for every world w′ ⩾ w.

Proof. By induction on the formula A.

Given a context Γ = A1 , . . . , An , a formula A, and a Kripke structure W , we
write Γ ⊨W A when, for every world w ∈ W in which all the formulas Ai are
satisfied, the formula A is also satisfied. We write Γ ⊨ A when Γ ⊨W A holds
for every structure W : in this case, we say that A is valid in the context Γ.
Remark 2.8.1.2. It should be observed that the notion of Kripke structure gen-
eralizes the notion of boolean model recalled in section 2.5.6. Namely, a boolean
valuation ρ : X → B can be seen as a Kripke structure W with a single world w,
the valuation being given by ρ. The notion of validity for Kripke structures
defined above then coincides with the one for boolean models.
A following theorem ensures that Kripke semantics are sound: a provable
formula is valid.
Theorem 2.8.1.3 (Soundness). If a sequent Γ ⊢ A is derivable in intuitionistic
logic then Γ ⊨ A.
Proof. By induction on the proof of Γ ⊢ A.

The contrapositive of this theorem says that if we can find a Kripke structure
in which there is a world where a formula A is not satisfied, then A is not
intuitionistically provable. This thus provides an alternative to methods based
on cut-elimination (see section 2.3.5) in order to establish the non-provability
of formulas.
CHAPTER 2. PROPOSITIONAL LOGIC 108

Example 2.8.1.4. Consider the formula expressing double negation elimination

¬¬X ⇒ X and the Kripke structure with W = {w0 , w1 }, with w0 ⩽ w1 , and
ρ(w0 , X) = 0 and ρ(w1 , X) = 1, which can be pictured as

X
· ·
w0 w1

We have w0 ⊭ ¬X (because there is the future world w1 in which X holds) and

w1 ⊭ ¬X, and thus w0 ⊨ ¬¬X (in fact, it can be shown that w ⊨ ¬¬X in an
arbitrary structure iff for every world w′ ⩾ w there exists a world w′′ ⩾ w′ such
that w′′ ⊨ X). Moreover, we have w0 ⊭ X, and thus w0 ⊭ ¬¬X ⇒ X. This
shows that ¬¬X ⇒ X is not intuitionistically provable. In the same Kripke
structure, we have w0 ⊭ ¬X ∨ X and thus the excluded middle ¬X ∨ X is not
intuitionistically provable either.
Given an arbitrary formula A, by theorem 2.8.1.1, in this structure, this
formula is either satisfied both in w0 and w1 , or only in w1 or in no world:

A A A
· · · · · ·
w0 w1 w0 w1 w0 w1

In the two first cases, ¬¬A is satisfied and in the last one ¬A is satisfied.
Therefore, the weak excluded middle ¬¬A ∨ ¬A is always satisfied: this shows
that the weak excluded middle does not imply the excluded middle. By using a
similar reasoning, it can be shown that the linearity axiom (A ⇒ B) ∨ (B ⇒ A)
does not imply the excluded middle. Both thus give rise to intermediate logics,
see section 2.5.10.
Example 2.8.1.5. The Kripke structure

X Y
· · ·

shows that the linearity formula (X ⇒ Y ) ∨ (Y ⇒ X) is not intuitionistically

provable (whereas classically it is).

2.8.2 Completeness. We now consider the converse of the theorem 2.8.1.3.

We will show that if a formula is valid then it is provable intuitionistically. Or
equivalently, that if a formula is not provable, then we can always exhibit a
Kripke structure in which it does not hold.
Given a possibly infinite set Φ of formulas, we write Φ ⊢ A whenever there
exists a finite subset Γ ⊆ Φ such that Γ ⊢ A is intuitionistically provable. Such
a set is consistent if Φ ⊬ ⊥. By theorem 2.3.4.1, we have:
Lemma 2.8.2.1. A set Φ of formulas is consistent if and only if there is a for-
mula A such that Φ ⊬ A.
A set Φ of formulas is disjunctive if Φ ⊢ A ∨ B implies Φ ⊢ A or Φ ⊢ B.
Lemma 2.8.2.2. Given a set Φ of formulas and a formula A such that Φ ⊬ A,
there exists a disjunctive set Φ such that Φ ⊆ Φ and Φ ⊬ A.
Proof. Suppose fixed an enumeration of all the formulas of the form B ∨ C
occurring in Φ. We construct by induction a sequence Φn of sets of formulas
which are such that Φn ⊬ A. We set Φ0 = Φ. Suppose Φn constructed and
consider the n-th formula B ∨ C in Φ:
CHAPTER 2. PROPOSITIONAL LOGIC 109

– if Φn , B ⊬ A, we define Φn+1 = Φn ∪ {B},

– if Φn , B ⊢ A, we define Φn+1 = Φn ∪ {C}.

In the first case, it is obvious that Φn+1 ⊬ A. In the second one, we have
Φn ⊢ B ∨ C and Φn , B ⊢ A, if we also had Φn , C ⊢ A then, by (∨E ), we would
S Φn ⊢ A, which is excluded by induction hypothesis. Finally, we take
also have
Φ = n∈N Φn .
A set Φ of formulas is saturated if, for every formula A, Φ ⊢ A implies A ∈ Φ.
Lemma 2.8.2.3. Given a set Φ of formulas, the set Φ = {A | Φ ⊢ A} is saturated.
A set is complete if it is consistent, disjunctive and saturated. Combining the
above lemmas we obtain,
Lemma 2.8.2.4. Given a set Φ of formulas and a formula A such that Φ ⊭ A,
there exists a complete set Φ such that Φ ⊆ Φ and A ̸∈ Φ.

Proof. By theorem 2.8.2.2, there exists a disjunctive set of formulas Φ such that
Φ ⊆ Φ and Φ ⊬ A. This set of consistent by theorem 2.8.2.1. Moreover, by
theorem 2.8.2.3, we can suppose that this set is saturated (the construction is
easily checked to preserve consistency and disjunctiveness) and such that A ̸∈ Φ.

The universal Kripke structure W is defined by

W = {wΦ | Φ is complete}

with wΦ ⩽ wΦ′ whenever Φ ⊆ Φ′ , and ρ(wΦ , X) = 1 iff X ∈ Φ.

Lemma 2.8.2.5. Let Φ be a complete set and A a formula. Then wΦ ⊨ A iff
A ∈ Φ.
Proof. By induction on the formula A.
– If A = X is a propositional variable, we have wΦ ⊨ X iff ρ(wΦ , X) = 1 iff
X ∈ Φ.

– If A = ⊤, we always have wΦ ⊨ ⊤ and we always have ⊤ ∈ Φ because

Φ ⊢ ⊤ by (⊤I ) and Φ is saturated.
– If A = ⊥, we never have wΦ ⊨ ⊥ and we never have ⊥ ∈ Φ because Φ is
consistent.

– If A = B ∧ C.
Suppose that wΦ ⊨ B ∧ C. Then wΦ ⊨ B and wΦ ⊨ C, and therefore
Φ ⊢ B and Φ ⊢ C by induction hypothesis. We deduce Φ ⊢ B ∧ C by (∧I )
and weakening and thus B ∧ C ∈ Φ by saturation.
Conversely, suppose B∧C ∈ Φ and thus Φ ⊢ B∧C. This entails Φ ⊢ B and
Φ ⊢ C by (∧lE ) and (∧rE ), and thus B ∈ Φ and C ∈ Φ by saturation. By
induction hypothesis, we have wΦ ⊨ B and wΦ ⊨ C, and thus wΦ ⊨ B ∧ C.
CHAPTER 2. PROPOSITIONAL LOGIC 110

– If A = B ∨ C.
Suppose that wΦ ⊨ B ∨ C. Then wΦ ⊨ B or wΦ ⊨ C, and therefore Φ ⊢ B
or Φ ⊢ C by induction hypothesis. We deduce Φ ⊢ B ∨ C by (∨lI ) or (∨rI )
and thus B ∨ C ∈ Φ by saturation.
Conversely, suppose B ∨ C ∈ Φ. Since Φ is disjunctive, we have B ∈ Φ or
C ∈ Φ. By induction hypothesis, we have wΦ ⊨ B or wΦ ⊨ C, and thus
wΦ ⊨ B ∨ C.
– If A = B ⇒ C.
Suppose that wΦ ⊨ B ⇒ C. Our goal is to show B ⇒ C ∈ Φ. By (⇒I )
and saturation, it is enough to show Φ, B ⊢ C. Suppose that it is not
the case. By theorem 2.8.2.4, we can construct a complete set Φ′ with
Φ ⊆ Φ′ , B ∈ Φ′ and C ̸∈ Φ′ .