Abstract
In this article we investigate the positive, i.e. \(\lnot ,\bot \)-free formulas of intuitionistic propositional and predicate logic, IPC and IQC, and minimal logic, MPC and MQC. For each formula \(\varphi \) of IQC we define the positive formula \(\varphi ^+\) that represents the positive content of \(\varphi \). The formulas \(\varphi \) and \(\varphi ^+\) exhibit the same behavior on top models, models with a largest world that makes all atomic sentences true. We characterize the positive formulas of IPC and IQC as the formulas that are immune to the operation of turning a model into a top model. With the +-operation on formulas we show, using the uniform interpolation theorem for IPC, that both the positive fragment of IPC and MPC respect a revised version of uniform interpolation. In propositional logic the well-known theorem that KC is conservative over the positive fragment of IPC is shown to generalize to many logics with positive axioms. In first-order logic, we show that IQC + DNS (double negation shift) + KC is conservative over the positive fragment of IQC and similar results as for IPC.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsNotes
- 1.
We do not consider identity and functional symbols, but our results will surely hold for the extension with such symbols.
- 2.
A Kripke frame is of depth \(n\) if the largest chain contains \(n\) nodes.
References
Brouwer, L.E.J.: Essentieel negatieve eigenschappen. Indag. Math. 10, 322–323 (1948)
Chagrov, A.V., Zakharyaschev, M.: Modal Logic. Oxford Logic Guides. Clarendon Press, Oxford (1997)
de Jongh, D., Yang, F.: Jankov’s theorems for intermediate logics in the setting of universal models. In: Bezhanishvili, N., Löbner, S., Schwabe, K., Spada, L. (eds.) TbiLLC 2009. LNCS, vol. 6618, pp. 53–76. Springer, Heidelberg (2011)
Diego, A.: Sur les Algèbres de Hilbert, vol. 21. E. Nauwelaerts, Gauthier-Villars, Louvain (1966)
Enderton, H.B.: A Mathematical Introduction to Logic. Harcourt/Academic Press, Burlington (2001)
Gabbay, D.M., de Jongh, D.H.J.: A sequence of decidable finitely axiomatizable: intermediate logics with the disjunction property. J. Symbolic Logic 39(1), 67–78 (1974)
Gabbay, D.M., Shehtman, V., Skvortsov, D.: Quantification in Nonclassical Logic I. Studies in Logic and the Foundations of Mathematics. Clarendon Press, Oxford (2009)
Ghilardi, S., Zawadowski, M.W.: Undefinability of propositional quantifiers in the modal system S4. Stud. Logica. 55(2), 259–271 (1995)
Griss, G.F.C.: Negationless intuitionistic mathematics I. Indag. Math. 8, 675–681 (1946)
Heyting, A.: Die formalen Regeln der intuitionistischen Logik, pp. 42–56 (1930)
Jankov, V.A.: Calculus of the weak law of the excluded middle (in russian). Izv. Akad. Nauk SSSR Ser. Mat. 32(5), 1044–1051 (1968)
Johansson, I.: Der Minimalkalkül Ein Reduzierter Intuitionistischer Formalismus. Compos. Math. 4, 119–136 (1937)
Kolmogorov, A.: Zur Deutung der intuitionistischen Logik. Math. Z. 35(1), 58–65 (1932)
Pitts, A.M.: On an interpretation of second order quantification in first order intuitionistic propositional logic. J. Symb. Logic 57, 33–52 (1992)
Renardel de Lavalette, G.R., Hendriks, A., de Jongh, D.: Intuitionistic implication without disjunction. J. Log. Comput. 22(3), 375–404 (2012)
Troelstra, A., van Dalen, D.: Constructivism in Mathematics, vols. 2. North-Holland, Amsterdam (1988)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2000)
Tzimoulis, A., Zhao, Z.: The Universal Model for the Negation-free Fragment of IPC. Technical Notes (X) Series X-2013-01, ILLC, University of Amsterdam (2013)
van Dalen, D.: Logic and Structure. Universitext. Springer, London (2012)
Visser, A.: Uniform interpolation and layered bisimulation. In: Hájek, P. (ed.) Proceedings of Gödel 1996: Logical Foundations of Mathematics, Computer Science and Physics - Kurt Gödel’s Legacy, Brno, Czech Republic. Lecture Notes Logic, vol. 6, pp. 139–164. Springer Verlag, Berlin (1996)
Zhao, Z.: An Investigation of Jankov’s Logic (2012) (Unpublished paper)
Acknowledgement
We thank Albert Visser, Nick Bezhanishvili, Rosalie Iemhoff, Grisha Mints and Anne Troelstra for informative discussions on the subject. We thank the referees for their corrections and Linde Frölke for her preparatory work.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Jongh, D., Zhao, Z. (2015). Positive Formulas in Intuitionistic and Minimal Logic. In: Aher, M., Hole, D., Jeřábek, E., Kupke, C. (eds) Logic, Language, and Computation. TbiLLC 2013. Lecture Notes in Computer Science(), vol 8984. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46906-4_11
Download citation
DOI: https://doi.org/10.1007/978-3-662-46906-4_11
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46905-7
Online ISBN: 978-3-662-46906-4
eBook Packages: Computer ScienceComputer Science (R0)