Home Philosophy Advances in Proof-Theoretic Semantics

## Concluding Remarks and Further ApplicationsLooking at the single detour conversion schemes in the proof of Theorem 1, we notice that simplification convertibility with disjunction in case 2.2 leaves two possible results of conversion. For the rest of detour conversions, the local transformations produce unique converted derivations, and that property is sufficient for the overall result: Bar induction is a principle by which such There is at each stage of strong normalization a finite number of non-normalities from which to choose the conversion to be made. Therefore strong normalization is a consequence of the variety of bar induction known as the fan theorem. The consistency of arithmetic was originally proved by bar induction by Gentzen and soon replaced by a proof through transfinite induction (see von Plato 2015 [8], and Siders and von Plato (2015) [4] for an explicit formulation of Gentzen's bar induction). As with Gentzen's proof, also the present proof could be carried through by the use of transfinite ordinals. What the least ordinal needed is, is at present not known, but because the fan theorem suffices for the result, Gentzen's The proofs of normalization and strong normalization through The proofs can obviously be worked through also for standard natural deduction, along the lines of my paper (von Plato 2011 [6]). Two more applications of explicit composition can be noted here: 1. 2. ization and strong normalization can be turned into a corresponding proof for typed [ .
A selector term is ## References1. Gentzen, G.: Untersuchungen über das logische Schließen. Mathematische Zeitschrift 2. Gentzen, G.: Der erste Widerspruchsfreiheitsbeweis für die klassische Zahlentheorie. First published in Archiv für mathematische Logik 3. Prawitz, D.: Natural Deduction: A Proof-Theoretical Study. Almqvist & Wiksell, Stockholm (1965) 4. Siders, A., von Plato, J.: Bar induction in the proof of termination of Gentzen's reduction procedure. In: Kahle, R., Rathjen, M. (eds.) Gentzen's Centenary: The Quest of Consistency, pp. 127–130. Springer, New York (2015) 5. von Plato, J.: Natural deduction with general elimination rules. Arch. Math. Log. 6. von Plato, J.: A sequent calculus isomorphic to Gentzen's natural deduction. Rev. Symb. Log.
7. von Plato, J.: Elements of Logical Reasoning. Cambridge University Press, Cambridge (2013) 8. von Plato, J.: From 9. von Plato, J., Siders, A.: Normal derivability in classical natural deduction. Rev. Symb. Log. |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2020