Lectures on the Curry-Howard Isomorphism (Volume 149) (Studies in Logic and the Foundations of Mathematics, Volume 149)

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 transforms proofs 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 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 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 transforms proofs 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