Authors: Assylbek Issakhov and Fariza Rakymzhankyzy

Let \(F\) be a family of total functions which is computable by an oracle \(A\), where \(A\) is an arbitrary set. A numbering \(\alpha:\omega\mapsto \mathcal F\) is called \(A\)-computable if the binary function \(\alpha(n)(x)\) is \(A\)-computable, [1]. We call a numbering \(\alpha\) decidable (resp., positive, and Friedberg) if equivalence relation \(\theta_{\alpha} = \{ (x,y) \mid \alpha (x) = \alpha (y) \}\) is computable (resp., c.e., and identity).

An infinite set \(A\) is hyperimmune iff no recursive function majorizes \(A\). A degree is called hyperimmune if it contains a hyperimmune set, otherwise it is hyperimmune free. Every nonzero degree comparable with \(0'\) is hyperimmune.

In [2] it was proved that there is a c.e. noncomputable set \(B\) such that \(B\leq_{T} A\) iff for all families \(S\) of sets, it is true that if \(S\) has an \(A\)-computable Friedberg numbering, then \(S\) has infinitely many positive non-decidable \(A\)-computable numberings.

It is known that if \(\mathcal F\) is an infinite \(A\)-computable family of total functions, where \(A\) is a hyperimmune set, then \(\mathcal F\) has infinitely many pairwise nonequivalent \(A\)-computable Friedberg numberings, [3].

Let \(\mathcal F\) be an infinite \(A\)-computable family of total functions, where \(A\) is a hyperimmune set. Then

Theorem. \(\mathcal F\) has infinitely many pairwise nonequivalent positive non-decidable \(A\)-computable numberings.

Theorem. \(\mathcal F\) has infinitely many pairwise nonequivalent minimal non-positive \(A\)-computable numberings.

We know that if \(\mathcal F\) is an infinite \(A\)-computable family of total functions, where \(\emptyset' \leq_{T} A\), then the Rogers semilattice \(R_{A} (\mathcal F)\) contains an ideal without minimal elements, [4]. Now we are interested in investigating such property for the case with hyperimmune oracles.

Bibliography

1. S. A. Badaev, S. S. Goncharov, Generalized computable universal numberings, Algebra and Logic, vol. 53 (2014), no. 5, pp. 355–364.
2. F. Rakymzhankyzy, N.A. Bazhenov, A.A. Issakhov, B.S. Kalmurzayev, Minimal generalized computable numberings and families of positive preorders,Algebra and Logic, vol. 61 (2022), no. 3, pp. 188–206.
3. A. A. Issakhov, F. Rakymzhankyzy, Hyperimmunity and \(A\)-computable numberings,The Bulletin of Symbolic Logic, vol. 24 (2018), no. 2, pp. 248–249.
4. A. A. Issakhov, Ideals without minimal elements in Rogers semilattices,Algebra and Logic, vol. 54 (2015), no. 3, pp. 197–203.

Authors: Konstantinos Papafilippou and David Fernández Duque

A classical result of provability logic is the fixed point theorem, proved independently by D. de Jongh and G. Sambin [3] with various proof methods for it ever since. Its statement is the following: Given a modal formula \(\phi(p)\) that is modalized for \(p\) — i.e. every occurrence of \(p\) in \(\phi\) occurs within the scope of a \(\Box\) — there is a formula \(\sigma\) without \(p\) occurring in it such that \(GL \vdash \phi(\sigma) \rightarrow \sigma\). In fact, this fixed point is unique under equivalence over GL. Sambin’s construction [3,4], gives a rough upper bound for succinctness of the fixed point \(\sigma\) relative to the original formula \(\phi\) of the scale of \(\mid\sigma\mid \leq n^{O(n)}\) where \(n = \mid\phi\mid\). However there was no known succinctness lower bound.

The methods that we use to obtain a succinctness lower bound are those of formula-size games that were developed in the setting of Boolean function complexity [1] and of first-order logic and some temporal logics [2]. By now, the formula-size games have been adapted to a host of modal logics and used to obtain lower bounds on modal formulas expressing properties of Kripke models. These methods work by selecting a formula \(\phi\) of a language \(\mathcal{L}\) and two sets of models \(\mathcal{A}, \mathcal{B}\) that are separable by \(\phi\). Then the game is setup and played with rules according to a language \(\mathcal{L}'\). Once the game is concluded, we obtain a formula \(\psi\) in \(\mathcal{L}'\) equivalent to \(\phi\) and the size of \(\psi\) can be calculated by a careful analysis of the game on the sets \(\mathcal{A}\) and \(\mathcal{B}\).

Let \(\mathcal L_\Diamond\) be the standard modal language (with an irreflexive modality) and \(\mathcal L_\dot{\Diamond}\) be the language which instead includes a reflexive modality as primitive. In the case of GL, P. Iliev and D. Fern'andez-Duque have derived an exponential (\(2^{O(n)}\)) succinctness lower bound for \(\mathcal{L}_{\dot{\Diamond}}\) over \(\mathcal{L}_\Diamond\) in GL where \(\dot{\Diamond}\phi =: \phi \vee \Diamond \phi\). The sequence of formulas they used were defined inductively as:

• \(\phi_1 = p_1\);
• \(\phi_{n+1} = \dot{\Diamond} (p_{n+1} \wedge \phi_n )\).

Their result can be easily reformulated to show a succinctness lower bound for formulas in \(\mathcal{L}_{\Diamond}\), thus giving the following:
Theorem. There exists a sequence of formulas \((\psi_n)_{n<\omega}\) linear in \(n\) such that any fixed point in \(\mathcal L_\Diamond\) for \(\psi_n\) over \(\sf GL\) has size \(2^{O(n)}\).

We expand this succinctness lower bound in the following sense, we write formulas of \(\mathcal{L}\) whose fixed point in \(\mathcal{L}_{\Diamond\dot{\Diamond}}\) (i.e., the bi-modal logic with a reflexive and an irreflexive modality) is of the scale \(2^{O({n})}\). This is done with formulas expressing a kind of tree embeddability into our model. With this, we may improve upon the above Theorem as follows.
Theorem. There exists a sequence of formulas \((\gamma_n)_{n<\omega}\) linear in \(n\) such that any fixed point in \(\mathcal L_{\Diamond\dot{\Diamond}}\) for \(\gamma_n\) over \(\sf GL\) has size \(2^{O(n)}\).

Bibliography

1. Razborov A. A. Applications of matrix methods to the theory of lower bounds in computational complexity. {\em Combinatorica}, 10(1):81–93, 1990.
2. Micah Adler and Neil Immerman. An n! lower bound on formula size. {\em ACM Trans. Comput. Logic}, 4(3):296–314, jul 2003.
3. Sambin Giovanni and Valentini Silvio. {The modal logic of provability. The sequential approach}. {\em Journal of Philosophical Logic}, 11(3):311 – 342, 1982.
4. Lisa Reidhaar-Olson. {A new proof of the fixed-point theorem of provability logic.} {\em Notre Dame Journal of Formal Logic}, 31(1):37 – 43, 1989.

In [1], Kripke proposed to carry out his fixed-point semantics for truth over supervaluationist schemes in the style of [2]. Three schemes stood out, corresponding to different admissibility criteria for extensions of the truth predicate that are considered in the supervaluationist satisfaction relations: (1) the scheme vb, which considers extensions consistent with the original one; (2) the scheme vc, which considers consistent extensions more generally, and; (3) the scheme mc, which considers maximally consistent extensions. In [3], Cantini presented the axiomatic theory of truth VF, which happened to be sound with respect to the fixed points of Kripke’s theory constructed over the scheme vc: that is, every classical fixed-point model for vc over the standard model of arithmetic \(\mathbb{N}\) is also a model of VF. As [4] shows, this is the best one could hope for in relation to any of the supervaluationist schemes mentioned above—there is no sound theory satisfying the reverse implication. Furthermore, Cantini proved that VF is a remarkably strong theory from a proof-theoretic point of view, matching the strength of the impredicative theory ID\(_1\).

In this paper, we complete the picture of axiomatic theories of supervaluationist truth, introducing two new theories that correspond—and are sound with respect—to the schemes vb and mc. In the case of the former scheme, we advance a theory that we call VF\(^-\), and establish its proof-theoretic strength, which equals that of VF.

The most substantial part of the paper, however, is dedicated to the theory which axiomatizes the fixed-point semantic theory over mc. We provide a proof-theoretic analysis of this theory, which we call VFM, in two stages. For the lower bound, we show that the theory can define Tarskian ramified truth predicates up to \(\varepsilon_0\) (RA\(_{<\varepsilon_0}\)). For the upper bound, we provide a cut elimination argument formalized within the theory ID\(^*_1\), which is known to be proof-theoretically equivalent to RA\(_{<\varepsilon_0}\). Hence, we conclude that VFM is proof-theoretically much weaker than the rest of theories of the supervaluationist family, and indeed on a par with the well-known theory KF.

Finally, we also introduce the schematic reflective closure of the theory VFM, as defined in [5]. We establish its consistency, and carry out the proof-theoretic analysis for this theory, which confirms that this schematic reflective closure as proof-theoretically strong as the theory RA\(_{<\Gamma_0}\).

This is joint work with Daichi Hayashi.

Bibliography

1. Saul Kripke,Outline of a theory of truth,The Journal of Philosophy,vol. 72 (1975), no. 19, pp. 690–716.
2. Bas C. van Fraassen,Singular terms, truth-value gaps, and free logic.,The Journal of Philosophy,vol. 63 (1966), no. 17, pp. 481-495.
3. Andrea Cantini,A theory of formal truth arithmetically equivalent to {ID}\(_1\),Journal of Symbolic Logic,vol. 55 (1990), no. 1, pp. 244–259.
4. Martin Fischer, Volker Halbach, Jönne Kriener, and Johannes Stern,Axiomatizing semantic theories of truth?,The Review of Symbolic Logic,vol. 8 (2015), no. 2, pp. 257–278.
5. Solomon Feferman,Reflecting on incompleteness,Journal of Symbolic Logic,vol. 56 (1991), no. 1, pp. 1–49.

Authors: Juan Aguilera and Fedor Pakhomov

In his well-known paper [4] Robert Solovay proved that the provability logic of \(\mathsf{PA}\) is the Gödel-Löb logic \(\mathsf{GL}\). Also in the same paper Solovay considered some set-theoretic interpretations of provability logic which lead to stronger provability logics.

Latter Japaridze [3] proved arithmetical completeness theorem for the polymodal provability logic \(\mathsf{GLP}\), where for a modernized version [2] of his result \([n]\phi\) is interpreted as “the sentence \(\phi\) is provable in \(\mathsf{PA}\) extended by all true \(\Pi_n\)-sentences.”

In our work [1] we investigated the set theoretic interpretation of \([n]\), where \([n]\phi\) mean “the sentence \(\phi\) is true in all \(\Sigma_{n+1}\)-correct transitive sets.” Assuming Gödel’s axiom \(V = L\) we prove that the set of polymodal formulas valid under this interpretation is precisely the set of theorems of the logic \(\mathsf{GLP}.3\). Here \(\mathsf{GLP}.3\) is the extension of \(\mathsf{GLP}\) by the axioms of linearity for all \([n]\). We also show that this result is not provable in \(\mathsf{ZFS}\), so the hypothesis \(V = L\) cannot be removed.

As part of the proof, we derive the following purely modal-logical results which are of independent interest: the logic \(\mathsf{GLP}.3\) coincides with the logic of closed substitutions of \(\mathsf{GLP}\), and is the maximal normal extension of \(\mathsf{GLP}\) that doesn’t prove \([n]\bot\), for any \(n\).

Bibliography

1. Juan P. Aguilera and Fedor Pakhomov,The Logic of Correct Models.,arXiv preprints,2402.15382, 20 pages, 2024.
2. L.D. Beklemishev,A simplified proof of arithmetical completeness theorem for provability logic GLP.,Proceedings of the Steklov Institute of Mathematics,274 (2011): 25-33.
3. G.K. Japaridze,The modal logical means of investigation of provability. Thesis in Philosophy,Moscow (in Russian), 1986.
4. Robert M. Solovay,Provability interpretations of modal logic.,Israel Journal of Mathematics,25 (1976): 287-304.

We provide a syntactical translation from poly-modal provability logic \(GLP\) to the Gödel-Löb logic \(GL\). This translation has two parts: first we use a translation similar to the Beklemishev’s translation [1] from \(GLP\) to a subsytem \(J^-\) of \(GLP\), in which the monotonicity axiom \([n] A\to[n+1] A\) is replaced by \([n] A\to [n+i] [n] A\). Then we define a translation which makes nested boxes ascending, i.e. if \([n]\) occurs inside some \([m]\), then \(n\geq m\).

Finally we provide a simple Kripke-style semantics for \(J^-\) which enables us to reprove arithmetical completeness of \(GLP\).

Bibliography

1. L. D. Beklemishev,Kripke semantics for provability logic GLP, Annals of Pure and Applied Logic 161 (2010) 756–774.