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
    0 references
    epsilon substitution method
    0 references
    predicate logic
    0 references
    axiom of equality
    0 references
    axiom of extensionality
    0 references
    0 references

    Identifiers

    0 references
    0 references
    0 references
    0 references
    0 references
    0 references