Book contents
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Basic proof theory
Published online by Cambridge University Press: 05 November 2011
- Frontmatter
- Contents
- Preface
- Programme of lectures
- Basic proof theory
- A short course in ordinal analysis
- Proofs as Programs
- A simplified version of local predicativity
- A note on bootstrapping intuitionistic bounded arithmetic
- Termination orderings and complexity characterisations
- Logics for termination and correctness of functional programs, II. Logics of strength PRA
- Reflecting the semantics of reflected proof
- Fragments of Kripke-Platek set theory with infinity
- Provable computable selection functions on abstract structures
Summary
Introduction
This paper is an amalgam of two introductory lecture courses given at the Summer School. As the title suggests, the aim is to present fundamental notions of Proof Theory in their simplest settings, thus: Completeness and Cut-Elimination in Pure Predicate Logic; the Curry-Howard Correspondence and Normalization in the core part of Natural Deduction; connections to Sequent Calculus and Linear Logic; and applications to the Σ1-Inductive fragment of arithmetic and the synthesis of primitive recursive bounding functions. The authors have tried to preserve a (readable) balance between rigour and informal lecture-note style.
Pure Predicate Logic—Completeness
Classical first order predicate calculus (PC) is formulated here essentially in “Schütte-Ackermann-Tait” style, but with multisets instead of sets of formulas for sequents. It is kept “pure” (i.e., no function symbols) merely for the sake of technical simplicity. The refinement to multiset sequents illuminates the rôle of the so-called structural inferences of contraction and weakening in proof-theoretic arguments.
The language of PC. The language consists of
Individual variables: x0, x1, x2, …;
Predicate symbols: P0, P0, P1, P1, … occurring in complementary pairs;
Logical symbols: V (or), Λ (and), Ǝ (some), ∀ (all);
Brackets for unique readability.
- Type
- Chapter
- Information
- Proof TheoryA selection of papers from the Leeds Proof Theory Programme 1990, pp. 1 - 26Publisher: Cambridge University PressPrint publication year: 1993
- 1
- Cited by