A method of epsilon substitution for the predicate logic with equality
type: Item
instance of: scholarly article
title: A method of epsilon substitution for the predicate logic with equality
zbMATH Open document ID: 0934.03073
DOI: 10.1007/BF02358997
published in: Journal of Mathematical Sciences (New York)
publication date: 1999-11-22T00:00:00Z
review text: 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.
reviewed by: Osamu Sonobe
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 03B10
Mathematics Subject Classification ID: 03F03
zbMATH DE Number: 1364699
zbMATH Keywords: epsilon substitution method
zbMATH Keywords: predicate logic
zbMATH Keywords: axiom of equality
zbMATH Keywords: axiom of extensionality
author: G. E. Mints
MaRDI profile type: Publication
cites work: Q3268377
cites work: The consistency of arithmetics
cites work: On the Interpretation of Non-Finitist Proofs--Part I
cites work: On the interpretation of non-finitist proofs–Part II
cites work: Q3674650
cites work: Q3832565
cites work: Q4325774
cites work: Epsilon substitution method for elementary analysis
cites work: Strong termination for the epsilon substitution method
cites work: Q5608741
cites work: The substitution method
cites work: David Hilbert and his mathematical work
full work available at URL: https://doi.org/10.1007/bf02358997
OpenAlex ID: W2008841321
description: scientific article; zbMATH DE number 1364699