Geodesic
On Prenex Fragment of Provability Logic with Quantifiers on Proofs
Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 123-135.

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

We consider a fragment of provability logic with quantifiers on proofs that consists of formulas with no occurrences of quantifiers in the scope of the proof predicate. By definition, a logic ql is the set of formulas that are true in the standard model of arithmetic under every interpretation based on the standard Gödel proof predicate. We describe Kripke-style semantics for the logic ql and prove the corresponding completeness theorem. For the case of injective arithmetical interpretations, the decidability is proved. 
@article{TM_2003_242_a9,
     author = {R. \`E. Yavorskii},
     title = {On {Prenex} {Fragment} of {Provability} {Logic} with {Quantifiers} on {Proofs}},
     journal = {Trudy Matematicheskogo Instituta imeni V.A. Steklova},
     pages = {123--135},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TM_2003_242_a9/}
}
TY  - JOUR
AU  - R. È. Yavorskii
TI  - On Prenex Fragment of Provability Logic with Quantifiers on Proofs
JO  - Trudy Matematicheskogo Instituta imeni V.A. Steklova
PY  - 2003
SP  - 123
EP  - 135
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TM_2003_242_a9/
LA  - ru
ID  - TM_2003_242_a9
ER  - 
%0 Journal Article
%A R. È. Yavorskii
%T On Prenex Fragment of Provability Logic with Quantifiers on Proofs
%J Trudy Matematicheskogo Instituta imeni V.A. Steklova
%D 2003
%P 123-135
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TM_2003_242_a9/
%G ru
%F TM_2003_242_a9
R. È. Yavorskii. On Prenex Fragment of Provability Logic with Quantifiers on Proofs. Trudy Matematicheskogo Instituta imeni V.A. Steklova, Mathematical logic and algebra, Tome 242 (2003), pp. 123-135. http://geodesic.mathdoc.fr/item/TM_2003_242_a9/

[1] Artemov S. N., “Nearifmetichnost istinnostnykh predikatnykh logik dokazuemosti”, DAN SSSR, 284:2 (1985), 270–271 | MR | Zbl

[2] Beklemishev L. D., “O klassifikatsii propozitsionalnykh logik dokazuemosti”, Izv. AN SSSR. Ser. mat., 53:5 (1989), 915–943 | MR

[3] Vardanyan V. A., “Otsenki arifmeticheskoi slozhnosti predikatnykh logik dokazuemosti”, Slozhnost vychislenii i prikladnaya matematicheskaya logika. Voprosy kibernetiki, M., 1988, 46–72 | MR | Zbl

[4] Orlov I. E., “Ischislenie sravnimosti propozitsii”, Mat. sb., 35 (1928), 263–286 | Zbl

[5] Sidon T. L., “Logika dokazuemosti s operatsiyami nad dokazatelstvami”, Fund. i prikl. matematika, 3:4 (1997), 1173–1197 | MR | Zbl

[6] Sidon T. L., “Neaksiomatiziruemost predikatnykh logik dokazatelstv”, Vestn. MGU. Matematika. Mekhanika, 1997, no. 3, 12–16 | MR

[7] Artemov S., “Logic of proofs”, Ann. Pure and Appl. Logic, 67 (1994), 29–59 | DOI | MR | Zbl

[8] Artemov S., “Explicit provability and constructive semantics”, Bull. Symb. Logic, 7:1 (2001), 1–36 | DOI | MR | Zbl

[9] Artemov S., Sidon-Yavorskaya T., “On the first order logic of proofs”, Moscow Math. J., 1:4 (2001), 475–490 | MR | Zbl

[10] Boolos G., The logic of provability, Cambridge Univ. Press, Cambridge, 1993 | MR | Zbl

[11] Gödel K., “Eine Interpretation des intuitionistischen Aussagenkalkuls”, Ergeb. Math. Kolloq., 4 (1933), 39–40 | Zbl

[12] Japaridze G., de Jongh D., “Logic of provability”, Handbook of proof theory, ed. S. Buss, Elsevier, Amsterdam, 1998, 475–546 | MR | Zbl

[13] Krupski V. N., “Operational logic of proofs with functionality condition on proof predicate”, Lect. Notes Comput. Sci., 1234, 1997, 167–177 | MR | Zbl

[14] Krupski V. N., “The single-conclusion proof logic and inference rules specification”, Ann. Pure and Appl. Logic, 113:1–3 (2001), 181–206 | DOI | MR

[15] Solovay R. M., “Provability interpretations of modal logic”, Israel J. Math., 28 (1976), 33–71 | MR

[16] Yavorsky R. E., “On the logic of the standard proof predicate”, Lect. Notes Comput. Sci., 1862, 2000, 527–542 | MR

[17] Yavorsky R. E., “Provability logics with quantifiers on proofs”, Ann. Pure and Appl. Logic, 113:1–3 (2001), 373–387 | DOI | MR

[18] Yavorsky R. E., “On arithmetical completeness of first-order logics of provability”, Advances in Modal Logic, CSLI Publ., 3 (to appear) | MR