Intuitionistic Predicate Logic with Decidable Propositional Formulas

• Autorzy: Sakharov A.
• Języki publikacji: EN

Abstrakty

EN

First-order intuitionistic logic extended with the assumption about decidability of all propositional atoms combines classical and intuitionistic properties. Two classes of formulas on which this extension coincides with classical and intuitionis tic logic, respectively, are identied. Constrained Kripke structures are introduced for modeling intuitionistic logic with decidable propositional atoms. The extent of applicability of classicalonly laws, the extent of the disjunction and existence properties, decidability issues, and translations are investigated.

• Wydawca: Wydawnictwo Uniwersytetu Jagiellońskiego
• Czasopismo: Reports on Mathematical Logic
• Rocznik: 2007
• Tom: No. 42
• Strony: 153--168
• Opis fizyczny: Bibliogr. 16 poz., rys.

Twórcy

autor

Sakharov A.

• Verizon 40 Sylvan Road Waltham, MA 02451, USA,

Bibliografia

• [1] A. Degtyarev, A. Voronkov. Decidability Problems for the Prenex Fragment of Intuitionistic Logic. IEEE Symposium on Logic in Computer Science (LICS'96), pp.503-512, 1996.
• [2] D. Gabbay, Fibring Logics, Oxford University Press, 1999.
• [3] G. Gentzen, The Collected Papers of Gerhard Gentzen, edited by M. E. Szabo.North Holland, 1969.
• [4] A. Heyting, ed. L. E. J. Brouwer, Collected Works: Philosophy and Foundations of Mathematics, Elsevier, Amsterdam and New York, 1975.
• [5] S. C. Kleene, Introduction to Metamathematics. North Holland, 1952.
• [6] S. C. Kleene, Mathematical Logic, John Wiley and Sons, 1967.
• [7] R. Kontchakov, A. Kurucz, M. Zakharyaschev, Undecidability of First-Order Intuitionistic and Modal Logics with Two Variables. The Bulletin of Symbolic Logic, v.ol, no.3 (2005), pp. 428-438.
• [8] H. Kurokawa, Intuitionistic Logic with Classical Atoms. CUNY Technical Report, 2004, available at http://www.cs.gc.cuny.edu/tr/files/TR-2004003.pdf
• [9] G. Mints, A Short Introduction to Intuitionistic Logic, Kluwer Academic – Plenum Publishers, 2000.
• [10] S. Negri, J. von Plato, Structural Proof Theory. Cambridge University Press, 2001.
• [11] V. P. Orevkov, Solvable classes of pseudo-prenex formulas (in Russian), Zapiski Nauchnyh Seminarov LOMI, v. 60 (1976), pp. 109-170, English translation in: Journal of Soviet Mathematics.
• [12] C. Sernadas, J. Rasga, W. A. Carnielli, Modulated fibring and the collapsing problem.Journal of Symbolic Logic, v. 67, #4 (2002), pp. 1541-1569.
• [13] J. Suranyi. Zur Reduktion des Entscheidungsproblems des logischen Funktioskalkuls.Mathematikai es Fizikai Lapok, v. 50 (1943), pp. 51-74.
• [14] A. S. Troelstra, D. van Dalen, Constructivism in Mathematics: An Introduction, North-Holland, 1988.
• [15] A. S. Troelstra, H. Schwichtenberg. Basic Proof Theory. Cambridge University Press, 2005.
• [16] H. Weyl, Mathematics and Logic, American Mathematics Monthly, v.53, 2-13, 1946.