Geodesic
On a Diophantine representation of the predicate of provability
Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XII, Tome 407 (2012), pp. 77-104
Cet article a éte moissonné depuis la source Math-Net.Ru

Voir la notice du chapitre de livre

Let $\mathcal P$ be the first order predicate calculus with a single binary predicate letter. Making use of the techniques of Diophantine coding developed in the works on Hilbert tenth problem, we construct a polynomial $F(t;x_1,\ldots,x_n)$ with integral rational coefficients such that the Diophantine equation $$ F(t_0;x_1,\ldots,x_n)=0 $$ is soluble in integers if and only if the formula of $\mathcal P$, numbered $t_0$ in the chosen numbering of the formulae of $\mathcal P$, is provable in $\mathcal P$. As an application of that construction, we describe a class of Diophantine equations which can be proved insoluble only under some additional axioms of the axiomatic set theory, for instance, assuming existence of an inaccessible cardinal. 
@article{ZNSL_2012_407_a3,
     author = {M. Carl and B. Z. Moroz},
     title = {On {a~Diophantine} representation of the predicate of provability},
     journal = {Zapiski Nauchnykh Seminarov POMI},
     pages = {77--104},
     year = {2012},
     volume = {407},
     language = {en},
     url = {http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a3/}
}
TY  - JOUR
AU  - M. Carl
AU  - B. Z. Moroz
TI  - On a Diophantine representation of the predicate of provability
JO  - Zapiski Nauchnykh Seminarov POMI
PY  - 2012
SP  - 77
EP  - 104
VL  - 407
UR  - http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a3/
LA  - en
ID  - ZNSL_2012_407_a3
ER  - 
%0 Journal Article
%A M. Carl
%A B. Z. Moroz
%T On a Diophantine representation of the predicate of provability
%J Zapiski Nauchnykh Seminarov POMI
%D 2012
%P 77-104
%V 407
%U http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a3/
%G en
%F ZNSL_2012_407_a3
M. Carl; B. Z. Moroz. On a Diophantine representation of the predicate of provability. Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part XII, Tome 407 (2012), pp. 77-104. http://geodesic.mathdoc.fr/item/ZNSL_2012_407_a3/

[1] M. Carl, Formale Mathematik und diophantische Gleichungen, Diplomarbeit, Universität Bonn, 2007

[2] M. Davis, “Hilbert's tenth problem is unsolvable”, The American Mathematical Monthly, 80 (1973), 233–269 | DOI | MR | Zbl

[3] M. Davis, Yu. Matijasevic̆, Ju. Robinson, “Hilbert's tenth problem. Diophantine equations: positive aspects of a negative solution”, Proceedings of Symposia in Pure Maths, 28 (1976), 323–378 | DOI | MR | Zbl

[4] V. H. Dyson, J. P. Jones, J. C. Shepherdson, “Some Diophantine forms of Gödel's theorem”, Archiv für Mathematische Logik und Grundlagenforschung, 22:1–2 (1982), 51–60 | MR | Zbl

[5] H. M. Friedman, “Finite functions and the necessary use of large cardinals”, Ann. Math., 148 (1998), 803–893 | DOI | MR | Zbl

[6] K. Gödel, The consistency of the axiom of choice and of the generalised continuum hypothesis with the axioms of set theory, Princeton University Press, 1940 | MR | Zbl

[7] J. P. Jones, “Universal Diophantine equation”, J. Symb. Logic, 47 (1982), 549–571 | DOI | MR | Zbl

[8] L. Kalmár, “Zurückführung des Entscheidungsproblems auf den Fall von Formeln mit einer einzigen binären Funktionsvariablen”, Compositio Mathematica, 4 (1936), 137–144 | MR | Zbl

[9] Yu. I. Manin, “Brouwer memorial lecture”, Nieuw Arch. Wisk. (4), 6:1–2 (1988), 1–6 | MR | Zbl

[10] Yu. V. Matiyasevich, “Enumerable sets are Diophantine”, Dokl. Akad. Nauk SSSR, 191:2 (1970), 279–282 | MR | Zbl

[11] Yu. V. Matiyasevich, “Diophantine representation of enumerable predicates”, Izv. Akad Nauk SSSR. Ser. Mat., 35:1 (1971), 3–30 | MR | Zbl

[12] Yu. V. Matiyasevich, Hilbert's Tenth Problem, Nauka, Moskva, 1993 | MR | Zbl

[13] Yu. V. Matiyasevich, An e-mail letter to the second author, March 2005

[14] E. Mendelson, Introduction to Mathematical Logic, Chapman Hall/CRM, 2001 | MR