On an extension of Hilbert's second ε-theorem

Publisher Website
Google Scholar
Abstract
The aim of this paper is to correct an error in the proof in [2] of a strengthened version of Hilbert's second ε-theorem.Hilbert's original theorem says (effectively) that formulae of the form ∃xA → A(εxA) can be eliminated from deductions of ∈-free sentences B (i.e. those which do not contain the ε-symbol) from collections X of ε-free sentences. The extended version (Theorem III. 11 of [2]) says that, in addition, instances of Ackermann's schema can also be eliminated.The error in [2] occurs in the proof of Theorem III.7 and is described as follows. If A′ is the formula obtained from A by replacing every occurrence of ∃yB by B(εyB) (or ∀yC by C(εyB) if B is of the form ¬ C), and if A is a Q3 or Q4-axiom then, contrary to the claim on p. 73 of [2], A′ is not necessarily an axiom of the same form. For example, if A is the Q3-axiom where the rank of εx∃yD(x, y) is ≤ the rank of εyB (see p. 70) and where B is D(t,y), then A′ is which is not a Q3-axiom. In other words, the notion of rank as defined in [2] is inadequate for the proof of Theorem III.11.

This publication has 0 references indexed in Scilit: