zbMATH — the first resource for mathematics

Reflexive intermediate propositional logics. (English) Zbl 1105.03025
The author modifies the formulation and proof of a theorem due to D. C. McCarty [Notre Dame J. Formal Logic 43, 243–248 (2002; Zbl 1050.03041)] to get the following statement: Let \(T\) be a second-order theory based on a superintuitionistic logic. If \(T\) proves the completeness theorem (consistency implies existence of a model) for some superintuitionistic propositional logic, then \(T\) proves every instance of \(\neg\varphi\vee\neg\neg\varphi\). The proof uses very few properties of \(T\) except comprehension. Defining \(A= \{p\mid\neg\varphi\}\cup \{\neg p\mid\neg\neg\varphi\}\) and \(B= A\cup\{p\vee\neg p\}\), \(B\) is consistent since both \(\{p\}\) and \(\{\neg p\}\) are. By completeness, there is a model \(M\models B\), hence \(M\models p\vee\neg p\), so \(\neg\varphi\vee\neg\neg\varphi\).

03B55 Intermediate logics
Full Text: DOI
[1] Bernays, P., Beiträge zur axiomatischen Behandlung des Logik-Kalküls , Habilitationsschrift, Göttingen, 1918. Manuscript. Bernays Nachlaß, ETH Zürich, Hs 973.192.
[2] Enderton, H. B., A Mathematical Introduction to Logic , Academic Press, New York, 1972. · Zbl 0992.03001
[3] Gabbay, D. M., Semantical Investigations in Heyting’s Intuitionistic Logic , vol. 148 of Synthese Library , D. Reidel Publishing Co., Dordrecht, 1981. · Zbl 0453.03001
[4] Johnstone, P. T., ”Conditions related to De Morgan’s law”, pp. 479–91 in Applications of Sheaves , edited by M. P. Fourman, C. J. Mulvey, and D. S. Scott, vol. 753 of Lecture Notes in Mathemathics , Springer, Berlin, 1979. · Zbl 0445.03041
[5] Johnstone, P. T., ”Another condition equivalent to De Morgan’s law”, Communications in Algebra , vol. 7 (1979), pp. 1309–12. · Zbl 0417.18002
[6] Kreisel, G., ”Elementary completeness properties of intuitionistic logic with a note on negations of prenex formulae”, The Journal of Symbolic Logic , vol. 23 (1958), pp. 317–30. · Zbl 0086.24601
[7] Kreisel, G., ”A remark on free choice sequences and the topological completeness proofs”, The Journal of Symbolic Logic , vol. 23 (1958), pp. 369–88. · Zbl 0091.01101
[8] Kreisel, G., ”On weak completeness of intuitionistic predicate logic”, The Journal of Symbolic Logic , vol. 27 (1962), pp. 139–58. · Zbl 0117.01005
[9] Kreisel, G., ”Church’s thesis: A kind of reducibility axiom for constructive mathematics”, pp. 121–50 in Intuitionism and Proof Theory (Proceedings of the Summer Conference, Buffalo, 1968), North-Holland, Amsterdam, 1970. · Zbl 0199.30001
[10] Leivant, D., ”Failure of completeness properties of intuitionistic predicate logic for constructive models”, Annales Scientifiques de l’Université de Clermont. Mathématiques , (1976), pp. 93–107. · Zbl 0362.02014
[11] McCarty, D. C., ”Intuitionistic completeness and classical logic”, Notre Dame Journal of Formal Logic , vol. 43 (2002), pp. 243–48. · Zbl 1050.03041
[12] McCarty, D., ”Completeness for intuitionistic logic”, pp. 301–34 in Kreiseliana , A. K. Peters, Wellesley, 1996. · Zbl 0896.03007
[13] McCarty, D. C., ”Incompleteness in intuitionistic metamathematics”, Notre Dame Journal of Formal Logic , vol. 32 (1991), pp. 323–58. · Zbl 0751.03030
[14] Post, E. L., ”Introduction to general theory of elementary propositions”, American Journal of Mathematics , vol. 43 (1921), pp. 163–85. · JFM 48.1122.01
[15] Rautenberg, W., Klassische und nichtklassische Aussagenlogik , vol. 22 of Logik und Grundlagen der Mathematik , Friedrich Vieweg & Sohn, Braunschweig, 1979. · Zbl 0424.03007
[16] Simpson, S. G., Subsystems of Second Order Arithmetic , Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1999. · Zbl 0909.03048
[17] Troelstra, A. S., Choice Sequences, A Chapter of Intuitionistic Mathematics , edited by D. Scott, Oxford Logic Guides, Clarendon Press, Oxford, 1977. · Zbl 0355.02026
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.