Contributed Talks 6
Chair: Joost Joosten
Time allocation: 20 minutes per speaker; 5 minutes for each changeover
Talks in this session
| 14:00 |
Piotr Gruza, Tightness and solidity in fragments of Peano Arithmetic |
|
Theories \(S\) and \(T\) are bi-interpretable if and only if there exist interpretations \(g:S\rhd T\) and \(h:T\rhd S\) such that \(h\circ g\) and \(g\circ h\) are definably isomorphic to identity interpretations (in \(S\) and \(T\) respectively). In some contexts, bi-interpretable theories can be considered equivalent. It was shown by Visser that Peano Arithmetic has the property that no two distinct extensions of it (in its language) are bi-interpretable. Enayat proposed to refer to this property of a theory as tightness and to carry out a more systematic study of tightness and its stronger variants, which he called neatness and solidity. Enayat proved that not only \(\mathrm{PA}\), but also \(\mathrm{ZF}\), \(\mathrm{Z}_{2}\), and \(\mathrm{KM}\) are solid; and on the other hand, that finitely axiomatisable fragments of them are not even tight. Later work by a number of authors (Enayat, Freire, Hamkins, Williams) showed that many natural proper fragments of these theories are also not tight. Enayat asked whether there are proper solid subtheories (containing basic axioms that depend on the theory) of the theories listed above. We answer this question in the case of \(\mathrm{PA}\) by proving that for every \(n\) there exists a solid theory strictly between \(\mathrm{I}\Sigma_{n}\) and \(\mathrm{PA}\). Furthermore, we can require that the theory does not interpret \(\mathrm{PA}\). We also prove some theorems concerning separations between the above notions, e.g. we show that for every \(n\) there exists a tight but not neat theory strictly between \(\mathrm{I}\Sigma_{n}\) and \(\mathrm{PA}\). Joint work with Leszek Kołodziejczyk and Mateusz Łełyk. |
|
| 14:25 |
Mateusz Łełyk, Internal categoricity for schemes |
|
Authors: Mateusz Łełyk and Ali Enayat The talk is devoted to the exposition and explanation of the recent results on the notion of internal categoricity and its various declinations. Within this line of research we aim at understanding how much of the second-order categoricity of various foundational theories (such as Peano Arithmetic, PA or Zermelo-Fraenkel set theory, ZF) can be recovered in the first-order setting? These considerations germinated in the introduction of the concept of internal categoricity of \(\text{PA}\) in full second order logic by Hellman and Parsons, which was followed by Väänänen’s introduction of the notion of internal categoricity of Peano Arithmetic and Zermelo-Fraenkel set theory in the context of Henkin models of second order logic in [6] and in joint work with Wong [5], and later in the context of first order logic, as in [8] and [7]. Internal categoricity has been substantially explored and debated in the philosophical literature, as witnessed by Button and Walsh’s monograph [1], the recent monograph of Maddy and Väänänen [4], and in the recent work of Fischer and Zicchetti [3]. In the talk we argue that the notion of internal categoricity is best seen as a property of schemes, i.e. first-order formulae with a second-order parameter which apply to (first-order) languages returning (first-order) theories. To wit, we prove that each sufficiently strong r.e. theory (in particular: each r.e. extension of PA or ZF) can be axiomatized by a scheme which is not internally categorical. Secondly, we introduce a short hierarchy of categoricity-like notions for schemes which refine internal categoricity and are based on Enayat’s notion of solidity ([2]). Using it we prove two general theorems on the preservation of the appropriate properties by adding the full comprehension and the minimality scheme. As a corollary we are able to derive in a uniform fashion the internal categoricity of the \(n\)-th order arithmetic and Burgess’ extension of the untyped Kripke-Feferman truth theory, KF\(\mu\). Bibliography
|
|
| 14:50 |
Eitetsu Ken, Provability in relativized arithmetics and games with backtracking options |
|
In the realm of propositional proof complexity and bounded arithmetics, the notion of a pebble game gives us a neat way to analyze resolution proof system and \(T^{1}_{2}(R)\). In this talk, towards a deeper understanding of the method, we consider the relativized arithmetic \(I\Sigma_k(X)\) (\(k \geq 1\)) and a game notion corresponding to it and reprove some classical results of ordinal analysis without cut-elimination for \(\omega\)-logic. |
|
| 15:15 |
Léon Probst, Self-referential Gödel numberings and uniformity |
|
In arithmetic, self-reference relies, among other things, on a correct choice of Gödel numbering. Interestingly, one can build self-reference directly into a numbering, which allows us to get the diagonal lemma for free, i.e. bypassing the usual arithmetic of the syntax. For this reason, self-referential numberings are often considered inadequate in a philosophical interpretation of certain metamathematical theorem. However, it is difficult to impose a precise criterion on the numberings (such as monotonicity) to exclude these numberings. Most common criteria fail in this respect or seem unmotivated (cf. [1]). This talk introduces uniformity as a new criterion for numbering. First, we show that standard numberings (on the common conceptions of syntax), as well as other standard codings (e.g. of ordered pairs), are indeed uniform. Second, we show how our criterion excludes the non-standard numberings, including the deviant and self-referential ones. Finally, we discuss its philosophical motivations and some of its implications. Joint work with Balthasar Grabmayr. Bibliography
|
|
| 15:40 |
Philipp Provenzano, Reflection and induction for subsystems of HA |
|
Authors: Philipp Provenzano, Mojtaba Mojtahedi, Fedor Pakhomov and Albert Visser By a classical result of Leivant and Ono [1,2], the subsystem \(\text{I}\Pi_n\) of PA is equivalent to the scheme of uniform reflection \(\text{RFN}_{\Pi_{n+2}}(\text{EA})\) over elementary arithmetic EA. In the present paper, we study the correspondence between the schemes of induction and reflection for subsystems of Heyting arithmetic HA. In an intuitionistic setting, complexity classes of formulas behave quite differently than over classical logic. Underpinning this, we show by an application of realizability that reflection over prenex formulas \(\text{RFN}_{\Pi_\infty}(i\text{EA})\) is equivalent over intuitionistic elementary arithmetic \(i\text{EA}\) to just \(\text{RFN}_{\Sigma_1}(i\text{EA})\) or the totality of hyperexponentiation. More generally, for any class \(\Gamma\supseteq\Sigma_1\) of formulas, we have an equivalence between \(\text{RFN}_{\Pi_\infty\Gamma}(i\text{EA})\) and \(\text{RFN}_{\Gamma}(i\text{EA})\). This phenomenon does not have any counterpart in classical logic where \(\Pi_\infty\) exhausts all arithmetical formulas. As our main result, we show that a suitable generalization of the result by Leivant and Ono holds true intuitionistically. We show for some natural classes \(\Gamma\) of formulas that the principle of induction \(\text{I}\Gamma\) for \(\Gamma\) is equivalent over \(i\text{EA}\) to the reflection principle \(\text{RFN}_{\forall(\Gamma\rightarrow\Gamma)\rightarrow\Gamma}(i\text{EA})\). Here \(\forall(\Gamma\rightarrow\Gamma)\rightarrow\Gamma\) denotes the class of formulas of type \(\forall x. (\phi(x)\rightarrow\psi(x))\rightarrow\theta\) with \(\phi,\psi,\theta\in\Gamma\). This appears as the natural class containing the induction axioms for \(\Gamma\). Note that classically, for \(\Gamma=\Pi_n\), (the universal closure of) this class is just equivalent to \(\Pi_{n+2}\), in harmony with the classical result. Bibliography
|