Epsilon substitution method for elementary analysis
The fundamental expression of the language on which the epsilon substitution method, introduced by Hilbert, is based, is \(\varepsilon xF[x]\), meaning ``an \(x\) satisfying the condition \(F[x]\). In such a context the existential and the universal quantifiers can be defined explicitly as follows: \(\exists xF[x] = F [\varepsilon xF[x]]\) and \(\forall xF[x] = F [\varepsilon x \neg F[x]]\), and the central axioms of the corresponding formalism are the so-called critical formulae having the following form \(F[t] \to F [\varepsilon x F[x]]\). Hilbert's basic idea to transform any (non-finitistic) number-theoretic proof into a finitistic proof by means of the substitution method was described in Grundlagen der Mathematik (Bd. 2) (by \textit{D. Hilbert} and \textit{P. Bernays}, see the new edition by Springer-Verlag (Berlin, 1970; Zbl 0211.00901)). The main problem in the realisation of this great idea, in the context of various mathematical theories, is to prove that the corresponding procedure terminates. In this paper, the authors formulate the epsilon substitution method for the second-order arithmetic with comprehension for arithmetical formulae with predicate parameters (i.e. for elementary analysis). Two essentially different proofs of termination are presented, the first of which, the constructive one, uses embedding into a ramified system of level one via cut-elimination, and the second, shorter and non-constructive one, uses a continuity argument. Due to the authors' nice style of presentation, this paper is very pleasant to read, although this subject, by definition, includes a lot of difficult and complex arguments and technical details.
- Grundlagen der Mathematik. Bd. II.
- A formalization of recursive arithmetic.
- Les méthodes axiomatiques modernes et les fondements des mathématiques.
- Der Hilbertsche Formalismus. I: Der Formalismus H\(_{\text{I}}\).
- Classificatión sistemática de la propriedades lógicas.
- Zur Widerspruchsfreiheit der Zahlentheorie.
- The interdeducibility of the new Hilbert-Bernays theory and Principia Mathematica.
- Grundzüge der theoretischen Logik.
- Beweis der Widerspruchsfreiheit des Funktionenkalküls der mathematischen Logik.
- David Hilbert and his mathematical work
- Epsilon substitution method for elementary analysis
- Functionals defined by transfinite recursion
- Grundlagen der Mathematik I
- scientific article; zbMATH DE number 3150889 (Why is no real title available?)
- scientific article; zbMATH DE number 3827857 (Why is no real title available?)
- scientific article; zbMATH DE number 4108755 (Why is no real title available?)
- scientific article; zbMATH DE number 733386 (Why is no real title available?)
- scientific article; zbMATH DE number 3073037 (Why is no real title available?)
- On the Interpretation of Non-Finitist Proofs--Part I
- On the interpretation of non-finitist proofs–Part II
- The consistency of arithmetics
- The substitution method
- Epsilon substitution method for \(\text{ID}_{1}(\Pi_{1}^{0}\vee{\Sigma} _{1}^{0})\)
- A termination proof for epsilon substitution using partial derivations
- Epsilon substitution method for theories of jump hierarchies
- Epsilon substitution for \(ID_1\) via cut-elimination
- Epsilon substitution for transfinite induction
- A method of epsilon substitution for the predicate logic with equality
- Epsilon substitution method for elementary analysis
- Epsilon substitution for first- and second-order predicate logic
- Cut elimination for a simple formulation of epsilon calculus
- Ackermann's substitution method (remixed)
- Epsilon substitution method for \([\Pi^0_1,\Pi^0_1]\)-FIX
- On natural deduction in classical first-order logic: Curry-Howard correspondence, strong normalization and Herbrand's theorem
- The substitution method revisited
- Strong termination for the epsilon substitution method
- scientific article; zbMATH DE number 3859084 (Why is no real title available?)
- The Rank Function and Hilbert'S Second ε-Theorem
- scientific article; zbMATH DE number 4108755 (Why is no real title available?)
- scientific article; zbMATH DE number 733386 (Why is no real title available?)
- scientific article; zbMATH DE number 1078590 (Why is no real title available?)
- Epsilon Substitution Method for 11 - CR: a Constructive Termination Proof
- A constructive analysis of learning in Peano arithmetic
- 1998–99 Annual Meeting of the Association for Symbolic Logic
- scientific article; zbMATH DE number 1418438 (Why is no real title available?)
- Constructive forcing, CPS translations and witness extraction in interactive realizability
- 2005 Annual Meeting of the Association for Symbolic Logic
- VON NEUMANN’S CONSISTENCY PROOF
- Interactive realizability for second-order Heyting arithmetic with EM1 and SK1
- What evidence is there that \(2^{\land}65536\) is a natural number?
- The practice of finitism: epsilon calculus and consistency proofs in Hilbert's program
This page was built for publication: Epsilon substitution method for elementary analysis
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1908821)
