# zbMATH — the first resource for mathematics

Substitutions of $$\Sigma_1^0$$-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic. (English) Zbl 1009.03029
The main theme of this paper is various notions of consequences. But this is a synthesized report of the author’s work of the past two decades, and so other approaches can be also discerned. One of them is IPC (intuitionistic propositional calculus). Here, implication causes trouble. (Negation is a special form of implication.) The author isolates the class of “manageable formulas”, NNIL (no nesting of implications to the left) syntactically, and shows that it is exactly the class of robust formulas, modulo IPC equivalence. Robustness is defined semantically by preservation under Kripke submodels. To a formula $$A$$ he associates an NNIL formula $$A^*$$, and shows $$A^*\vdash B$$ (in IPC) is equivalent to the consequence relations $$A \vdash_\sigma B$$ and $$A\vdash_r B$$. Here, the $$\sigma$$-relation, $$\vdash_\sigma$$, is axiomatically given (like, $$C\vdash_\sigma A$$ and $$C\vdash_\sigma B$$ then $$C\vdash_\sigma A\wedge B$$; the condition involving implication is much more complicated), and $$A\vdash_r B$$ is, by definition for any robust $$C$$, $$C\vdash A \Rightarrow C\vdash B$$. {Notations, $$\vdash_\sigma$$ and $$\vdash_r$$, etc. are the reviewer’s, not the author’s.}
On the arithmetic side, “propositional contents” is of interest, and so two languages of IPC and HA are involved. Among other things, another characterization of $$\vdash_\sigma$$ is given via HA: $$A\vdash_\sigma B$$ iff (*) $$\text{HA}\vdash f[A]\Rightarrow \text{HA}\vdash f[B]$$ for any substitution $$f$$ of propositional variables by $$\Sigma$$-formulas. When $$f$$ ranges over all HA-formulas, (*) characterizes another axiomatically given $$\alpha$$-relation.
The last section is about closed fragments of the provability logics of HA, $$\text{HA}^*$$, and PA. On the propositional side, now the language, $${\mathcal L}_\square$$, has no variables, but has $$\square$$. In the arithmetical side, this $$\square$$ is replaced by an arithmetical provability formula. The closed fragment, $${\mathcal C}$$, consists of, by definition, those $$A$$ in $${\mathcal L}_\square$$ whose translation $$\langle A\rangle$$ is provable in the arithmetic in question. Each formula of $${\mathcal L}_\square$$ is associated to a degree of falsity, $$0,1,\dots,\omega$$. $$(0$$ is for $$\perp$$, and $$\omega$$ for $$\top$$.) The main theorem states that if many, but reasonable, conditions are met, then $$A$$ is in $${\mathcal C}$$ iff its degree is $$\omega$$. For the case of $$\text{HA}^*$$, its closed fragment is axiomatized. (Here, $$\text{HA}^*$$ is obtained from HA by adding $$A\to\text{Prov}(A)$$.)
Throughout the paper, examples and computations are presented, here and there.

##### MSC:
 03F55 Intuitionistic mathematics 03F30 First-order arithmetic and fragments 03F45 Provability logics and related algebras (e.g., diagonalizable algebras) 03B20 Subsystems of classical logic (including intuitionistic logic)
Full Text:
##### References:
  Beeson, M., The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations, J. symbolic logic, 40, 321-346, (1975) · Zbl 0316.02038  Berarducci, A.; Verbrugge, R., On the provability logic of bounded arithmetic, Ann. pure appl. logic, 61, 75-93, (1993) · Zbl 0803.03037  Boolos, G., The logic of provability, (1993), Cambridge University Press Cambridge · Zbl 0891.03004  Burr, W., Fragments of Heyting-arithmetic, J. symbolic logic, 65, 1223-1240, (2000) · Zbl 0966.03052  de Jongh, D.H.J., The maximality of the intuitionistic predicate calculus with respect to Heyting’s arithmetic, J. symbolic logic, 36, 606, (1970)  de Jongh, D.H.J., Formulas of one propositional variable in intuitionistic arithmetic, (), 51-64  de Jongh, D.H.J.; Chagrova, L.A., The decidability of dependency in intuitionistic propositional logic, J. symbolic logic, 60, 495-504, (1995) · Zbl 0836.03010  de Jongh, D.H.J.; Visser, A., Embeddings of Heyting algebras, (), 187-213 · Zbl 0857.03041  Friedman, H., One hundred and two problems in mathematical logic, J. symbolic logic, 40, 113-129, (1975) · Zbl 0318.02002  Friedman, H., Classically and intuitionistically provably recursive functions, (), 21-27 · Zbl 0396.03045  Gavrilenko, Yu.V., Recursive realizability from the intuitionistic point of view, Sov. math. dokl., 23, 9-14, (1981) · Zbl 0467.03055  Ghilardi, S., Unification in intuitionistic logic, J. symbolic logic, 64, 859-880, (1999) · Zbl 0930.03009  Ghilardi, S.; Zawadowski, M., A sheaf representation and duality for finitely presented Heyting algebras, J. symbolic logic, 60, 911-939, (1995) · Zbl 0837.03047  Ghilardi, S.; Zawadowski, M., Undefinability of propositional quantifiers in the modal system S4, Stud. logica, 55, 259-271, (1995) · Zbl 0831.03008  R. Grigolia, Free Algebras of Non-classical Logics, Metsniereba Press, Tbilisi, 1987 (in Russian).  P. Hájek (Ed.), Gödel ’96, Logical Foundations of Mathematics, Computer Science and Physics—Kurt Gödel’s Legacy, Springer, Berlin, 1996.  W. Hodges, M. Hyland, C. Steinhorn, J. Truss (Eds.), Logic: from Foundations to Applications, Clarendon Press, Oxford, 1996. · Zbl 0851.00045  R. Iemhoff, On the admissible rules of Intuitionistic propositional logic. preprint PP-1990-08, ILLC, Plantage Muidergracht 24, NL-1018TV Amsterdam, 1999, J. Symbolic Locic, to appear.  R. Iemhoff, A modal analysis of some principles of the provability logic of Heyting arithmetic, Proc. AiML’98, vol. 2, Uppsala, 20XX. · Zbl 0995.03045  Japaridze, G.; de Jongh, D., The logic of provability, (), 475-546 · Zbl 0915.03019  Leivant, D., Absoluteness in intuitionistic logic, vol. 73, (1975), Mathematical Centre Tract Amsterdam · Zbl 0459.03024  Leivant, D., Innocuous substitutions, J. symbolic logic, 45, 363-368, (1980) · Zbl 0434.03041  Leivant, D., Implicational complexity in intuitionistic arithmetic, J. symbolic logic, 46, 240-248, (1981) · Zbl 0488.03032  MacLane, S., Categories for the working Mathematician, graduate texts in mathematics, vol. 5, (1971), Springer New York  Pitts, A., On an interpretation of second order quantification in first order intuitionistic propositional logic, J. symbolic logic, 57, 33-52, (1992) · Zbl 0763.03009  Plisko, V.E., The nonarithmeticity of the class of realizable formulas, Math. USSR izv., 11, 453-471, (1997) · Zbl 0382.03043  Plisko, V.E., Some variants of the notion of realizability for predicate formulas, Math. USSR izv., 12, 588-604, (1978) · Zbl 0414.03038  Plisko, V.E., Absolute realizability of predicate formulas, Math. USSR izv., 22, 291-308, (1983) · Zbl 0554.03029  Rybakov, V.V., Rules of inference with parameters for intuitionistic logic, J. symbolic logic, 57, 912-923, (1992) · Zbl 0788.03007  Rybakov, V.V., Admissibility of logical inference rules, studies in logic, (1997), Elsevier Amsterdam · Zbl 0872.03002  V.Yu. Shavrukov, Subalgebras of diagonalizable algebras of theories containing arithmetic, Dissertationes Mathematicae (Rozprawy matematycne), CCCXXIII, 1993. · Zbl 0803.03044  Smoryński, C., Applications of Kripke models, (), 324-391  Smoryński, C., Self-reference and modal logic, universitext, (1985), Springer New York · Zbl 0596.03001  Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoret. comput. sci., 9, 67-72, (1979) · Zbl 0411.03049  A.S. Troelstra, in: Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, Springer Lecture Notes, Vol. 344, Springer, Berlin, 1973.  Troelstra, A.S.; van Dalen, D., Constructivism in mathematics, vol. 1, studies in logic and the foundations of mathematics, Vol. 121, (1988), North-Holland Amsterdam · Zbl 0653.03040  Troelstra, A.S.; van Dalen, D., Constructivism in mathematics, vol. 2, studies in logic and the foundations of mathematics, Vol. 123, (1988), North-Holland Amsterdam · Zbl 0653.03040  J.F.A.K. van Benthem, Temporal logic, in: Dov Gabbay, et al., (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Oxford University Press, Oxford, 1995. · Zbl 0850.03057  van Oosten, J., A semantical proof of de Jongh’s theorem, Arch. math. logic, 31, 105-114, (1991) · Zbl 0712.03047  L.C. Verbrugge, Efficient metamathematics, ILLC-Disseration Series 1993-3, Amsterdam, 1993.  A. Visser, Aspects of diagonalization and provability Ph.D. Thesis, Department of Philosophy, Utrecht University, 1981.  Visser, A., On the completeness principle, Ann. math. logic, 22, 263-295, (1982) · Zbl 0505.03026  A. Visser, Evaluation, provably deductive equivalence in Heyting’s arithmetic of substitution instances of propositional formulas, Logic Group Preprint Series 4, Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, 1985.  A. Visser, Propositional combinations of Σ-sentences in Heyting’s Arithmetic, Logic Group Preprint Series 117, Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, 1994.  Visser, A., Uniform interpolation and layered bisimulation, (), 139-164 · Zbl 0854.03026  Visser, A., An overview of interpretability logic, (), 307-359 · Zbl 0915.03020  A. Visser, Rules and arithmetics, Logic Group Preprint Series 189, Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, , 1998. To appear in Notre Dame Journal of Formal Logic.  A. Visser, Submodels of Kripke models, Logic Group Preprint Series 189, Department of Philosophy, Utrecht University, Heidelberglaan 8, 3584 CS Utrecht, , 1998. To appear in Archive for Mathematical Logic.  Visser, A.; van Benthem, J.; de Jongh, D.; Renardel de Lavalette, G., NNIL, a study in intuitionistic propositional logic, (), 289-326  R.E. Yavorsky, Logical schemes for first order theories, in: Springer Lecture Notes in Computer Science, Yaroslavl’97 volume, Vol. 1234, 1997, pp. 410-418. · Zbl 0888.03018  Zambella, D., Shavrukov’s theorem on the subalgebras of diagonalizable algebras for theories containing $$IΔ0+EXP$$, Notre dame J. formal logic, 35, 147-157, (1994) · Zbl 0801.03037
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.