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, Paweł Urzyczyn
Series: Studies in Logic and the Foundations of Mathematics 149
Publisher: Elsevier Science
Year: 2006
Language: English
Commentary: all letters are surrounded by dots
Pages: 458
Cover......Page 1
Title page......Page 5
Preface......Page 7
Contents......Page 13
1.1 A gentle introduction......Page 17
1.2 Pre-terms and λ-terms......Page 19
1.3 Reduction......Page 26
1.4 The Church-Rosser theorem......Page 28
1.5 Leftmost reductions are normalizing......Page 30
1.6 Perpetual reductions and the conservation theorem......Page 34
1.7 Expressibility and undecidability......Page 35
1.8 Notes......Page 38
1.9 Exercises......Page 39
2 Intuitionistic logic......Page 43
2.1 The BHK interpretation......Page 44
2.2 Natural deduction......Page 48
2.3 Algebraic semantics of classical logic......Page 50
2.4 Heyting algebras......Page 53
2.5 Kripke semantics......Page 59
2.6 The implicational fragment......Page 63
2.7 Notes......Page 64
2.8 Exercises......Page 66
3 Simply typed λ-calcuIus......Page 71
3.1 Simply typed λ-calculus à la Curry......Page 72
3.2 Type reconstruction algorithm......Page 76
3.3 Simply typed λ-calculus à la Church......Page 79
3.4 Church versus Curry typing......Page 81
3.5 Normalization......Page 83
3.6 Church-Rosser property......Page 86
3.7 Expressibility......Page 88
3.8 Notes......Page 89
3.9 Exercises......Page 90
4.1 Proofs and terms......Page 93
4.2 Type inhabitation......Page 95
4.3 Not an exact isomorphism......Page 97
4.4 Proof normalization......Page 99
4.5 Sums and products......Page 102
4.6 Prover-skeptic dialogues......Page 105
4.7 Prover-skeptic dialogues with absurdity......Page 110
4.8 Notes......Page 112
4.9 Exercises......Page 116
5.1 Hilbert style proofs......Page 119
5.2 Combinatory logic......Page 124
5.3 Typed combinators......Page 126
5.4 Combinators versus lambda terms......Page 129
5.5 Extensionality......Page 132
5.6 Relevance and linearity......Page 134
5.7 Notes......Page 138
5.8 Exercises......Page 139
6.1 Classical propositional logic......Page 143
6.2 The λμ-calculus......Page 148
6.3 Subject reduction, confluence, strong normalization......Page 153
6.4 Logical embedding and CPS translation......Page 156
6.5 Classical prover-skeptic dialogues......Page 160
6.6 The pure implicational fragment......Page 166
6.7 Conjunction and disjunction......Page 169
6.8 Notes......Page 172
6.9 Exercises......Page 173
7 Sequent calculus......Page 177
7.1 Gentzen's sequent calculus LK......Page 178
7.2 Fragments of LK versus natural deduction......Page 181
7.3 Gentzen's Hauptsatz......Page 185
7.4 Cut elimination versus normalization......Page 190
7.5 Lorenzen dialogues......Page 197
7.6 Notes......Page 205
7.7 Exercises......Page 207
8.1 Syntax of first-order logic......Page 211
8.2 Informal semantics......Page 213
8.3 Proof systems......Page 216
8.4 Classical semantics......Page 221
8.5 Algebraic semantics of intuitionistic logic......Page 223
8.6 Kripke semantics......Page 228
8.7 Lambda-calculus......Page 231
8.8 Undecidability......Page 237
8.9 Notes......Page 240
8.10 Exercises......Page 241
9.1 The language of arithmetic......Page 245
9.2 Peano Arithmetic......Page 248
9.3 Gödel's theorems......Page 250
9.4 Representable and provably recursive functions......Page 253
9.5 Heyting Arithmetic......Page 256
9.6 Kleene's realizability interpretation......Page 259
9.7 Notes......Page 261
9.8 Exercises......Page 263
10.1 From Heyting Arithmetic to system T......Page 267
10.2 Syntax......Page 269
10.3 Strong normalization......Page 272
10.4 Modified realizability......Page 276
10.5 Notes......Page 281
10.6 Exercises......Page 282
11 Second-order logic and polymorphism......Page 285
11.1 Propositional second-order logic......Page 286
11.2 Polymorphic lambda-calculus (system F)......Page 292
11.3 Expressive power......Page 296
11.4 Curry-style polymorphism......Page 300
11.5 Strong normalization......Page 303
11.6 The inhabitation problem......Page 306
11.7 Higher-order polymorphism......Page 312
11.8 Notes......Page 315
11.9 Exercises......Page 316
12.1 Second-order syntax......Page 319
12.2 Classical second-order logic......Page 321
12.3 Intuitionistic second-order logic......Page 324
12.4 Second-order Peano Arithmetic......Page 327
12.5 Second-order Heyting Arithmetic......Page 330
12.6 Simplified syntax......Page 331
12.7 Lambda-calculus......Page 334
12.9 Exercises......Page 339
13 Dependent types......Page 341
13.1 The language of λP......Page 342
13.2 Type assignment......Page 344
13.3 Strong normalization......Page 349
13.4 Dependent types à la Curry......Page 351
13.5 Correspondence with first-order logic......Page 353
13.6 Notes......Page 355
13.7 Exercises......Page 356
14.1 System λP revisited......Page 359
14.2 Pure type systems......Page 360
14.3 The Calculus of Constructions......Page 362
14.4 Strong normalization......Page 364
14.5 Beyond the cube......Page 367
14.6 Girard's paradox......Page 368
14.7 Notes......Page 373
14.8 Exercises......Page 374
A.1 Set theory......Page 377
A.2 Algebra and unification......Page 381
A.3 Partial recursive functions......Page 382
A.4 Decision problems......Page 384
A.5 Hard and complete......Page 386
Solutions to Chapter 1......Page 389
Solutions to Chapter 2......Page 391
Solutions to Chapter 3......Page 396
Solutions to Chapter 4......Page 398
Solutions to Chapter 5......Page 400
Solutions to Chapter 6......Page 402
Solutions to Chapter 7......Page 403
Solutions to Chapter 8......Page 405
Solutions to Chapter 9......Page 409
Solutions to Chapter 10......Page 410
Solutions to Chapter 11......Page 411
Solutions to Chapter 12......Page 416
Solutions to Chapter 14......Page 417
A......Page 419
B......Page 420
C......Page 422
D......Page 424
F......Page 426
G......Page 427
H......Page 430
K......Page 432
L......Page 434
M......Page 436
O......Page 438
P......Page 439
R......Page 440
S......Page 441
T......Page 444
W......Page 445
Z......Page 446
B......Page 447
C......Page 448
E......Page 449
G......Page 450
K......Page 451
M......Page 452
P......Page 453
R......Page 454
S......Page 455
T......Page 456
V......Page 457
Z......Page 458
