On two classical results in the first order logic. (English) Zbl 1265.03064

The goal of the author is to prove a lemma which is the common core of two theorems, namely the Hilbert-Ackermann theorem (§4.3 of [J. R. Shoenfield, Mathematical logic. Reading, MA etc.: Addison-Wesley Publishing Company (1967; Zbl 0155.01102); reprint: Natick, MA: Association for Symbolic Logic (2001; Zbl 0965.03001)]; provability of open formulae from open theories in predicate logic coincides with provability in propositional logic), and Herbrand’s theorem. Both theorems were proved in [S. R. Buss, “On Herbrand’s theorem”, Lect. Notes Comput. Sci. 960, 195–209 (1995; doi:10.1007/3-540-60178-3_85); “An introduction to proof theory”, in: Handbook of proof theory, Stud. Logic Found. Math. 137, 1–78 (1998; Zbl 0912.03024)]; however, Buss notes mistakes for both articles at
which were repaired by [R. McKinley, “A sequent calculus demonstration of Herbrand’s”, 18 August 2010, http://www.iam.unibe.ch/~mckinley/herbrandnote.pdf]. This indicates that it is easy to make mistakes when proving those theorems.
The common lemma given in the article under review expresses that, if a formula \(\varphi\) is provable in an open theory \(T\), then a formula \(\varphi^H\) is provable as well. This lemma implies immediately the two theorems mentioned. Unfortunately, the proof of this lemma has some gaps for which we couldn’t find any easy way of repairing them. One gap is that the author claims in the second paragraph of the proof of Lemma 1 that we can assume \(\psi^D\) and \(\varphi^D\) to have no free variables in common and that these variables differ from critical variables in the proof. We do not know how to achieve this in a proof of the formula \((P(x)\to\exists x. P(x))\land(Q(x)\to\exists x. Q(x))\). Neither were we able to prove the statement in the third paragraph of the proof of Lemma 1, saying that “if \(\psi\to\theta\) is a substitution axiom, then \(\dots\)”. The use of the cut rule at the top of page 23 does not coincide with its definition in the source used [Shoenfield, loc. cit., p. 23]. We did not check the remainder of the proof of Lemma 1 carefully.


03F05 Cut-elimination and normal-form theorems
03F07 Structure of proofs
Full Text: DOI