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

generalization of proofs modification of Kreisel's conjecture monadic language partial proof data proof complexity uniform derivability of a proof schema

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Structure of proofs (03F07) First-order arithmetic and fragments (03F30)

Review text

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.

Recommendations

Cites work

Cited in

(17)

This page was built for publication: Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q930260)