Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic.

*(English)*Zbl 1009.03029The 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.

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.

Reviewer: M.Yasuhara (Princeton)

##### 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) |

##### Keywords:

Heyting arithmetic; intuitionistic propositional calculus; robust formulas; consequence relations; provability logics; closed fragment
PDF
BibTeX
XML
Cite

\textit{A. Visser}, Ann. Pure Appl. Logic 114, No. 1--3, 227--271 (2002; Zbl 1009.03029)

Full Text:
DOI

##### References:

[1] | 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 |

[2] | Berarducci, A.; Verbrugge, R., On the provability logic of bounded arithmetic, Ann. pure appl. logic, 61, 75-93, (1993) · Zbl 0803.03037 |

[3] | Boolos, G., The logic of provability, (1993), Cambridge University Press Cambridge · Zbl 0891.03004 |

[4] | Burr, W., Fragments of Heyting-arithmetic, J. symbolic logic, 65, 1223-1240, (2000) · Zbl 0966.03052 |

[5] | de Jongh, D.H.J., The maximality of the intuitionistic predicate calculus with respect to Heyting’s arithmetic, J. symbolic logic, 36, 606, (1970) |

[6] | de Jongh, D.H.J., Formulas of one propositional variable in intuitionistic arithmetic, (), 51-64 |

[7] | 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 |

[8] | de Jongh, D.H.J.; Visser, A., Embeddings of Heyting algebras, (), 187-213 · Zbl 0857.03041 |

[9] | Friedman, H., One hundred and two problems in mathematical logic, J. symbolic logic, 40, 113-129, (1975) · Zbl 0318.02002 |

[10] | Friedman, H., Classically and intuitionistically provably recursive functions, (), 21-27 · Zbl 0396.03045 |

[11] | Gavrilenko, Yu.V., Recursive realizability from the intuitionistic point of view, Sov. math. dokl., 23, 9-14, (1981) · Zbl 0467.03055 |

[12] | Ghilardi, S., Unification in intuitionistic logic, J. symbolic logic, 64, 859-880, (1999) · Zbl 0930.03009 |

[13] | Ghilardi, S.; Zawadowski, M., A sheaf representation and duality for finitely presented Heyting algebras, J. symbolic logic, 60, 911-939, (1995) · Zbl 0837.03047 |

[14] | Ghilardi, S.; Zawadowski, M., Undefinability of propositional quantifiers in the modal system S4, Stud. logica, 55, 259-271, (1995) · Zbl 0831.03008 |

[15] | R. Grigolia, Free Algebras of Non-classical Logics, Metsniereba Press, Tbilisi, 1987 (in Russian). |

[16] | P. Hájek (Ed.), Gödel ’96, Logical Foundations of Mathematics, Computer Science and Physics—Kurt Gödel’s Legacy, Springer, Berlin, 1996. |

[17] | W. Hodges, M. Hyland, C. Steinhorn, J. Truss (Eds.), Logic: from Foundations to Applications, Clarendon Press, Oxford, 1996. · Zbl 0851.00045 |

[18] | 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. |

[19] | 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 |

[20] | Japaridze, G.; de Jongh, D., The logic of provability, (), 475-546 · Zbl 0915.03019 |

[21] | Leivant, D., Absoluteness in intuitionistic logic, vol. 73, (1975), Mathematical Centre Tract Amsterdam · Zbl 0459.03024 |

[22] | Leivant, D., Innocuous substitutions, J. symbolic logic, 45, 363-368, (1980) · Zbl 0434.03041 |

[23] | Leivant, D., Implicational complexity in intuitionistic arithmetic, J. symbolic logic, 46, 240-248, (1981) · Zbl 0488.03032 |

[24] | MacLane, S., Categories for the working Mathematician, graduate texts in mathematics, vol. 5, (1971), Springer New York |

[25] | 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 |

[26] | Plisko, V.E., The nonarithmeticity of the class of realizable formulas, Math. USSR izv., 11, 453-471, (1997) · Zbl 0382.03043 |

[27] | Plisko, V.E., Some variants of the notion of realizability for predicate formulas, Math. USSR izv., 12, 588-604, (1978) · Zbl 0414.03038 |

[28] | Plisko, V.E., Absolute realizability of predicate formulas, Math. USSR izv., 22, 291-308, (1983) · Zbl 0554.03029 |

[29] | Rybakov, V.V., Rules of inference with parameters for intuitionistic logic, J. symbolic logic, 57, 912-923, (1992) · Zbl 0788.03007 |

[30] | Rybakov, V.V., Admissibility of logical inference rules, studies in logic, (1997), Elsevier Amsterdam · Zbl 0872.03002 |

[31] | V.Yu. Shavrukov, Subalgebras of diagonalizable algebras of theories containing arithmetic, Dissertationes Mathematicae (Rozprawy matematycne), CCCXXIII, 1993. · Zbl 0803.03044 |

[32] | Smoryński, C., Applications of Kripke models, (), 324-391 |

[33] | Smoryński, C., Self-reference and modal logic, universitext, (1985), Springer New York · Zbl 0596.03001 |

[34] | Statman, R., Intuitionistic propositional logic is polynomial-space complete, Theoret. comput. sci., 9, 67-72, (1979) · Zbl 0411.03049 |

[35] | A.S. Troelstra, in: Metamathematical Investigations of Intuitionistic Arithmetic and Analysis, Springer Lecture Notes, Vol. 344, Springer, Berlin, 1973. |

[36] | 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 |

[37] | 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 |

[38] | 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 |

[39] | van Oosten, J., A semantical proof of de Jongh’s theorem, Arch. math. logic, 31, 105-114, (1991) · Zbl 0712.03047 |

[40] | L.C. Verbrugge, Efficient metamathematics, ILLC-Disseration Series 1993-3, Amsterdam, 1993. |

[41] | A. Visser, Aspects of diagonalization and provability Ph.D. Thesis, Department of Philosophy, Utrecht University, 1981. |

[42] | Visser, A., On the completeness principle, Ann. math. logic, 22, 263-295, (1982) · Zbl 0505.03026 |

[43] | 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. |

[44] | 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. |

[45] | Visser, A., Uniform interpolation and layered bisimulation, (), 139-164 · Zbl 0854.03026 |

[46] | Visser, A., An overview of interpretability logic, (), 307-359 · Zbl 0915.03020 |

[47] | 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. |

[48] | 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. |

[49] | Visser, A.; van Benthem, J.; de Jongh, D.; Renardel de Lavalette, G., NNIL, a study in intuitionistic propositional logic, (), 289-326 |

[50] | 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 |

[51] | 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.