Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 136-140
Citer cet article
M. Baaz. Note on a Translation to Characterize Constructivity. Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 136-140. http://geodesic.mathdoc.fr/item/TM_2003_242_a10/
@article{TM_2003_242_a10,
author = {M. Baaz},
title = {Note on {a~Translation} to {Characterize} {Constructivity}},
journal = {Trudy Matematicheskogo Instituta imeni V.A. Steklova},
pages = {136--140},
year = {2003},
volume = {242},
language = {en},
url = {http://geodesic.mathdoc.fr/item/TM_2003_242_a10/}
}
TY - JOUR
AU - M. Baaz
TI - Note on a Translation to Characterize Constructivity
JO - Trudy Matematicheskogo Instituta imeni V.A. Steklova
PY - 2003
SP - 136
EP - 140
VL - 242
UR - http://geodesic.mathdoc.fr/item/TM_2003_242_a10/
LA - en
ID - TM_2003_242_a10
ER -
%0 Journal Article
%A M. Baaz
%T Note on a Translation to Characterize Constructivity
%J Trudy Matematicheskogo Instituta imeni V.A. Steklova
%D 2003
%P 136-140
%V 242
%U http://geodesic.mathdoc.fr/item/TM_2003_242_a10/
%G en
%F TM_2003_242_a10
This note describes a straightforward translation $\mathcal C^{(1)}$ such that $T\vdash A(t)$ for some term $t$$\Leftrightarrow$$\mathcal C^{(1)}(T)\vdash \mathcal C^{(1)}(\exists xA(x))$ for universal $T$ and purely existential $\exists xA(x)$. The correspondence is based on the properties of resolution calculus.
