{"@context":["https://w3id.org/fdo/context/v1",{"schema":"https://schema.org/","prov":"http://www.w3.org/ns/prov#","fdo":"https://w3id.org/fdo/vocabulary/"}],"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q1807464","@type":"DigitalObject","kernel":{"@id":"https://fdo.portal.mardi4nfdi.de/fdo/Q1807464","digitalObjectType":"https://schema.org/ScholarlyArticle","primaryIdentifier":"mardi:Q1807464","kernelVersion":"v1","immutable":true,"modified":"2025-12-25T16:28:03Z"},"profile":{"@context":"https://schema.org","@type":"ScholarlyArticle","@id":"https://portal.mardi4nfdi.de/entity/Q1807464","name":"A method of epsilon substitution for the predicate logic with equality","headline":"A method of epsilon substitution for the predicate logic with equality","description":"scientific article; zbMATH DE number 1364699","url":"https://portal.mardi4nfdi.de/entity/Q1807464","datePublished":"1999-11-22","author":[{"@id":"https://portal.mardi4nfdi.de/entity/Q454365"}],"publisher":[{"@id":"https://portal.mardi4nfdi.de/entity/Q195577"}],"identifier":{"@type":"PropertyValue","propertyID":"doi","value":"10.1007/BF02358997","url":"https://doi.org/10.1007/BF02358997"},"sameAs":["https://doi.org/10.1007/BF02358997"],"comment":"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.","citation":[{"@id":"https://portal.mardi4nfdi.de/entity/Q3268377"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5925300"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5806808"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5809142"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3674650"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3832565"},{"@id":"https://portal.mardi4nfdi.de/entity/Q4325774"},{"@id":"https://portal.mardi4nfdi.de/entity/Q1908821"},{"@id":"https://portal.mardi4nfdi.de/entity/Q3128468"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5608741"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5343336"},{"@id":"https://portal.mardi4nfdi.de/entity/Q5834186"}]},"provenance":{"prov:generatedAtTime":"2025-12-25T16:28:03Z","prov:wasAttributedTo":"MaRDI Knowledge Graph"}}