Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). (Q930260)

From MaRDI portal
Revision as of 08:32, 10 December 2024 by Import241208061232 (talk | contribs) (Normalize DOI.)
(diff) ← Older revision | Latest revision (diff) | Newer revision → (diff)
scientific article
Language Label Description Also known as
English
Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
scientific article

    Statements

    Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). (English)
    0 references
    0 references
    0 references
    23 June 2008
    0 references
    Kreisel's conjecture stated that if Peano Arithmetic PA proves \(A(S^n0)\) for each \(n\) by a proof with \(\leq k\) lines then PA proves \(\forall xA(x)\). It had been proved by \textit{R. Parikh} [Trans. Am. Math. Soc. 177, 29--36 (1973; Zbl 0269.02011)] for a monadic formulation of PA with \(S\) as the only function and predicates for addition and multiplication. The paper under review provides a detailed treatment in numerous special cases for the following drastic modification by \textit{G. Kreisel} (in a supplement to [\textit{G. Takeuti}, Proof theory. 2nd ed. Amsterdam etc.: North-Holland (1987; Zbl 0609.03019)]). Suppose that \(\pi\) is a proof of \(A(S^n0)\) for just one (but large) \(n\). Then there is an infinite set \(X(\Pi,A)\subset \mathbf{N}\) with proofs of the same logical form \(\Pi\) as \(\pi\) for all \(A(S^m0)\) with \(m\in X(\Pi,A)\). The central notion in the reviewed paper is uniform derivability of a schema (by one and the same proof schema for all instances) instead of derivability in \(k\) steps. Descriptions of the sets \(X(\Pi,a)\) are derived from the properties of linear diophantine equations describing the proof schema. Equivalent (with respect to the set of theorems) formulations of PA behave differently in this respect. The ordinary successor induction gives uniform proofs of \(\exists x(x+x=S^{2n}0)\), whereas the order induction schema \(\forall\alpha(\forall \beta<\alpha A(\beta)\rightarrow A(\alpha)) \rightarrow \forall\alpha A(\alpha)\) admits generalization from \(n\) sufficiently large to \(A(S^nx)\). Hence the successor induction schema is not uniformly derivable from order induction, while the other direction holds in the presence of finitely many basic arithmetical axioms. A long postscript by \textit{G. Kreisel} supplements and criticizes the main body of the paper.
    0 references
    generalization of proofs
    0 references
    monadic language
    0 references
    partial proof data
    0 references
    modification of Kreisel's conjecture
    0 references
    proof complexity
    0 references
    uniform derivability of a proof schema
    0 references
    0 references

    Identifiers