Contributed Talks 4
Chair: Mateusz Łełyk
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
16:30 
Assylbek Issakhov, Types of minimal numberings with hyperimmune oracles 
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 nondecidable \(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 nondecidable \(A\)computable numberings. Theorem. \(\mathcal F\) has infinitely many pairwise nonequivalent minimal nonpositive \(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


16:55 
Konstantinos Papafilippou, Succinctness of the fixed point theorem for provability logic 
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 formulasize games that were developed in the setting of Boolean function complexity [1] and of firstorder logic and some temporal logics [2]. By now, the formulasize 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'andezDuque 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:
Their result can be easily reformulated to show a succinctness lower bound for formulas in \(\mathcal{L}_{\Diamond}\), thus giving the following: 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 bimodal 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. Bibliography


17:20 
Pablo Dopico, Axiomatic theories of supervaluationist truth: completing the picture 
In [1], Kripke proposed to carry out his fixedpoint 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 fixedpoint 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 prooftheoretic 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 prooftheoretic strength, which equals that of VF. The most substantial part of the paper, however, is dedicated to the theory which axiomatizes the fixedpoint semantic theory over mc. We provide a prooftheoretic 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 prooftheoretically equivalent to RA\(_{<\varepsilon_0}\). Hence, we conclude that VFM is prooftheoretically much weaker than the rest of theories of the supervaluationist family, and indeed on a par with the wellknown 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 prooftheoretic analysis for this theory, which confirms that this schematic reflective closure as prooftheoretically strong as the theory RA\(_{<\Gamma_0}\). This is joint work with Daichi Hayashi. Bibliography


17:45 
Fedor Pakhomov, The Logic of Correct Models 
Authors: Juan Aguilera and Fedor Pakhomov In his wellknown paper [4] Robert Solovay proved that the provability logic of \(\mathsf{PA}\) is the GödelLöb logic \(\mathsf{GL}\). Also in the same paper Solovay considered some settheoretic 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 modallogical 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


18:10 
Mojtaba Mojtahedi, A translation from GLP into GL 
We provide a syntactical translation from polymodal provability logic \(GLP\) to the GödelLö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 Kripkestyle semantics for \(J^\) which enables us to reprove arithmetical completeness of \(GLP\). Bibliography
