Three-valued logic and cut-elimination: The actual meaning of Takeuti's conjecture

J. Y. Girard

GDML_Books, (1976), p.

Résumé

CONTENTSIntroduction............................................................................................................ 5A. The three-valued predicate calculus............................................................ 8 A 1. Three-valued structures; classical case............................................. 8 A 2. Three-valued structures; intuitionistic case........................................ 10 A 3. Theories; models..................................................................................... 12 A 4. The completeness theorem.................................................................. 14 A 5. The thinness theorem............................................................................. 18B. Three-valued analysis and cut elimination......................................................... 19 B 1. The syntax................................................................................................. 19 B 2. The semantics......................................................................................... 22 B 3. Cut-free provability................................................................................... 23 B 4. Takeuti’s conjecture................................................................................ 28C. Applications to the metamathematics of cut-free analysis.............................. 30 C 1. Poor and absorbing formulas............................................................... 31 C 2. A candidate for synonymity.................................................................... 32 C 3. Syntactic conditions for poverty............................................................. 35 C 4. Takeuti’s conjectures and $∑^0_1$-reflection.................................. 36 C 5. Cut elimination in the classical case.................................................. 37 C 6. The poverty theorem............................................................................... 39Appendix......................................................................................................................... 41 1. Tait’s proof.................................................................................................... 41 2. Prawitz’s proof.............................................................................................. 42 3. Prawitz’s third proof..................................................................................... 43 4. The co-rule.................................................................................................... 43 5. The simple theory of types......................................................................... 44 References............................................................................................... 45

Détail

Zbl 0357.02027

EUDML-ID : urn:eudml:doc:268582