A method of epsilon substitution for the predicate logic with equality (Q1807464)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A method of epsilon substitution for the predicate logic with equality |
scientific article |
Statements
A method of epsilon substitution for the predicate logic with equality (English)
0 references
22 November 1999
0 references
The method of epsilon substitution for arithmetic proposed by Hilbert proceeds by a series of finite approximations ``from below'' to a solution of a fixed system of critical formulas. Ackermann applied the method also to the first order predicate logic with equality and extensionality formalized in terms of the epsilon symbol, which however proceeds ``from above'' by replacing the epsilon-terms of highest complexity similarly to cut-elimination. In this paper, the author provides for the predicate logic and its extensions by equality and extensionality, respectively, a method of epsilon substitution ``from below'' resembling Hilbert's original program, and proves the strong termination of the substitution process which corresponds to the strong normalizability in cut-elimination and is not obtained by Ackermann's method. As an application, a Herbrand-type theorem is shown to hold for the respective epsilon calculus.
0 references
epsilon substitution method
0 references
predicate logic
0 references
axiom of equality
0 references
axiom of extensionality
0 references