The Curry-Howard isomorphism states an amazing correspondence between systems of formal logic as encountered in proof theory and computational calculi as found in type theory. For instance,minimal propositional logic corresponds to simply typed lambda-calculus, first-order logic corresponds to dependent types, second-order logic corresponds to polymorphic types, sequent calculus is related to explicit substitution, etc.The isomorphism has many aspects, even at the syntactic level:formulas correspond to types, proofs correspond to terms, provability corresponds to inhabitation, proof normalization corresponds to term reduction, etc.But there is more to the isomorphism than this. For instance, it is an old idea---due to Brouwer, Kolmogorov, and Heyting---that a constructive proof of an implication is a procedure that transformsproofs of the antecedent into proofs of the succedent; the Curry-Howard isomorphism gives syntactic representations of such procedures. The Curry-Howard isomorphism also provides theoretical foundations for many modern proof-assistant systems (e.g. Coq).This book give an introduction to parts of proof theory and related aspects of type theory relevant for the Curry-Howard isomorphism. It can serve as an introduction to any or both of typed lambda-calculus and intuitionistic logic.Key features - The Curry-Howard Isomorphism treated as common theme - Reader-friendly introduction to two complementary subjects: Lambda-calculus and constructive logics - Thorough study of the connection between calculi and logics - Elaborate study of classical logics and control operators - Account of dialogue games for classical and intuitionistic logic - Theoretical foundations of computer-assisted reasoning · The Curry-Howard Isomorphism treated as the common theme.· Reader-friendly introduction to two complementary subjects: lambda-calculus and constructive logics · Thorough study of the connection between calculi and logics.· Elaborate study of classical logics and control operators.· Account of dialogue games for classical and intuitionistic logic.· Theoretical foundations of computer-assisted reasoning
Author(s): Morten Heine Sørensen M.Sc Ph.D, Pawel Urzyczyn prof. dr hab.
Series: Studies in Logic and the Foundations of Mathematics 149
Edition: 1
Publisher: Elsevier Science
Year: 2006
Language: English
Pages: 456
Preface......Page 5
Contents......Page 11
1.1 A gentle introduction......Page 15
1.2 Pre-terms and λ-terms......Page 17
1.3 Reduction......Page 24
1.4 The Church-Rosser theorem......Page 26
1.5 Leftmost reductions are normalizing......Page 28
1.6 Perpetual reductions and the conservation theorem......Page 32
1.7 Expressibility and undeeidability......Page 33
1.8 Notes......Page 36
1.9 Exercises......Page 37
2. Intultionistic logic......Page 41
2.1 The BHK interpretation......Page 42
2.2 Natural deduction......Page 46
2.3 Algebraic semantics of classical logic......Page 48
2.4 Heyting algebras......Page 51
2.5 Kripke semantics......Page 57
2.6 The implicational fragment......Page 61
2.7 Notes......Page 62
2.8 Exercises......Page 64
3. Simply typed λ-calcuIus......Page 69
3.1 Simply typed λ-calculus a la Curry......Page 70
3.2 Type reconstruction algorithm......Page 74
3.3 Simply typed λ-calculus a la Church......Page 77
3.4 Church versus Curry typing......Page 79
3.5 Normalization......Page 81
3.6 Church-Rosser property......Page 84
3.7 Expressibility......Page 86
3.8 Notes......Page 87
3.9 Exercises......Page 88
4.1 Proofs and terms......Page 91
4.2 Type inhabitation......Page 93
4.3 Not an exact isomorphism......Page 95
4.4 Proof normalization......Page 97
4.5 Sums and products......Page 100
4.6 Prover-skeptic dialogues......Page 103
4.7 Prover-skeptic dialogues with absurdity......Page 108
4.8 Notes......Page 110
4.9 Exercises......Page 114
5.1 Hilbert style proofs......Page 117
5.2 Combinatory logic......Page 122
5.3 Typed combinators......Page 124
5.4 Combinators versus lambda terms......Page 127
5.5 Extensionality......Page 130
5.6 Relevance and linearity......Page 132
5.7 Notes......Page 136
5.8 Exercises......Page 137
6.1 Classical prepositional lope......Page 141
6.2 The λμ-calculus......Page 146
6.3 Subject reduction, confluence, strong normalization......Page 151
6.4 Logical embedding and CPS translation......Page 154
6.5 Classical prover-skeptic dialogues......Page 158
6.6 The pure implicational fragment......Page 164
6.7 Conjunction and disjunction......Page 167
6.8 Notes......Page 170
6.9 Exercises......Page 171
7. Sequent calculus......Page 175
7.1 Gentzen's sequent calculus LK......Page 176
7.2 Fragments of LK versus natural deduction......Page 179
7.3 Gentzen's Hauptsatz......Page 183
7.4 Cut elimination versus normalization......Page 188
7.5 Lorenzen dialogues......Page 195
7.6 Notes......Page 203
7.7 Exercises......Page 205
8.1 Syntax of first-order logic......Page 209
8.2 Informal semantics......Page 211
8.3 Proof systems......Page 214
8.4 Classical semantics......Page 219
8.5 Algebraic semantics of intuitionistie logic......Page 221
8.6 Kripke semantics......Page 226
8.7 λ-calculus......Page 233
8.8 Undecidability......Page 235
8.9 Notes......Page 238
8.10 Exercises......Page 239
9.1 The language of arithmetic......Page 243
9.2 Peano Arithmetic......Page 246
9.3 Godel's theorems......Page 248
9.4 Representable and provably recursive functions......Page 251
9.5 Heyting Arithmetic......Page 254
9.6 Kleene's realizability interpretation......Page 257
9.7 Notes......Page 259
9.8 Exercises......Page 261
10.1 From Heyting Arithmetic to system T......Page 265
10.2 Syntax......Page 267
10.3 Strong normalization......Page 270
10.4 Modified realizability......Page 274
10.5 Notes......Page 279
10.6 Exercises......Page 280
11.Second-order logic and polymorphism......Page 283
11.1 Prepositional second-order logic......Page 284
11.2 Polymorphic λ-calculus (system F)......Page 290
11.3 Expressive power......Page 294
11.4 Curry-style polymorphism......Page 298
11.5 Strong normalization......Page 301
11.6 The inhabitation problem......Page 304
11.7 Higher-order polymorphism......Page 310
11.8 Notes......Page 313
11.9 Exercises......Page 314
12.1 Second-order syntax......Page 317
12.2 Classical second-order logic......Page 319
12.3 Intuitionistic second-order logic......Page 322
12.4 Second-order Peano Arithmetic......Page 325
12.5 Second-order Heyting Arithmetic......Page 328
12.6 Simplified syntax......Page 329
12.7 λ-calculus......Page 332
12.9 Exercises......Page 337
13. Dependent types......Page 339
13.1 The language of λP......Page 340
13.2 Type assignment......Page 342
13.3 Strong normalization......Page 347
13.4 Dependent types a la Curry......Page 349
13.5 Correspondence with first-order logic......Page 351
13.6 Notes......Page 353
13.7 Exercises......Page 354
14.1 System λP revisited......Page 357
14.2 Pure type systems......Page 358
14.3 The Calculus of Constructions......Page 360
14.4 Strong normalization......Page 362
14.5 Beyond the cube......Page 365
14.6 Girard's paradox......Page 366
14.7 Notes......Page 371
14.8 Exercises......Page 372
A.1 Set theory......Page 375
A.2 Algebra and unification......Page 379
A.3 Partial recursive functions......Page 380
A.4 Decision problems......Page 382
A.5 Hard and complete......Page 384
Appendix B: Solutions and hints to selected exercises......Page 387
Bibliography......Page 417
Index......Page 445
