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/exp041

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 Dashkov, E. 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

Arithmetical Completeness of the Intuitionistic Logic of Proofs

Evgenij Dashkov

Department of Mathematical Logic and Theory of Algorithms, Faculty of Mechanics and Mathematics, Lomonosov Moscow State University, Moscow 119992, Russia.
E-mail: edashkov{at}gmail.com

Received 3 February 2009.

Classical logic of proofs LP naturally extends propositional calculus to the language enriched with formulas meaning t is a proof of formula F. Intuitionistic logic of proofs iLP introduced by Artemov and Iemhoff was conjectured to be complete with respect to intuitionistic arithmetic HA. The article presents a proof of this conjecture.

Keywords: Logic of proofs; intuitionistic arithmetic; admissible rules

References

1. Artemov S. Explicit provability and constructive semantics. The Bulletin for Symbolic Logic (2001) 7:136.
2. Artemov S. Unified semantics for modality and -terms via proof polynomials. In: Algebras, Diagrams and Decisions in Language, Logic and Computation—Vermeulen K, Copestake A, eds. (2002) CSLI Publications, Stanford University.
3. Artemov S, Iemhoff R. The basic intuitionistic logic of proofs. The Journal of Symbolic Logic (2007) 72:439–451.[CrossRef]
4. Beklemishev L, Visser A. Problems in the Logic of Provability. In: Mathematical Problems from Applied Logic I—Gabbay DM, Goncharov SS, Zakharyaschev M, eds. (2006) Springer.
5. Dashkov E. Intuitionistic Logic of Proofs. In: Logic Group Preprint Series (2008) Last accessed on date 6 May 2009. 269. University of Utrecht. Available at http://www.phil.uu.nl/preprints/preprints/PREPRINTS/preprint269.pdf.
6. Fitting M. The Logic of Proofs, Semantically. Annals of Pure and Applied Logic (2005) 132:1–25.[CrossRef][Web of Science]
7. Ghilardi S. Unification in intuitionistic logic. The Journal of Symbolic Logic (1999) 64:859–880.[CrossRef]
8. Iemhoff R. On the admissible rules of intuitionistic propositional logic. The Journal of Symbolic Logic (2001) 66:281–294.[CrossRef]
9. Iemhoff R. Provability Logic and Admissible Rules (2001) University of Amsterdam. PhD Thesis.
10. Kleene S. Introduction to Metamathematics (1952) D. van Nostrand Co. Inc.
11. Mkrtychev A. Models for the Logic of Proofs. Adian SI, Nerode A, eds. (1997) Springer. 266–275. In Proceedings of the 4th International Symposium on Logical Foundations of Computer Science (LFCS’97), Yaroslavl, Vol. 1234 of Lecture Notes in Computer Science.
12. Smorynski C. Applications of Kripke models. In: Mathematical Investigations of Intuitionistic Arithmetic and Analysis—Troelstra A, ed. (1973) Springer.
13. Smorynski C. Self-reference and Modal Logic. (1985) Springer.
14. Visser A. Rules and Arithmetics. Notre Dame Journal of Formal Logic (1999) 40:116–140.[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 Dashkov, E. Social Bookmarking          What's this?