zbMATH — the first resource for mathematics

Propositions in propositional logic provable only by indirect proofs. (English) Zbl 0906.03056
D. Prawitz noticed [Natural deduction. A proof-theoretical study (1965; Zbl 0173.00205), p. 95] that normalization fails for “naive” set theory with the standard introduction and elimination rules for \(\in\): \[ \in I:\quad \Gamma \Rightarrow A[x/t]/ \Gamma \Rightarrow t\in \{x| A\}; \qquad \in E:\quad \Gamma \Rightarrow t\in \{x| A\}/ \Gamma \Rightarrow A[x/t] \] L. Hallnäs developed this observation in his dissertation [“On normalization of proofs in set theory”, Diss. Math. 261 (1988; Zbl 0667.03041)]. The present paper brings this observation down to the propositional level (a similar observation was made by N. Tennant). By translating the “naive” comprehension axiom \(t\in t\leftrightarrow t\notin t\) (where \(t\equiv \{x| x\notin x\})\) by \(P\rightarrow \neg P\) it is shown that the intuitionistically deducible formula \(\neg(P \leftrightarrow \neg P)\) does not have a normal deduction \(d\) which is also “extensively normal”: every subdeduction \(d'\) of \(d\) deriving a sequent \(\Gamma' \Rightarrow A\) contains no proper subdeduction \(d''\) of a sequent \(\Gamma'' \Rightarrow A\) with \(\Gamma'' \subseteq \Gamma'\). In particular normalization according to standard reductions plus reduction of \(d'\) to \(d''\) does not terminate. This observation is extended to classical logic and to a wider class of formulas. One of the corollaries: a provable propositional sequent having no extensively normal deduction has infinitely many different deductions.
Reviewer: G.Mints (Stanford)

03F05 Cut-elimination and normal-form theorems
03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text: DOI
[1] Gentzen, Mathematische Zeitschrift 39 pp 176– (1934)
[2] English edition in: The Collected Papers of Gerhard Gentzen (ed.), North-Holland Publ. Comp., Amsterdam 1969.
[3] Natural Deduction: A Proof-Theoretical Study. Almquist b. Wiksell, Stockholm 1964.
[4] Ideas and Results in Proof Theory. In: Proceedings of the Second Scandinavian Logic Symposium (ed.), North-Holland Publ. Comp., Amsterdam 1971, pp. 235–307. · doi:10.1016/S0049-237X(08)70849-8
[5] Stålmarck, J. Symbolic Logic 56 pp 129– (1991)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.