Journal of Logic and Computation

Journal of Logic and Computation Advance Access published online on August 17, 2009
Journal of Logic and Computation, doi:10.1093/logcom/exp045

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Plisko, V. Social Bookmarking          What's this?

© The Author, 2009. Published by Oxford University Press. All rights reserved. For Permissions, please email: journals.permissions@oxfordjournals.org

Original Papers

On two Attempts of Describing Propositional Realizability Logic

Valery Plisko

Faculty of Mechanics and Mathematics, Moscow State University, Moscow 119991, Russia.
E-mail: veplisko{at}yandex.ru

Received 6 February 2009.

The study of propositional realizability logic was initiated in the 50th of the last century. Unfortunately, no description of the class of realizable propositional formulas is found up to now. Nevertheless, some attempts of such a description were made. In 1974, the author proved that every known realizable propositional formula has the property that every one of its closed arithmetical instances is deducible in the system obtained by adding Extended Church's Thesis and Markov Principle as axiom schemes to Intuitionistic Arithmetic. Visser calls this system Markov's Arithmetic. In 1990, another attempt of describing the class of realizable propositional formulas was made by Varpakhovskii who proposed a calculus in an extended propositional language and proved that all known realizable propositional formulas are deducible in this calculus. In this article we prove that every propositional formula deducible in Varpakhovskii's calculus has the property that each of its closed arithmetical instances is deducible in Markov's Arithmetic.

Keywords: Propositional logic; recursive realizability; Markov's Arithmetic

References

1. Dragalin AG. Mathematical Intuitionism (1988) American Mathematical Society, Providence.
2. Kleene SC. On the interpretation of intuitionistic number theory. Journal of Symbolic Logic (1945) 10:109–124.[CrossRef]
3. Kleene SC. Introduction to Metamathematics (1952) North-Holland Publishing Company.
4. Nelson D. Recursive functions and intuitionistic number theory. Transactions of the American Mathematical Society (1947) 61:307–368.[CrossRef][Web of Science]
5. Plisko VE. A certain formal system that is connected with realizability (Russian). In: Teoriya Algorifmov i Matematicheskaya Logika (Theory of Algorithms and Mathematical Logic)—Kushner BA, Nagornyi NM, eds. (1974) Vychislitelnyi Centr AN SSSR. 148–158.
6. Plisko VE. A survey of propositional realizability logic. The Bulletin of Symbolic Logic (2009) 15:1–42.[CrossRef]
7. Plisko VE. The Varpakhovskii calculus and Markov arithmetic. Utrecht University, Logic Group Preprint Series (2009) 271:1–43.
8. Troelstra AS, ed. Metamathematical Investigation of Intuitionistic Arithmetic, & Analysis (1973) Springer. Vol. 344 of Lecture Notes in Mathematics.
9. Varpakhovskii FL. On the axiomatization of realizable propositional formulae (Russian). In: Doklady Akademii Nauk SSSR (1990) 314:32–36. Translation Soviet Mathematics Doklady, 42, 260–264, 1991.
10. Visser A. Propositional logics of closed and open substitutions over Heyting Arithmetic. The Notre Dame Journal of Formal Logic (2006) 47:299–309.[CrossRef]

CiteULike    Connotea    Del.icio.us    What's this?

This Article Abstract Full Text (PDF) Alert me when this article is cited Alert me if a correction is posted Services Email this article to a friend Similar articles in this journal Alert me to new issues of the journal Add to My Personal Archive Download to citation manager Request Permissions Google Scholar Articles by Plisko, V. Social Bookmarking          What's this?