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

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.