Geodesic
A method of epsilon substitution for the predicate logic with equality
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IX, Tome 220 (1995), pp. 93-122

Voir la notice de l'article provenant de la source Math-Net.Ru

The method of epsilon substitution was defined for arithmetic with interpretation of $\varepsilon xA(x)$ as the least $x$ satisfying $A(x)$. It proceeds by a series of finite approximations “from below” to a solution of a timed system of critical formulas. For the predicate logic only approach “from above” similar to cut-elimination was available. We present a definition of epsilon substitution for the predicate logic, prove the termination of the substitution process, and derive the corresponding Herbrand-type theorem. Bibliography: 18 titles. 
@article{ZNSL_1995_220_a6,
     author = {G. E. Mints},
     title = {A method of epsilon substitution for the predicate logic with equality},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {93--122},
     publisher = {mathdoc},
     volume = {220},
     year = {1995},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_1995_220_a6/}
}
TY  - JOUR
AU  - G. E. Mints
TI  - A method of epsilon substitution for the predicate logic with equality
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 1995
SP  - 93
EP  - 122
VL  - 220
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/ZNSL_1995_220_a6/
LA  - ru
ID  - ZNSL_1995_220_a6
ER  - 
%0 Journal Article
%A G. E. Mints
%T A method of epsilon substitution for the predicate logic with equality
%J Zapiski Nauchnykh Seminarov POMI
%D 1995
%P 93-122
%V 220
%I mathdoc
%U http://geodesic.mathdoc.fr/item/ZNSL_1995_220_a6/
%G ru
%F ZNSL_1995_220_a6
G. E. Mints. A method of epsilon substitution for the predicate logic with equality. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part IX, Tome 220 (1995), pp. 93-122. http://geodesic.mathdoc.fr/item/ZNSL_1995_220_a6/