On First-Order Theories with Provability Operator
Artemov, Sergei ; Montagna, Franco
J. Symbolic Logic, Tome 59 (1994) no. 1, p. 1139-1153 / Harvested from Project Euclid
In this paper the modal operator "$x$ is provable in Peano Arithmetic" is incorporated into first-order theories. A provability extension of a theory is defined. Presburger Arithmetic of addition, Skolem Arithmetic of multiplication, and some first order theories of partial consistency statements are shown to remain decidable after natural provability extensions. It is also shown that natural provability extensions of a decidable theory may be undecidable.
Publié le : 1994-12-14
Classification: 
@article{1183744616,
     author = {Artemov, Sergei and Montagna, Franco},
     title = {On First-Order Theories with Provability Operator},
     journal = {J. Symbolic Logic},
     volume = {59},
     number = {1},
     year = {1994},
     pages = { 1139-1153},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1183744616}
}
Artemov, Sergei; Montagna, Franco. On First-Order Theories with Provability Operator. J. Symbolic Logic, Tome 59 (1994) no. 1, pp.  1139-1153. http://gdmltest.u-ga.fr/item/1183744616/