Logic Colloquium 2024, the annual European Summer Meeting of the Association of Symbolic Logic, took place at the University of Gothenburg, June 24 through June 28, 2024. The conference was held in person at the Humanisten Building of the University of Gothenburg with 190 registered participants, including 70 students. ASL travel grants were awarded to 41 graduate students and recent PhDs.

Funding for the conference was provided by the Association for Symbolic Logic; the Royal Society of Arts and Sciences in Gothenburg; the Royal Swedish Academy of Sciences and G.S. Magnuson Foundation; the Knut and Alice Wallenberg Foundation; the National Science Foundation of the United States; and the Department of Philosophy, Linguistics, and the Theory of Science as well as the Centre for Linguistic Theory and Studies in Probability, both at the University of Gothenburg.

The success of the meeting owes a great deal to the excellent work of the Local Organizing Committee chaired by Bahareh Afshari and composed of Giacomo Barlucchi, Rasmus Blanck, Gianluca Curzi, Fredrik Engström, Tjeerd Fokkens, Mattias Granberg Olsson, Martin Kaså, Graham Leigh, Ivan Di Liberti, Orvar Lorimer Olsson and Dominik Wehr.

The Program Committee was chaired by Ulrich Kohlenbach (Darmstadt, Germany) and consisted of Bahareh Afshari (Gothenburg, Sweden), Gal Binyamini (Jerusalem, Israel), Natasha Dobrinen (Notre Dame, USA), Keng Meng Ng (Singapore), Francesca Poggiolesi (Paris, France), Mehrnoosh Sadrazadeh (London, UK), Reed Solomon (Connecticut, USA) and Szymon Toruńczyk (Warsaw, Poland).

The program included three tutorial courses, seven plenary lectures, eighteen invited lectures in six special sessions (applied model theory; computable structures; logic, language and computation; logic in philosophy; proof theory; and set theory), the Thirty-Fifth Gödel lecture, and 106 contributed talks. The Gödel lecture (Un)decidability in fields was given by Thomas Scanlon (University of California Berkeley). The following tutorial courses were given.

Anuj Dawar (University of Cambridge), Model theory of tame classes of finite structures.

Alberto Marcone (Universitá di Udine), WQOs and BQOs in logic.

Andrei Sipoş (University of Bucarest), An exploration of proof mining.

The following invited plenary lectures were presented.

Daisuke Bekki (Ochanomizu University), From dependent types to natural language semantics.

Johanna Franklin (Hofstra University), Structural highness notions.

James Freitag (University of Illinois at Chicago), When any three solutions are independent.

Marianna Girlando (University of Amsterdam), Proof systems and decision algorithms for intuitionistic K.

Stephen Jackson (University of North Texas), Recent advances in the combinatorics of determinacy models.

Leszek Kołodziejczyk (University of Warsaw), Models of arithmetic that satisfy more collection than induction.

Paul-André Melliès (Université Paris Denis Diderot), Recent advances in higher-order automata and profinite lambda calculus.

Abstracts of invited and contributed talks by members of the Association follow.

For the Program Committee

Ulrich Kohlenbach

Abstract of the invited 35th Annual Gödel Lecture

▸THOMAS SCANLON, (Un)decidability in fields.

Department of Mathematics, University of California Berkeley, Berkeley, CA, USA.

E-mail: scanlon@math.berkeley.edu.

From Tarski’s 1929 proof of the decidability of the first-order theory of the field of real numbers and Robinson’s 1949 proof of the complementary theorem that theory of the rational numbers is undecidable, the boundary between theories of fields with decidable or undecidable theories has remained unclear. Many more examples are known on both sides of the divide. Generally, the proofs mix ideas from logic, arithmetic, and geometry. The notable test case of theory of the field of rational functions in one variable over the complex numbers was explicitly raised in print in 1963 but remains open to this day.

I will discuss the history of this problem, will describe some recent work, and will explain why its resolution has been difficult.

Abstract of invited tutorials

▸ANUJ DAWAR, Model theory of tame classes of finite structures.

Department of Computer Science and Technology, University of Cambridge, U.K.

E-mail: anuj.dawar@cl.cam.ac.uk.

URL Address: https://www.cst.cam.ac.uk/people/ad260.

The class of finite structures is a notoriously ill-behaved one from the point of view of model theory. In the early years of this century, this led to the study of subclasses of this class which exhibit better behaviour. The focus was on classes defined by the sparsity of their underlying Gaifman graph. Such sparse classes were shown to be well-behaved in model-theoretic and algorithmic terms. A review of the work on this, as of 2007 can be found in [2]. The good behaviour discussed there focussed on two aspects: that such classes show preservation properties that fail on the class of finite structures, and evaluation of first-order formulas is algorithmically tractable in such classes. A common theme is the use of the locality of first-order logic which, in the absence of compactness, is a key tool of finite model theory. The line of work on the algorithmic evaluation of first-order formulas in sparse classes culminated in the result of Grohe et al. on nowhere-dense classes of structures [3]. More recent work has sought to extend this work to classes of finite structures that are not sparse, and identify tame classes of dense structures. This has seen a convergence with notions of tameness coming from stability theory (see, for example, [1]).

In this tutorial, I review the use of locality in identifying tame classes; discuss the tameness of some sparse classes; and present some recent extensions to dense classes and the connections with stability. I prove the results for illustrative examples of classes.

[1] S. Braunfeld, A. Dawar, I. Eleftheriadis, and A. Papadopoulos, Monadic NIP in monotone classes of relational structures, 50th International Colloquium on Automata, Languages, and Programming (Paderborn, Germany) (K. Etessami, U. Feige, and G. Puppis, editors), Schloss Dagstuhl, 2023, pp. 119:1–119:18.

[2] A. Dawar, Finite model theory on tame classes of structures, International Symposium on Mathematical Foundations of Computer Science (L. Kučera and A. Kučera, editors), Lecture Notes in Computer Science, vol. 4708, Springer, 2007, pp. 2–12.

[3] M. Grohe, S. Siebertz and S. Kreutzer Deciding first-order properties of nowhere dense graphs. Journal of the ACM , vol. 64 (2017), no. 3, pp. 17:1–17:32.

▸ALBERTO MARCONE, WQOs and BQOs in logic.

Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine, via delle Scienze 206, 33100 Udine, Italy.

E-mail: alberto.marcone@uniud.it.

The notion of well quasi-order (WQO) is a natural generalization of well-orders to partial orders. Simply put, a partial order is a WQO if it is well-founded and all its antichains are finite. Several equivalent characterizations of WQO show that the notion is actually quite robust.

In the 1960s Nash–Williams introduced a strengthening of WQO he called better quasi-order (BQO). This was instrumental in Laver’s 1971 proof of Fraïssé’s conjecture: the collection of countable linear orders is a WQO under embeddability. In fact all proofs of Fraïssé’s conjecture actually establish Laver’s stronger statement: countable linear orders are a BQO under embeddability.

This survey assumes no previous knowledge of WQOs and BQOs: we will start from the definitions and the basic characterizations, then move on to some sample results. We will pay attention to the logic side of the theory, looking at WQO and BQO theory from the viewpoint of ordinal analysis, reverse mathematics and Weihrauch reducibility. For example, it turns out that many proofs and proof techniques in this area require quite strong axioms.

▸ANDREI SIPOŞ, An exploration of proof mining.

Facultatea de Matematic $\check{\mathrm{a}} $ şi Informatic $\check{\mathrm{a}} $ , Universitatea din Bucureşti, Bucureşti, Rom $\check{\mathrm{a}} $ nia.

E-mail: andrei.sipos@fmi.unibuc.ro.

Proof mining is a research paradigm connected to mathematical logic that aims to analyze concrete proofs in mainstream mathematics using tools originating in proof theory in order to reveal information which is not immediately apparent. This information may be qualitative, like eliminating premises, quantitative, like the determination of witnesses and bounds for existentially quantified variables, or mixed, like the uniformity of the latter quantities with respect to parameters of the problem. The paradigm originated with Georg Kreisel in the 1950s and reached its current mature form within the school of Ulrich Kohlenbach.

I aim to briefly present the theoretical underpinnings of proof mining but largely adopt a hands-on approach via focusing on a plethora of increasingly complex case studies, of which I mention Ulrich Berger’s didactic example for the classical Herbrand theorem, Terence Tao’s finite monotone convergence principle, my own analysis of a convergence theorem on the unit interval due to D. Borwein and J. Borwein, and the finitary content of sunny nonexpansive retractions (joint work with U. Kohlenbach).

Abstracts of invited plenary lectures

▸JOHANNA FRANKLIN, Structural highness notions.

Department of Mathematics, Hofstra University, Room 306, Roosevelt Hall, Hempstead, NY 11549-0114, USA.

E-mail: johanna.n.franklin@hofstra.edu.

In computability theory, highness indicates maximal computational strength. We will develop the theory of highness in the context of computable structure theory. First, we will present some general results, and then we will turn to highness for structures such as Harrison orders and ill-founded linear orders. Finally, we will discuss the way the relationships between these concepts change when we restrict the functions that we use to find these isomorphisms.

This work is joint with Wesley Calvert and Dan Turetsky.

▸JAMES FREITAG, When any three solutions are independent.

Department of Mathematics, Statistics and Computer Science, University of Illinois at Chicago, Chicago, IL, USA.

E-mail: freitagj@gmail.com.

What can one prove in general about the algebraic relations between solutions of a differential equation? In this talk, we’ll talk about recent work in this direction connecting the problem to group-theoretic conjectures. We’ll also discuss the more general program of making quantitative several aspects of forking and indiscernible sequences. This work describes joint work with Rahim Moosa and Scott Mutchnik.

▸MARIANNA GIRLANDO, Proof systems and decision algorithms for intuitionistic K.

Institute for Logic, Language and Computation, University of Amsterdam, Amsterdam, Netherlands.

E-mail: m.girlando@uva.nl.

Proof systems can be used to define decision algorithms for a given logic, that is, automated procedures establishing whether a formula is valid or not within the logic. Such algorithms implement exhaustive and terminating root-first proof search for the formula in the calculus. If a proof is found the formula is valid. Otherwise, one can usually construct a countermodel for the formula at the root from a finite branch of a failed proof search tree. In the literature, proof-theoretic decision procedures have been defined for intuitionistic logic, using (among other) sequent calculi and labelled calculi. Similarly, decidability of modal logics has (also) been proven by implementing terminating proof search for nested calculi for the logics.

In this talk we consider intuitionistic modal logic IK. This logic is the intuitionistic variant of modal logic K proposed by Fisher Servi, Plotkin and Stirling, and studied by Simpson. Semantically, the logic is characterised by bi-relational frames, comprising a preorder relation, as in intuitionistic possible-worlds models, and a binary relation, representing the modal accessibility relation.

We shall present two proof systems for the logic: a fully labelled sequent calculus, explicitly representing the two relations of IK-models, and a bi-nested calculus, having one syntactic connective for each relation. After introducing the proof systems, we will discuss and compare the corresponding decision algorithms, defined by implementing terminating proof search in the two calculi.

This talk is based on joint work with Han Gao, Roman Kuznets, Sonia Marin, Marianela Morales, Nicola Olivetti, and Lutz Straßburger.

▸STEPHEN JACKSON, Recent advances in the combinatorics of determinacy models.

Department of Mathematics, University of North Texas, Denton, TX, USA.

E-mail: stephen.jackson@unt.edu.

We present several recent results in determinacy theory, in particular results around the ABCD conjecture which describes the comparison of cardinalities of the form $A^B$ where A, B are wellordered cardinals. In joint work with Chan and Trang we showed that if $\kappa $ is a weak partition cardinal then $\kappa ^{<\kappa }$ does not inject into $ON^{\epsilon }$ for any $\epsilon <\kappa $ , which establishes the conjecture at such $\kappa $ . We introduce generalized infinity Borel sets and discuss their relation to the conjecture, and then discuss Chan’s recent solution to the ABCD conjecture from AD $^+$ .

▸LESZEK KOŁODZIEJCZYK, Models of arithmetic that satisfy more collection than induction.

Institute of Mathematics, University of Warsaw, Poland.

E-mail: lak@mimuw.edu.pl.

Consider a model $\mathbb {M}$ of some amount of arithmetic, say induction for bounded formulas and the totality of the exponential function. This could be a structure in the basic language of ordered rings $\{+,\cdot , 0,1, \le \}$ or in $\{+,\cdot , 0,1, \le \} \cup \{A_1,\ldots ,A_k\}$ for some finite number of unary predicates $A_i$ that can be treated as “oracles”. The latter case has become important in recent decades due e.g. to its relevance for reverse mathematics: we may want to expand $\mathbb {M}$ by adding more oracle predicates to the language and eventually declare all the $A_i$ to be bona fide objects of a “second-order” sort, turning $\mathbb {M}$ into a model of some fragment of second-order arithmetic. This is a very natural technique in the study of the first-order strength of second-order arithmetic theories.

If $\mathbb {M}$ does not satisfy the full induction scheme in its language—in the language of ordered rings, that would be Peano Arithmetic—then exactly one of two things must hold. Either there is $n \ge 0$ such that $\mathbb {M}$ satisfies $\Sigma ^0_n$ -induction, $\mathrm {I}\Sigma ^0_n$ , but not the $\Sigma ^0_{n+1}$ -bounding (or collection) scheme, $\mathrm {B}\Sigma ^0_{n+1}$ , i.e.,

for $\Sigma ^0_{n+1}$ formulas $\psi $ ; or there is $n \ge 1$ such that $\mathbb {M}$ satisfies $\mathrm {B}\Sigma ^0_n$ but not $\mathrm {I}\Sigma ^0_{n}$ . Sometimes, one refers to models of the first kind as I-models and to those of the second kind as B-models.

A typical example of an I-model is a nonstandard pointwise $\Sigma ^0_n$ -definable one, i.e., one in which every singleton subset can be defined by a $\Sigma ^0_n$ formula without using parameters. Not every I-model is elementarily equivalent to a pointwise $\Sigma ^0_n$ -definable one, but the example is canonical at least in the following sense: every countable model of $\Sigma ^0_n$ -induction can be expanded (by adding a new oracle predicate) to a pointwise $\Sigma ^0_n$ -definable model. (This is implicit in a theorem proved in 2015 by Towsner.).

B-models, on the other hand, are not particularly well-understood and have a number of surprising properties. For example, it has been known since the 1990's that each countable B-model has continuum many automorphisms. Moreover, no B-model admits a definable injection from the universe into a bounded initial segment, regardless of the complexity of the definition. Neither of these things is true in a pointwise definable model. More recently, some results have emerged showing that, in contrast to the case of I-models, the possibilities of expanding a B-model so that the expanded structure remains a B-model are quite restricted.

In my talk, I will discuss some old and new results on the specific features of B-models, as well as some open problems. The emphasis will be on countable models and on features that have relevance to proof-theoretic issues such as provability and conservativity.

▸PAUL-ANDRÉ MELLIÈS, Recent advances in higher-order automata and profinite lambda calculus.

Laboratoire IRIF, Department of Computer Science, Université Paris Cité, Paris, France.

E-mail: mellies@irif.fr.

Abstracts of invited talks in the Special Session on Applied Model Theory

▸VINCENT BAGAYOKO, Ordered groups of regular growth rates.

Institut de Mathématiques de Jussieu-Paris Rive Gauche, Université Paris Cité, Paris, France.

E-mail: bagayoko@imj-prg.fr.

This talk will regard some first-order properties of ordered groups of germs of functions that are definable in an o-minimal structure. I will describe my progress toward finding a tame first-order theory of some of these groups, and give some elements of valuation theory on these ordered groups.

▸ANNA DMITRIEVA, Generic functions and quasiminimality.

School of Mathematics, University of East Anglia, United Kingdom.

E-mail: a.dmitrieva@uea.ac.uk.

In 2002, Zilber introduced the theory of a generic function on a field [4], coinciding with the limit theory of generic polynomials from [2]. Axiomatized in first-order logic by a version of the Schanuel property and existential closedness, this theory turns out to be $\omega $ -stable. As shown by Wilkie [3] and Koiran [1], one can explicitly construct such a generic function on the complex plane in a form of a Taylor series, using the ideas behind Liouville numbers.

In this talk, we look further into the properties of the theory of generic functions. As the main result, we show that adding any of these generic functions to the complex plane gives an isomorphic structure, which ought to be quasiminimal, i.e., any definable subset has to be countable or cocountable. Thus we obtain a non-trivial example of an entire function which keeps the complex field quasiminimal.

[1] P. Koiran, The theory of Liouville functions. The Journal of Symbolic Logic , vol. 68 (2003), no. 2, pp. 353–365.

[2] , The limit theory of generic polynomials, Logic Colloquium 2001 (Vienna, Austria) (M. Baaz, S.-D. Friedman, and J. Krajiček, editors), Lecture Notes in Logic, vol. 20, AK Peters, 2005, pp. 242–254.

[3] A. J. Wilkie, Liouville functions, Logic Colloquium 2000 (Paris, France) (R. Cori, A. Razborov, S. Todorčević, and C. Wood, editors), Lecture Notes in Logic, 19, AK Peters, 2005, pp. 383–391.

[4] B. Zilber, A theory of a generic function with derivations, Logic and Algebra (Y. Zhang, editor), Contemporary Mathematics, vol. 302, American Mathematical Society, 2002, pp. 85–99.

▸ADELE PADGETT, O-minimal definitions of the complex $\Gamma $ and Riemann $\zeta $ functions.

Kurt Gödel Research Center, Department of Mathematics, University of Vienna, Austria.

E-mail: adele.lee.padgett@univie.ac.at.

In this talk, I will discuss joint work with P. Speissegger in which we prove that the $\Gamma $ function and Riemann’s $\zeta $ function are o-minimal on certain unbounded complex domains. I will also discuss some applications of this result.

Abstracts of invited talks in the Special Session on Computable Structures

▸DAVID GONZALEZ, Semi-periodic functions and the Scott analysis of linear orderings.

Department of Mathematics, University of California Berkeley, Berkeley, CA, USA.

E-mail: david.gonzalez@berkeley.edu.

The concept of Scott complexity was introduced by Alvir, Greenberg, Harrison-Trainor and Turetsky and gives a way of assigning countable structures to elements of the Borel hierarchy that correspond to their descriptive complexity. This concept refines the previous notions of Scott rank. In computable structure theory, Scott analysis refers to a wide variety of pursuits related to the concepts of Scott rank and Scott complexity. For example, it is typical to study the sorts of Scott ranks and Scott complexities that can appear in a given class of structures or the sorts of structures from a class that can have a given Scott rank or Scott complexity.

I will describe recent work that solves a number of open questions regarding the Scott analysis of linear orderings (and of structures in general). Central to this work is a new construction of a linear ordering given a so-called semi-periodic function. We will discuss this construction and how to use the combinatorial structure of semi-periodic functions to extract Scott analytic facts about their corresponding linear orderings.

This talk is based on joint work with Turbo Ho and Matthew Harrison-Trainor.

▸MATTHEW HARRISON-TRAINOR, Interpretations, back-and-forth games, and group von Neumann algebras.

Department of Mathematics, Statistics and Computer Science, University of Illinois Chicago, Chicago, IL, USA.

E-mail: mht@uic.edu.

When defining the Ehrenfreucht–Fraisse back-and-forth games, it is common for model theorists to say that each player plays a single element at a time, while many computability theorists will often say that each player can play a tuple of arbitrary length. Both versions of these games appeared in Ehrenfreucht’s first treatment of back-and-forth games. However the two versions of the games can behave very differently, in particular by how they transfer through constructions like the construction from a ring R of the polynomial ring $R[x]$ . I will talk about some interesting aspects about the differences between the two versions of the back-and-forth games, and when one might use each one. One interesting example, from joint work with Isaac Goldbring, is the construction from a group of its group von Neumann algebra.

▸MENG-CHE “TURBO” HO, Decision problems for groups as equivalence relations.

Department of Mathematics, California State University Northridge, CA, USA.

E-mail: turbo.ho@csun.edu.

In 1911, Dehn proposed three decision problems for finitely presented groups: word problem, conjugacy problem, and isomorphism problem. These problems have been central to both group theory and logic, and were each proven to be undecidable in the 50s. There is much current research studying the decidability of these problems in classes of groups.

Although these problems are classically studied as decision problems, each of them is naturally an equivalence relation. In this talk, we study them as equivalence relations and compare them using computable reductions. This leads to a more refined measure of their complexity and brings new results and questions.

Parts of the talk are joint works with Uri Andrews, Matthew Harrison-Trainor, and Luca San Mauro.

Abstracts of invited talks in the Special Session on Logic, Language and Computation

▸KRISTINA LIEFKE, Reduction and unification in (typed) natural language ontology.

Department of Philosophy II, Ruhr University Bochum, Germany.

E-mail: Kristina.Liefke@ruhr-uni-bochum.de.

Natural language semantics uses many different kinds of objects, incl. individuals, propositions, properties, situations, events, and kinds. Simple type theories tame this ‘zoo’ [1] by assuming only a small number of primitive objects (e.g., individuals, situations), and obtaining all other objects via constructions out of these primitives. By distinguishing subtypes (or sorts), these theories straightforwardly obtain more finely-grained types (e.g., concrete vs. abstract individuals), allowing them to explain selectional restrictions (e.g., eat $\{^{\checkmark }$ an apple, $^{\#}$ an opinion $\}$ ) (i). However, this strategy blocks an easy account of selectional flexibility (i.e., why some predicates accept different-type arguments; e.g., remember $\{$ the girl, that she was dancing $\}$ ) (ii) and of semantic relations between such arguments (e.g., why remember that she $\ldots $ entails remember the girl) (iii).

My talk answers this challenge by unifying intuitively distinct types in a single higher-rank type, whose objects code the lower-type objects (see [2, 3, 4]). This unification allows the same-type interpretation of expressions from different grammatical categories, immediately explaining (ii) and—through the internal structure of the new objects—(iii). Selectional restrictions (see (i)) are explained through the particular lexical semantics of the embedding predicate and its interaction with the new, higher-type object.

[1] E. Bach, Natural language metaphysics, Logic, Methodology and Philosophy of Science VII (R. B. Marcus, editor), Elsevier, 1986, pp. 573–593.

[2] K. Liefke, Modelling selectional super-flexibility. Semantics and Linguistic Theory , vol. 31 (2021), pp. 324–344.

[3] K. Liefke and M. Werning, Evidence for single-type semantics. Journal of Semantics , vol. 35 (2018), no. 4, pp. 639–685.

[4] N. Theiler, F. Roelofsen, and M. Aloni, A uniform semantics for declarative and interrogative complements. Journal of Semantics , vol. 35 (2018), no. 3, pp. 409–466.

▸ZHAOHUI LUO, Common nouns as types: higher inductive types in type-theoretical semantics.

Department of Computer Science, Royal Holloway, University of London, United Kingdom.

E-mail: zhaohui.luo@hotmail.co.uk.

As pointed out by Geach and others, common nouns (CNs) are special in that they have their own criteria of identity (ICs) [3]. In type-theoretical semantics, this provides a justification for the idea of interpreting CNs as types and the ICs as equivalence relations over the types, i.e., the pairs called setoids [5]. However, there is a discrepancy here in the CNs-as-types paradigm: setoids are pairs, not types. Although in most cases ICs are ‘commonly understood’ and can hence be ignored, they cannot be so ignored in sophisticated cases where it is only adequate to interpret CNs as setoids [1, 6]. Furthermore, it is known that in practice working with setoids is inconvenient and direct treatments of quotient types are called for. The recent study of Higher Inductive Types [7, 4, 2], as a development in the research on Homotopy Type Theory as a foundational language of mathematics, has opened up a new avenue and, in particular, it enables the study of quotient types from a fresh angle with much needed computational justification of the resulting type theory. If time permits, I’ll also discuss some related ongoing research topics, albeit only briefly.

[1] S. Chatzikyriakidis and Z. Luo, Formal Semantics in Modern Type Theories , Wiley, 2020.

[2] T. Coquand, S. Huber, and P. Mortberg, On higher inductive types in cubical type theory, Proceedings of the 33rd Symposium on Logic in Computer Science (Oxford, UK) (A. Dawar and E. Grädel, editors), Association for Computing Machinary, 2018, pp. 255–264.

[3] P. Geach, Reference and Generality , Cornell University Press, 1962.

[4] P. Lumsdaine and M. Shulman, Semantics of higher inductive types. Mathematical Proceedings of the Cambridge Philosophical Society , vol. 169 (2020), pp. 159–208.

[5] Z. Luo, Common nouns as types, Logical Aspects of Computational Linguistics (LACL’2012) (Nantes, France) , (D. Bechet and A. Dikovsky, editors) Lecture Notes in Computer Science, vol. 7351, Springer, 2012, pp. 173–185.

[6] , Modern Type Theories: Their Development and Applications , Tsinghua University Press, 2024.

[7] Univarient Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics , Institute for Advanced Study, 2013.

▸PETER R. SUTTON, The challenge of polysemy for natural language semantics.

Department of Translation and Language Sciences, University of Pompeu Fabra, Barcelona, Spain.

E-mail: peter.r.sutton@icloud.com.

Polysemous nouns have closely related senses that denote different types of entities. For instance lunch can denote an eventuality (eating lunch) or a physical entity (the food eaten). Furthermore, polysemous nouns can be felicitous in copredication constructions such as (1) that arguably elicit both of these senses simultaneously.

1. (1) Lunch was delicious and lasted for two hours.

Data such as (1) have been claimed to pose a problem for canonical approaches to formal semantics in the Frege–Church–Montague tradition (see e.g., Chomsky 2000). For instance, given an assumption that lunch eating events and food are members of the domains of different semantic types, it can be shown that there is no set characterisable in simply typed lambda calculus that has as members entities that are lunch-eating eventualities and/or food.

This talk looks at two responses to the challenge of polysemy. A large number of analyses of polysemy go for an enrichment of the type theory, and so add structure. A lesser known option, I suggest, is to impoverish the type theory. This can be implemented within a mono-typed semantics as developed in e.g., Liefke 2014, Liefke & Werning 2018. However, I suggest there are reasons for why the latter approach still needs to make use of the kind of extra structure utilised by the former, even if this is not introduced in the type theory. I then discuss how distinct these two approaches may turn out to be.

Abstracts of invited talks in the Special Session on Logic in Philosophy

▸AGATA CIABATTONI, Normative reasoning: from Sanskrit philosophy to AI.

Institute of Logic & Computation, Technische Universität Wien, Austria.

E-mail: agata@logic.at.

URL Address: https://mimamsa.logic.at/.

URL Address: https://taiger.logic.at/.

Normative statements, which involve concepts such as obligation and prohibition, are enormously important in a variety of fields, from law and ethics to artificial intelligence. Reasoning with and about them requires deontic logic, which is a quite recent area of research. By contrast, for more than two millennia, one of the most important systems of Indian philosophy focused on analyzing normative statements. Mīmāṃsā, as it is called, looks at these statements found in the Vedas, the sacred texts of (what it is now called) Hinduism, and interprets them by explaining precisely what course of action they require. This talk will describe the findings from the research project Reasoning Tools for Deontic Logic and Applications to Indian Sacred Texts (with Elisa Freschi) on the deontic reasoning of Mīmāṃsā, and preliminary ideas on how to apply them to design autonomous agents sensitive to legal, social and ethical norms, see the research project TAIGER: Training and Guiding AI Agents with Ethical Rules (with Ezio Bartocci and Thomas Eiter).

The results I will present arise from a collaboration between logicians, sanskritists and computer scientists.

▸ANDRZEJ INDRZEJCZAK, Do theories of definite descriptions support Anselm’s God?.

Department of Logic, University of Lodz, Poland.

E-mail: andrzej.indrzejczak@filhist.uni.lodz.pl.

We examine the relationship between the ontological argument, in its original version provided by Anselm in Proslogion II, and theories of definite desriptions. Anselm’s ontological arguments, and its later variants proposed by such eminent philosophers as Descartes or Leibniz, still belong to the most discussed themes in the field of philosophy and theology. An advent of interest in these arguments in XXth century, among logicians and analytical philosophers, has thrown a new light on their structure and value. The prevailing approach to their formalisation is based on the application of modal logic, as in the works of Malcolm [3], Hartshorne [2], or Plantinga [6]. However, it seems that at least in the case of the version of the ontological argument formulated in Proslogion II, the crucial elements are contained in the description of God provided by Anselm. Therefore, following Barnes [1] or Oppenheimer and Zalta [4, 5], we take as our basic assumption that the proper analysis of the Anselm’s argument should use some logic of definite descriptions. In fact, several theories of definite descriptions were developed and the problem is: which of them is the most suitable tool for its formalisation and evaluation.

This project is funded by the European Union (ERC, ExtenDD, project number: 101054714). Views and opinions expressed are however those of the author(s) only and do not necessarily reflect those of the European Union or the European Research Council. Neither the European Union nor the granting authority can be held responsible for them.

[1] J. Barnes, The Ontological Argument , Macmillan, 1972.

[2] C. Hartshorne, Anselm’s Discovery , Open Court 1965.

[3] N. Malcolm, Anselm’s ontological arguments. The Philosophical Review , vol. 69 (1960), pp. 41–62.

[4] P. E. Oppenheimer and E. N. Zalta, On the logic of the ontological argument. Philosophical Perspectives , vol. 5 (1991), pp. 509–529.

[5] , A computationally-discovered simplification of the ontological argument, Australasian Journal of Philosophy , vol. 89 (2011), pp. 333–349.

[6] A. Plantinga, The Nature of Necessity , Oxford University Press 1974.

▸JOHANNES STERN, Truth, conditionals, and hyperintensionality.

Department of Philosophy, University of Bristol, United Kingdom.

E-mail: johannes.stern@bristol.ac.uk.

Tarski taught us that we cannot have both, a classical, semantically closed language and an adequate definition of truth. Kripke taught us that we can define a truth predicate for a semantically closed language, if we are willing to embrace a subclassical logic (at least on the sentential level). Yet, Tarski’s ghost is still with us, as these subclassical logics do not possess an attractive conditional connective, that is, a conditional that enables us to “carry on sustained ordinary reasoning”. In this talk we show how conditionals can be added to subclassical logics, in particular strong Kleene logic $\mathsf {K3}$ and investigate the costs and consequences of such an addition. This leads us to a discussion of hyperintensionality in logics and truth theories.

Abstracts of invited talks in the Special Session on Proof Theory

▸VALENTIN BLOT, Variants of bar recursion and their uses.

École Normale Supérieure Paris–Saclay, Gif-sur-Yvette, France.

E-mail: contact@valentinblot.org.

Bar recursion was invented by Spector to provide a proof of consistency for analysis via an extension of Gödel’s Dialectica interpretation to the axiom scheme of comprehension. Since then, several variants of this operator have been defined in various contexts, to provide computational content to diverse logical principles.

In this talk I will present various forms of bar recursion in the setting of the realizability and Dialectica interpretations. I will show how these operators give computational content to principles such as the double-negation shift, the axiom of choice in a classical setting, and the comprehension axiom of arithmetic.

▸LUKAS MELGAARD, Cyclic versions of arithmetic theories with inductive definitions.

School of Computer Science, University of Birmingham, United Kingdom.

E-mail: lxm402@student.bham.ac.uk.

We investigate the cyclic proof theory of extensions of Peano Arithmetic by (finitely iterated) inductive definitions. Such theories are essential to proof theoretic analyses of certain ‘impredicative’ theories; moreover, our cyclic systems naturally subsume Simpson’s Cyclic Arithmetic.

Our main result is that cyclic and inductive systems for arithmetical inductive definitions are equally powerful. We conduct a metamathematical argument, formalising the soundness of cyclic proofs within second-order arithmetic and appealing to conservativity. This approach is inspired by those of Simpson and Das for Cyclic Arithmetic, however we must further address a difficulty that the closure ordinals of our inductive definitions (around Church-Kleene) far exceed the proof theoretic ordinal of the appropriate metatheory (around Bachmann-Howard or Bucholz), and so explicit induction on their notations is not possible. For this reason, we rather rely on a formalisation of the theory of (recursive) ordinals within second-order arithmetic.

▸TAKAKO NEMOTO, Recursion thoery over intuitionistic logic.

Graduate of Information Sciences, Tohoku University, 6-3-09 Aoba, Aramaki-aza Aoba-ku, Sendai, 980-8579, Japan.

E-mail: nemototakako@gmail.com.

It is known that basic part of recursion theory, such as recursion theory, smn-theorem, recursion theorem and normal form theorem can be formalized in $\mathbf {HA}$ [2, Chapter 3.7].

The aim of this talk is to do recursion theory itself more in constructive mathematics. One of the problem is the treatment of complements of sets of natural numbers over intuitionistic logic. In this talk, we adopt the notion of complemented sets by [1, Chapter 3] and try to develop degree theory.

[1] E. Bishop and D. Bridges, Constructive Analysis , Springer-Verlag, 1980.

[2] A. Troelstra and D. van Dalen, Constructivism in Mathematics Volumes I , Studies in Logic and the Foundations of Mathematics, Elsevier, 1988.

Abstracts of invited talks in the Special Session on Set Theory

▸CLAUDIO AGOSTINI, The key properties of metrizability for (generalized) descriptive set theory.

Institut für Diskrete Mathematik und Geometrie, Technische Universität Wien, Wiedner Hauptstraße 8-10/104, 1040 Vienna, Austria.

E-mail: claudio.agostini@tuwien.ac.at.

Metrizable spaces are one of the most important concepts in many areas of mathematics (and descriptive set theory is no exception).

For this reason, the quest for characterizing metrizability has always risen a lot of interest, leading to results like Urysohn metrization theorem, Nagata–Smirnov–Bing metrization theorem, Arhangel’skij metrization theorem, and more.

These theorems highlight what are the fundamental topological properties that grant the nice behaviour of metric spaces. These properties, in turn, can be used in generalized descriptive set theory to define new classes of non-first-countable (and thus, non-metrizable) topological spaces. Then one can extend results from classical descriptive set theory about Polish spaces to these new classes of spaces.

In this talk, I will present different characterizations of metrizability. This includes a new (to the best of our knowledge) characterization of metrizability in terms of a topological game. Then I will introduce the respective classes of spaces generated by these theorems in the uncountable setting, and compare them up to homeomorphism and up to $\kappa ^+$ -Borel isomorphism.

This is a joint work with Luca Motto Ros.

▸TAMÁS KÁTAY, Generic properties of groups.

Department of Mathematics, Eötvös Loránd University, Budapest, Hungary.

E-mail: 13heted@gmail.com.

Generic properties (in the sense of Baire category) have been intensively studied in various spaces of mathematical objects. In this talk, I present an overview of the generic properties of groups. More specifically, we focus on two important cases: countably infinite (discrete) groups and compact metrizable groups.

In the space of countably infinite groups, there is no comeager isomorphism class. However, we characterize groups that occur in comeager many groups as subgroups. We also identify further generic properties. In contrast to the general case, the isomorphism class of $\bigoplus _{i \in \mathbb {N}}(\mathbb {Q}/\mathbb {N})$ is comeager among all countably infinite abelian groups. Also, the isomorphism class of the additive group of the rationals is comeager among all countably infinite torsion-free abelian groups.

Regarding compact metrizable groups in general, only partial results are known. However, if we restrict our attention to abelian groups, a very clear picture emerges. The isomorphism class of the countably infinite power of the so-called universal odometer is comeager. If we restrict our attention further to connected groups, we find that the isomorphism class of the so-called universal solenoid is comeager.

▸CHRIS LAMBIE-HANSON, Guessing models, cardinal arithmetic, and ultrafilters.

Institute of Mathematics, Czech Academy of Sciences, Žitná 25, Prague 1, 115 67, Czech Republic.

E-mail: lambiehanson@math.cas.cz.

Guessing models were introduced by Viale and Weiß in the course of their investigations into the consistency strength of the Proper Forcing Axiom ( $\mathsf {PFA}$ ). It quickly became apparent that guessing models are powerful tools for obtaining instances of compactness, and over the last fifteen years they have seen numerous applications. For example, results Weiß and of Viale indicate that the existence of guessing models implies the failure of relatively weak square principles, and results of Viale and of Krueger combine to show that the existence of guessing models implies the Singular Cardinals Hypothesis ( $\mathsf {SCH}$ ).

In this talk, we present two recent applications of guessing models. In the first, we pursue further investigations into the impact of guessing models on cardinal arithmetic. We show, for instance, that the existence of guessing models tightly correlates the values of $2^{\aleph _0}$ and $2^{\aleph _1}$ , and also that the existence of guessing models implies Shelah’s Strong Hypothesis ( $\textsf {SSH}$ ), a PCF-theoretic strengthening of $\mathsf {SCH}$ . We then use ideas from these arguments to show that the generalized narrow system property, a close relative of the strong tree property, at a cardinal $\kappa $ implies $\mathsf {SSH}$ above $\kappa $ .

The second application concerns indecomposable ultrafilters. A non-principal ultrafilter U over a cardinal $\kappa> \aleph _1$ is indecomposable if, for every $\lambda < \kappa $ and every $f:\kappa \rightarrow \lambda $ , there is a set $A \in U$ such that $f[A]$ is countable. Sheard, answering a question of Silver, proved in the 1980s that, relative to the consistency of a measurable cardinal, it is consistent that there is an inaccessible cardinal $\kappa $ such that $\kappa $ carries an indecomposable ultrafilter but $\kappa $ is not weakly compact. Recently, Goldberg showed that this cannot happen above a strongly compact cardinal: If $\mu $ is strongly compact and $\kappa \geq \mu $ carries an indecomposable ultrafilter, then $\kappa $ is either measurable or a limit of countably many measurable cardinals. Using guessing models, we show that the same conclusion follows from $\mathsf {PFA}$ . This provides another instance in the long list of compactness principles that were first shown to hold above a strongly compact or supercompact cardinal and later shown also to follow from $\mathsf {PFA}$ .

This talk contains joint work with Šárka Stejskalová and with Assaf Rinot and Jing Zhang.

Abstracts of contributed talks

▸BAHAREH AFSHARI, GIACOMO BARLUCCHI, AND GRAHAM E. LEIGH, The limit of recursion in state-based systems.

Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, Renströmsgatan 6, 412 55 Göteborg, Sweden.

E-mail: giacomo.barlucchi@gu.se.

In this talk we present a study about closure ordinals of the modal $\mu $ -calculus, i.e., modal logic extended with least and greatest fixed point operators. We show that $\omega ^2$ is a strict upper bound on the closure ordinals of the $\Sigma $ -fragment of the modal $\mu $ -calculus, i.e., formulas generated from closed $\mu $ -calculus formulas and variables through the logical and modal operators, and the $\mu $ operator. This reproves and extends the claims in [1] concerning closure ordinals of the alternation-free fragment. The approach presented here develops a theory of ordinal annotations based on the notion of well-annotations previously introduced by Kozen [2]. By imposing minimality on the annotating ordinals we relate well-annotations to the existence of closure ordinals. The central argument involves a pumping lemma for well-annotations. Assuming the existence of a sufficiently ‘large’ frame, repetition of annotated sets enables a transfinite series of substitutions, showing it possible to obtain a minimal well-annotation corresponding in size to an arbitrary countable ordinal, thereby refuting the existence of closure ordinals equal or greater than ω ².

[1] B. Afshari and G. E. Leigh, On closure ordinals for the modal mu-calculus, Computer Science Logic 2013 (CSL 2013) (Torino, Italy) (Simona Ronchi Della Rocca, editor), vol. 23, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2013, pp. 30–44.

[2] D. Kozen, A finite model theorem for the propositional mu-calculus. Studia Logica , vol. 47 (1988), no. 3, pp. 233–241.

▸BAHAREH AFSHARI, SEBASTIAN ENQVIST AND GRAHAM E. lEIGH, Herbrand schemes for cyclic proofs.

Institutionen för filosofi, lingvistik och vetenskapsteori, Göteborgs Universitet, Renströmsgatam 6 Göteborg, Sweden.

E-mail: bahareh.afshari@gu.se.

Filosofiska institutionen, Stockholms universitet, Universitetsvägen 10D Stockholm, Sweden

E-mail: sebastian.enqvist@philosophy.su.se.

Institutionen för filosofi, lingvistik och vetenskapsteori, Göteborgs Universitet, Renströmsgatam 6 Göteborg, Sweden.

E-mail: graham.leigh@gu.se.

Recent work by Afshari et al. introduce a notion of Herbrand schemes for first-order logic by associating a higher-order recursion scheme to a sequent calculus proof. Calculating the language of associated Herbrand schemes directly yields Herbrand disjunctions. As such, these schemes can be seen as programs extracted from proofs. Here, this computational interpretation is explored further by removing the restriction of acyclicity from Herbrand schemes which amounts to admitting recursively defined programs. It is shown that the notion of proof corresponding to these generalised Herbrand schemes is cyclic proofs, considered here in the context of classical theories of inductively defined predicates. In particular, for proofs with end sequents of a form generalising the notion of $\Sigma _1$ -sequents in the first-order setting, Herbrand schemes derive a language of witnesses from cyclic proofs via a simulation of non-wellfounded cut elimination. Thus Herbrand schemes can be used to directly compute the “Herbrand content” of cyclic proofs. This is based on unpublished work, for which a preprint is available at: https://eprints.illc.uva.nl/id/eprint/2292/1/Herbrand_schemes_for_cyclic_ proofs.pdf.

▸BAHAREH AFSHARI AND RAÚL RUIZ MORA, Team semantics for modal mu-calculus.

Department of Philosophy, Linguistics, Theory of Science, University of Gothenburg, Sweden.

E-mail: bahareh.afshari@gu.se.

Departament de Matemàtiques, Universitat de València, Spain.

E-mail: raul.ruiz-mora@uv.es.

Team semantics can be seen as a generalisation of Tarskian model theoretic semantics originally developed by Hodges in [1]. In recent work, see e.g., [3], team semantics have been developed for LTL, CTL and CTL*. Also, team semantics have been defined and studied for modal logic [3] and first order logic giving rise to dependence logic, independence logic and inclusion logic [5].

We define a team semantics for modal mu-calculus, show it enjoys the flatness property and aligns well with existing team temporal logics. The approach taken utilises team semantics for modal logic and involves an algebraic study of powerset structures in order to assign a reasonable team semantics to fixed-points [4].

[1] W. Hodges, Compositional semantics for a language of imperfect information. Logic Journal of the IGPL , vol. 5 (1997), no. 4, pp. 539–563.

[2] J. M. Kontinen, J. S. H. Schnoor, and H. Vollmer, A van Benthem theorem for modal team semantics, 24th EACSL Annual Conference on Computer Science Logic (CSL 2015) (Berlin, Germany) , (S. Kreutzer, editor), Leibniz International Proceedings in Informatics (LIPIcs), vol. 41, Schloss Dagstuhl, Leibniz-Zentrum für Informatik, 2015, pp. 277–291.

[3] A. Krebs, A. Meier, and J. Virtema, A team based variant of CTL, 22nd International Symposium on Temporal Representation and Reasoning (TIME) (Kassel, Germany) , (Fabio Grandi, Martin Lange and Alessio Lomuscio, editors), IEEE, 2015, pp. 140–149.

[4] R. Ruiz, Team semantics for modal mu-calculus, Master’s thesis, University of Amsterdam, 2023.

[5] J. Väänänen, Dependence Logic: A New Approach to Independence Friendly Logic , London Mathematical Society Student Texts, vol. 70, Cambridge University Press, 2007.

▸KATALIN BIMBÓ, Operational semantics for positive relevance logics.

Department of Philosophy, University of Alberta, 2–40 Assiniboia Hall, Edmonton, AB T6G 2E7, Canada.

E-mail: <bimbo@ualberta.ca>.

URL Address: www.ualberta.ca/~bimbo.

The relational semantics for relevance logics that was introduced by Meyer and Routley in the 1970s, utilizes a ternary relation, although it emerged from the idea of an operational semantics (cf. [2]). A binary operation in place of the ternary relation provides a certain simplification. However, the set of prime filters (or prime theories) is not closed under the fusion operation. For an informational interpretation of the semantics, it is desirable to use operations applicable to situations that have less structure than prime theories. In this talk, I define an operational semantics for the main positive relevance logics $\mathbf {T_+}$ , $\mathbf {E_+}$ and $\mathbf {R_+}$ , that is, the positive fragments of the logics of ticket entailment, of entailment and of relevant implication. The operational structure for these logics is based on pieces of information and it is augmented with a topology (which is similar to the topology used in [1]). The logics are proved to be sound and complete for these operational semantics.

[1] K. Bimbó, Dual gaggle semantics for entailment. Notre Dame Journal of Formal Logic , vol. 50 (2009), no. 1, pp. 23–41.

[2] K. Bimbó and J. M. Dunn, The emergence of set-theoretical semantics for relevance logics around 1970, Proceedings of the Third Workshop, May 16–17, 2016, Edmonton, Canada , (K. Bimbó and J. M. Dunn, editors), special issue of the IFCoLog Journal of Logics and their Applications , vol. 4 (2017), no. 3, pp. 557–589.

▸ANDREW BROOKE-TAYLOR, Disentangling $\Sigma _2$ variants of supercompactness.

School of Mathematics, University of Leeds, Leeds, LS2 9JT, UK.

E-mail: a.d.brooke-taylor@leeds.ac.uk.

If you know what a supercompact cardinal is, there are many possibilities that come to mind for what the phrase “ $\Sigma _2$ -supercompact” could mean. Noting that $\textrm {HOD}$ is $\Sigma _2$ -definable, it is natural to throw $\textrm {HOD}$ -supercompactness and supercompactness in $\textrm {HOD}$ into this mix, particularly given the interest in large cardinals in $\textrm {HOD}$ arising from Woodin’s $\textrm {HOD}$ conjecture. We report on joint work with Shoshana Friedman disentangling these various possibilities, in part building on work of Bea Adam-Day [1], with models separating examples of these variants that are inequivalent.

[1] B. Adam-Day, Indestructibility and $C^{(n)}$ -Supercompact Cardinals , Ph.D Thesis, University of Leeds, 2024.

▸GABRIELE BURIOLA, DOMENICO CANTONE, GIANLUCA CINCOTTI, EUGENIO G. OMODEO, AND GAETANO T. SPARTÀ, A parameterized family of decidable theories involving differentiable functions.

Department of Computer Science, University of Verona, Italy.

E-mail: Gabriele.Buriola@UniVr.it.

Department of Mathematics and Computer Science, University of Catania, Italy.

E-mail: domenico.cantone@unict.it.

E-mail: gianluca.cincotti@unict.it.

Department of Mathematics, Informatics, and Earth Sciences, University of Trieste, Italy.

E-mail: eomodeo@units.it.

Pontificia Università Gregoriana, Italy.

E-mail: g.sparta@unigre.it.

We build on the existing literature on decidability in elementary analysis [2, 3, 1] by introducing a new family of decidable theories called $\textit {RDF\/}^n$ . (Here the word ‘theory’ refers to a fragment of a logical language, subject to strong syntactic restraints.) These theories are parameterized by natural numbers and involve differentiable real functions of class $C^n$ . By extending the previously developed theory $\textit {RDF\/}^{*}$ (see [1]), each $\textit {RDF\/}^n$ is a quantifier-free first-order theory that includes numerical variables, basic arithmetic operations, function variables, and operators and relation symbols for function addition, multiplication by a scalar, differentiation, function comparisons, strict and non-strict monotonicity / convexity / concavity, and comparisons between functions (and their derivatives up to nth order) and real-valued terms. The sentences constituting the $\textit {RDF\/}^n$ language are (universally closed) propositional combinations of atomic formulas of the forms shown in the table below: therein, the prefix ‘ $\textit {S}\_$ ’ indicates strictness; $\alpha $ stands for an integer ranging from 1 to n and $D^\alpha $ denotes the $\alpha $ th order derivative; A stands for an interval specification; $\bowtie $ can be any of the relators $=,<,>,\leqslant ,\geqslant $ ; $s,t$ stand for real-valued terms, and $f,g$ for terms designating functions in $C^n$ .

Table 1

Atomic formulae of $\textit {RDF}^n$ .

The decidability of these theories relies on the one hand on Tarski’s celebrated theorem [6] concerning the decision problem for the algebra of real numbers and, on the other hand, on interpolation techniques. Our ultimate goal is to institute a uniform theory $\textit {RDF\/}^{\infty }$ that encompasses $C^{\infty }$ functions.

Additionally, we explore the limits of decidability in the presence of a richer endowment of constructs relating derivatives and functions, e.g., equalities of the form $D^2[f]=g$ , building upon the findings of Richardson [4] and the subsequent improvements by Laczkovich [5].

[1] G. Buriola, D. Cantone, G. Cincotti, E. Omodeo and G. Spartà, A decidable theory involving addition of differentiable real functions. Theoretical Computer Science , vol. 940 (2022), pp. 124–148.

[2] H. Friedman and Á. Seress, Decidability in elementary analysis, I. Advances in Mathematics , vol. 76 (1989), no. 1, pp. 94–115.

[3] , Decidability in elementary analysis, II. Advances in Mathematics , vol. 79 (1990), no. 1, pp. 1–17.

[4] D. Richardson, Some undecidable problems involving elementary functions of a real variable. Journal of Symbolic Logic , vol. 33 (1968), no. 4, pp. 514–520.

[5] M. Laczkovich, The removal of $\pi $ from some undecidable problems involving elementary functions. Proceedings of the American Mathematical Society , vol. 131 (2002), no. 7, pp. 2235–2240.

[6] A. Tarski, A Decision Method for Elementary Algebra and Geometry , Technical Report U.S. Air Force Project RAND R-109, Santa Monica, CA, 2nd revised edition, University of California Press, iii+63 pp., 1951.

▸GABRIELE BURIOLA AND ANDREAS WEIERMANN, Phase transition thresholds for generalized Goodstein sequences, hydra games and Ackermannian functions.

Department of Computer Science, University of Verona, Italy Department of Mathematics, University of Ghent, Belgium.

E-mail: Gabriele.Buriola@UniVr.it.

Department of Mathematics, University of Ghent, Belgium.

E-mail: Andreas.Weiermann@UGent.be.

We extend previous results [2] regarding the phase transition thresholds for Goodstein Sequences and Hydra Games to a more general setting. In both cases, we substitute the original successor function with the iterations of a strictly increasing primitive recursive function g satisfying the condition $g(x) \geq x+1$ ; more precisely, the steps of the Hydra Game, original of type $\alpha _{f\!,i+1}= \alpha _{f\!,i}[1+f(i)]$ , are now of the form $\alpha ^{f\!,g}_{i+1}=\alpha ^{f\!,g}_{i}[1+f(g^{i-1}(1))] $ , while the steps of Goodstein sequences are changed from $m_{f\!,i+1}=m_{f\!,i}\left (1+f(i) \mapsto 1+f(i+1)\right ) -1$ to $m^{f\!,g}_{i+1}=m^{f\!,g}_i\left (1+f(g^{i-1}(1)) \mapsto 1+f(g^{i}(1))\right ) -1$ . The new phase transition thresholds incorporate the starting function g. These findings also allow a generalization of the phase transition threshold for Ackermannian functions [1] and fit within a rich literature regarding phase transitions in provability [3, 4, 5].

[1] E. Omri and A. Weiermann, Classifying the phase transition threshold for Ackermannian functions. Journal of Pure and Applied Logic , vol. 158 (2009), pp. 156–162.

[2] F. Meskens and A. Weiermann, Classifying phase transition thresholds for Goodstein sequences and Hydra games, Gentzen’s Centenary , (R. Kahle and M. Rathjen, editors), Springer, 2015, pp. 455–478.

[3] L. Carlucci, G. Lee, and A. Weiermann, Sharp tresholds for hypergraph regressive Ramsey numbers, Journal of combinatorial theory. Series A , vol. 118 (2011), no. 2, pp. 558–585.

[4] M. de Smet and A. Weiermann, Sharp thresholds for a phase transition related to weakly increasing sequences. Journal of logic and computation , vol. 22 (2012), no. 2, pp. 207–211.

[5] L. Gordeev and A. Weiermann, Phase transitions in proof theory, Discrete Mathematics and Theoretical Computer Science , Proceedings vol. AM, (2010), pp. 343–358.

▸YONG CHENG, On Rosser theories.

School of Philosophy, Wuhan University, China.

E-mail: world-cyr@hotmail.com.

The notion of Rosser theories is introduced in [1]. Rosser theories play an important role in the study of the incompleteness phenomenon and mete-mathematics of arithmetic, and have important mete-mathematical properties. All definitions of Rosser theories in the literature are restricted to arithmetic languages which admit numerals for natural numbers. Results about Rosser theories in the literature are confined to 1-ary relations. A general theory of Rosser theories for n-ary relations for any $n\geq 1$ and relationships among them is missing in the literature.

We first introduce the notion of n-Rosser theories, which generalizes the notion of Rosser theories for RE sets to n-ary RE relations in a general setting via the notion of interpretation. Then, we introduce notions of exact n-Rosser theories, effectively n-Rosser theories and effectively exact n-Rosser theories. Our definitions of these notions are not restricted to arithmetic languages admitting numerals for natural numbers. Then we systematically examine properties of these notions, and study relationships among these notions. Especially, we generalize some important theorems about Rosser theories for RE sets in the literature to n-Rosser theories for any $n\geq 1$ . One important tool we use is the fact that for a disjoint pair of n-ary RE relations, semi- $\mathsf DU$ implies $\mathsf DU$ . We give three different proofs of this fact.

Let T be a consistent RE theory. We prove the following main theorems for any $n\geq 1$ :

1. 1. If T is $(n+1)$ -Rosser (exact $(n+1)$ -Rosser), then T is effectively n-Rosser (effectively exact n-Rosser).

2. 2. If T is $(n+1)$ -Rosser, then T is exact n-Rosser.

3. 3. T is effectively n-Rosser if and only if T is effectively exact n-Rosser.

4. 4. Suppose T is n-Rosser and any n-ary recursive functional on $\mathbb {N}^n$ is admissible in T, then T is exact n-Rosser.

5. 5. If the pairing function $J_2(x,y)$ is strongly definable in T, then for any $n\geq 1$ , the following are equivalent: n-Rosser, effectively n-Rosser, exact n-Rosser, effectively exact n-Rosser.

[1] R. M. Smullyan, Recursion Theory for Meta-Mathematics , Oxford Logic Guides 22, Oxford University Press, 1993.

▸VITTORIO CIPRIANI, Isomorphism problems and learning of algebraic structures.

Technische Universität Wien, Institut für Diskrete Mathematik und Geometrie, Austria.

E-mail: vittorio.cipriani17@gmail.com.

In this talk, we study the classification of isomorphism problems with countably many isomorphism types. Borel reducibility has proven to be a powerful tool for classifying classes of countable structures under isomorphism; however, such problems, when restricted to classes with only countably many isomorphism types, have the same Borel complexity.

To nicely classify such problems, we present a framework defined in a series of papers by Bazhenov, Fokina, Kötzing, and San Mauro which combines ideas from computable structure theory and algorithmic learning theory. Here, given a countable family of structures $\mathfrak {K}$ a learner receives larger and larger pieces of an isomorphic copy of a structure in $\mathfrak {K}$ and, at each stage, is required to output a conjecture about the isomorphism type of such a structure. The learning is successful if the conjectures eventually stabilize to a correct guess.

Together with Bazhenov and San Mauro, we showed that a countable family of countable structures is learnable if and only if the corresponding isomorphism problem reduces to $E_0$ , the equivalence relation of eventual agreement on infinite binary sequences. Replacing $E_0$ with other Borel equivalence relations, one obtains a hierarchy to rank such isomorphism problems. This improves the aforementioned framework by providing a way of calibrating the complexity of non-learnable families.

Starting from a result of Bazhenov, Fokina, and San Mauro we give a model-theoretic characterization of the learning power of several equivalence relations (with a focus on Friedman–Stanley jumps of the identity on $2^{\mathbb {N}}$ and $\mathbb {N}$ ) and also of other classical learning criteria.

This talk collects joint works with Bazhenov, Jain, Marcone, San Mauro, and Stephan.

▸DARIO DELLA MONICA AND MATTIA GUIOTTO, Expressiveness issues in interval temporal logics.

Department of Mathematics and Computer Science, University of Udine, Italy.

E-mail: dario.dellamonica@uniud.it.

E-mail: guiotto.mattia@spes.uniud.it.

Interval temporal logics provide a natural framework for temporal reasoning about interval structures over linearly ordered domains, where intervals are taken as the primitive ontological entities [6]. One of the most studied interval temporal logics is Halpern and Shoham’s Modal Logic of Time Intervals ( $\mathsf {HS}$ , for short) [5], which features 12 modal operators, one for each binary relation between intervals over linear orders, known as Allen’s relations [2]. It was proved that the satisfiability of $\mathsf {HS}$ formulae is highly undecidable, which motivated the search for syntactic fragments of $\mathsf {HS}$ offering a good balance between expressiveness and computational complexity. Each subset of modal operators gives rise to a syntactically different $\mathsf {HS}$ fragment. Due to the possibility of defining modal operators in terms of others, not all $\mathsf {HS}$ fragments are expressively different. We consider the problem of obtaining a complete classification of the relative expressive power of all $\mathsf {HS}$ fragments over the class of all discrete and the one of all finite linear orders. An almost complete picture has been obtained [1], with a unique, difficult problem being still open. The missing tile of the expressiveness puzzle is that of the definabilities for the modal operator of $\mathsf {HS}$ corresponding to the Allen relation overlaps. The aim of our work is to complete the picture by filling the remaining gap. More precisely, we conjecture that the set of known definabilities for the $\mathsf {HS}$ modal operator corresponding to the relation overlaps is complete for the class of all discrete linear orders. Proving such a conclusion requires the support of an important classic theoretical result, known as the bisimulation invariance property for modal formulae which is at the basis of undefinability results for modal logics [3]. We provide a proposal for a bisimulation construction, and give strong and convincing evidence to support its correctness. A complete formal proof is quite technically involved and tedious, and requires a meticulous case-by-case analysis. We managed to give a partial formal proof by completing one of the most difficult cases [4]. In conclusion, the work done paves the way towards the closure of the long-standing open issue of obtaining a complete expressiveness picture of the family of $\mathsf {HS}$ fragments over the class of all discrete and the one of all finite linear orders.

[1] L. Aceto, D. D. Monica, A. Ingólfsdóttir, A. Montanari, and G. Sciavicco, On the expressiveness of the interval logic of Allen’s relations over finite and discrete linear orders, Logics in Artificial Intelligence: 14th European Conference, JELIA 2014 (Funchal, Madeira, Portugal) , (Eduardo Fermé and João Leite, editors), Lecture Notes in Computer Science, vol. 8761, 2014, pp. 267–281.

[2] J. F. Allen, Maintaining knowledge about temporal intervals. Communications of the ACM , vol. 26 (1983), no. 11, pp. 832–843.

[3] V. Goranko and M. Otto, Handbook of modal logic, Model Theory of Modal Logic , Elsevier, 2006, pp. 255–325.

[4] M. Guiotto, Expressiveness issues in Interval Temporal Logic, Bachelor’s Thesis, University of Udine, 2023.

[5] J. Y. Halpern and Y. Shoham, A propositional modal logic of time intervals. Journal of the ACM , vol. 38 (1991), no. 4, pp. 935–962.

[6] B. C. Moszkowski and Z. Manna, Reasoning in Interval Temporal Logic, Logics of Programs (Carnegie Mellon University, Pittsburgh) , (E. M. Clarke and D. Kozen, editors), Lecture Notes in Computer Science, vol. 164, Springer, 1983, pp. 371–382.

▸PABLO DOPICO, Axiomatic theories of supervaluationist truth: completing the picture.

Department of Philosophy, King’s College London, Strand, London, WC2R 2LS, United Kingdom.

E-mail: pablo.dopico@kcl.ac.uk.

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$ ( $\textbf {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 $\textbf {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 $\textbf {RA}_{<\Gamma _0}$ .

This is joint work with Daichi Hayashi.

[1] S. Kripke, Outline of a theory of truth. The Journal of Philosophy , vol. 72 (1975), no. 19, pp. 690–716.

[2] B. C. van Fraassen, Singular terms, truth-value gaps, and free logic. The Journal of Philosophy , vol. 63 (1966), no. 17, pp. 481-495.

[3] A. Cantini, A theory of formal truth arithmetically equivalent to $ID_1$ . The Journal of Symbolic Logic , vol. 55 (1990), no. 1, pp. 244–259.

[4] M. Fischer, V. Halbach, J. Kriener, and J. Stern, Axiomatizing semantic theories of truth? The Review of Symbolic Logic , vol. 8 (2015), no. 2, pp. 257–278.

[5] S. Feferman, Reflecting on incompleteness. The Journal of Symbolic Logic , vol. 56 (1991), no. 1, pp. 1–49.

▸DAVID FERNÁNDEZ-DUQUE, ORIOLA GJETAJ AND ANDREAS WEIERMANN, A Goodstein independence result for $ID_2$ .

Department of Philosophy, University of Barcelona, Montalegre 6, 08001 Barcelona, Spain.

E-mail: fernandez-duque@ub.edu.

Institute for Analysis, Logic and Discrete Mathematics, Ghent University, Krijgslaan 281 S8, 9000 Ghent, Belgium.

E-mail: oriola.gjetaj@ugent.be.

E-mail: andreas.weiermann@ugent.be.

The Goodstein principle is a natural number-theoretic theorem. The original process works by writing natural numbers into nested exponential k-base normal form, then successively raising the base to k + 1 and subtracting 1 from the result. Such sequences always reach zero, but this fact is unprovable in Peano arithmetic. Drawing from previous results in the literature, we consider canonical representations with respect to the Fast-Growing Extended Grzegorczyk hierarchy $\{F_{a}\}_{a<\psi _0(\varepsilon _{\Omega +1})}$ . Normal forms are written as base-k representations and the component a is written as base- $\psi _0(\cdot )$ collapsing function up to Bachmann–Howard ordinal. We use an ordinal assignment to show that this sequence terminates and yields an independence result from the theory of $ID_2$ . This is part of joint work with A. Weiermann and D. Fernández-Duque on exploring normal form notations for the Goodstein principle.

[1] T. Arai, S. Wainer, and A. Weiermann, Goodstein sequences based on a parametrized Ackermann-Péter function. The Bulletin of Symbolic Logic , vol. 27 (2021), no. 2, pp. 168–186.

[2] W. Buchholz, E. A. Cichon, and A. Weiermann, A uniform approach to fundamental sequences and hierarchies. Mathematical Logic Quarterly , vol. 40 (1994), pp. 273–286.

[3] R. L. Goodstein, On the restricted ordinal theorem. The Journal of Symbolic Logic , vol. 9, (1944), pp. 33–41.

[4] L. Kirby and J. Paris., On the restricted ordinal theorem. Bulletin of The London Mathematical Society , 14,(1982), no. 4, pp. 285–293.

[5] A. Weiermann, Investigations on slow versus fast growing: How to majorize slow growing functions nontrivially by fast growing ones. Archive for Mathematical Logic , vol. 34 (1995), no. 5, pp. 313–330.

▸PAULO FIRMINO AND LAURENŢIU LEUŞTEAN, Proof mining and the viscosity approximation method.

Departamento de Matemática, Faculdade de Ciências, Universidade de Lisboa.

E-mail: fc49883@alunos.ciencias.ulisboa.pt.

LOS, Faculty of Mathematics and Computer Science, University of Bucharest, Simion Stoilow Institute of Mathematics of the Romanian Academy (IMAR), and Institute for Logic and Data Science, Bucharest.

E-mail: laurentiu.leustean@unibuc.ro.

This talk presents an application of proof mining to the viscosity approximation method (VAM) for accretive operators in Banach spaces, studied recently by Xu et al. [5]. Proof mining is a research program concerned with the extraction, by using proof-theoretic techniques, of new quantitative and qualitative information from mathematical proofs. We refer to Kohlenbach’s textbook [2] for details on proof mining.

Let X be a normed space and $A:X\to 2^X$ be an m-accretive operator with a nonempty set of zeros. The VAMe iteration, a generalization of VAM obtained by adding error terms, is defined as follows:

where $f:X\to X$ is an $\alpha $ -contraction for $\alpha \in [0,1)$ , $(\alpha _n)_{n\in \mathbb {N}}$ is a sequence in $[0,1]$ , $(\lambda _n)_{n\in \mathbb {N}}$ is a sequence in $(0,\infty )$ , $(e_n)_{n\in \mathbb {N}}$ is a sequence in X, and, for every $n\in \mathbb {N}$ , $J_{\lambda _n}^A$ is the resolvent of order $\lambda _n$ of A.

In [1] we apply proof mining methods to obtain quantitative asymptotic regularity results for the VAMe iteration, providing uniform rates of asymptotic regularity, $\left (J_{\lambda _n}^A\right )$ -asymptotic regularity and, for all $m\in \mathbb {N}$ , $J_{\lambda _m}^A$ -asymptotic regularity of VAMe. For concrete instances of the parameter sequences, linear rates are computed by applying [3, Lemma 2.8], a slight variation of a lemma due to Sabach and Shtern [4].

[1] P. Firmino and L. Leuştean, Quantitative asymptotic regularity of the VAM iteration with error terms for m-accretive operators in Banach spaces, Zeitschrift für Analysis und ihre Anwendungen , 2024, published online first.

[2] U. Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics , Springer Monographs in Mathematics, Springer, 2008.

[3] L. Leuştean and P. Pinto Rates of asymptotic regularity for the alternating Halpern-Mann iteration. Optimization Letters , vol. 18 (2024), pp. 529–543.

[4] S. Sabach and S. Shtern, A first order method for solving convex bilevel optimization problems. SIAM Journal on Optimization , vol. 27 (2017), no. 2, pp. 640–660.

[5] H.-K. Xu, N. Altwaijry, I. Alughaibi, and S. Chebbi, The viscosity approximation method for accretive operators in Banach spaces. Journal of Nonlinear and Variational Analysis , vol. 6 (2022), no. 1, pp. 37–50.

▸VALENTIN GORANKO, Local basic strategy logic.

Department of Philosophy, Stockholm University.

E-mail: valentin.goranko@philosophy.su.se.

URL Address: https://www2.philosophy.su.se/goranko.

Basic Strategy Logic ( $\mathsf {BSL}$ ) introduced in [1] is a minimal variation of Strategy Logic from [2]. $\mathsf {BSL}$ builds on some (usually temporalized) language for expressing agents goals, such as $\mathsf {LTL}$ , that defines a set of goal formulae $\Gamma $ which are evaluated on plays in concurrent game models. The language of $\mathsf {BSL}$ extends $\Gamma $ with standard Boolean connectives and associates with each agent $\mathsf {a}$ from a fixed set $\mathsf {Agt}$ a strategy variable, denoted by $\mathsf {x}_{\mathsf {a}}$ . These variables range over strategies for the respective agents and are quantified over within the formulae of $\mathsf {BSL}$ . Thus, $\mathsf {BSL}$ can be used for formalising and reasoning about strategic abilities of agents (players) and coalitions in concurrent multi-player games. It is shown in [1] that $\mathsf {BSL}$ is sufficiently expressive to capture many naturally defined recently studied operators and logics for strategic abilities. In this work I study its local version $\mathsf {LBSL}$ , which only involves in the language of $\Gamma $ the Nexttime temporal operator, referring to the immediate outcomes states from playing single-round concurrent games at the states of the model. I explore and characterise the expressiveness of $\mathsf {LBSL}$ , study its vailidities, present an axiomatic system for them, and discuss the problems of its completeness and of the decidability of $\mathsf {LBSL}$ .

[1] V. Goranko, Logics for strategic reasoning of socially interacting rational agents: An overview and perspectives, Logics , vol. 1 (2023), no. 1, pp. 4–35.

[2] Fabio Mogavero, Aniello Murano, and Moshe Y. Vardi, Reasoning about strategies, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2010) , (Kamal Lodaya and Meena Mahajan, editors), Leibniz International Proceedings in Informatics, vol. 8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2010, pp. 133–144.

▸JOOST J. JOOSTEN, LUKA MIKEC AND ALBERT VISSER, Feferman interpretability and applications.

Department of Philosophy, University of Barcelona, Montalegre 6, 08001, Barcelona, Catalonia, Spain.

E-mail: jjoosten@ub.edu.

Department of Mathematics, University of Zagreb, Bijenička cesta 30., 10 000 Zagreb, Croatia.

E-mail: lmikec@math.hr.

Department of Philosophy and Religious Studies, Faculty of Humanities, Utrecht University Janskerkhof 13, 3512 BL Utrecht, The Netherlands.

E-mail: a.visser@uu.nl.

Given two theories $U,V$ with axiomsets that are polytime decidable so that U interprets V—we write $U\rhd V$ —we will define a theory $V'$ in the spirit of Feferman provability so that $V'$ is extensionally the same as V and so that $U\rhd V \to \Box _{\mathsf {S}^1_2} (U\rhd V')$ becomes a trivial matter. We apply this technique to prove the two hierarchies of principles from [1] to be arithmetically sound in any theory containing $\mathsf { S}^1_2$ .

[1] E. Goris and J.J. Joosten, Two new series of principles in the interpretability logic of all reasonable arithmetical theories. Journal of Symbolic Logic , vol. 85 (2020), no. 1, pp. 1–25.

▸DARIUSZ KALOCINSKI, Scott ranks and intended models.

Institute of Computer Science, Polish Academy of Sciences, Warsaw, Poland.

E-mail: dariusz.kalocinski@ipipan.waw.pl.

Certain mathematical theories are about a single, so-called intended, structure (e.g., arithmetic is about natural numbers) while others investigate general properties of all structures they axiomatize (e.g., group theory). The former theories are known as non-algebraic, while the latter as algebraic. One of the problems in the philosophy of mathematics concerns a systematic explanation of this phenomenon, ideally providing a theoretical notion that could explicate the concept of intendedness. I will briefly review some of the existing philosophical approaches regarding arithmetic, including the work of Halbach and Horsten [3], Button and Smith [1] and Walter Dean [2], among others. In the main part of my talk I will suggest a novel perspective on this problem, based on the measures of complexity of models, such as Scott ranks. I will try to explain basic technicalities involved in this notion and illustrate how it deals with the problem at hand with a few examples of algebraic as well as non-algebraic theories, including PA (by leveraging results from [4]) and weaker systems like Robinson’s or Presburger’s arithmetic.

[1] T. Button and P. Smith, The philosophical significance of Tennenbaum’s theorem. Philosophia Mathematica , vol. 20 (2012), no. 1, pp. 114–121.

[2] W. Dean, Models and computability. Philosophia Mathematica , vol. 22 (2014), no. 2, pp. 143–166.

[3] V. Halbach and L. Horsten, Computational structuralism. Philosophia Mathematica , vol. 13 (2005), no. 2, pp. 174–186.

[4] A. Montalbán and D. Rossegger, The structural complexity of models of arithmetic. The Journal of Symbolic Logic , (2023), pp. 1–17.

▸EITETSU KEN, Provability in relativized arithmetics and games with backtracking options.

Graduate School of Mathematical Sciences, the University of Tokyo, 3-8-1, Komaba, Meguro-ku, Tokyo, 153-0041, Japan.

E-mail: yeongcheol-kwon@g.ecc.u-tokyo.ac.jp.

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.

▸GABRIELA LABOSKA, Some computability theoretic aspects of partition regularity over rings.

Department of Mathematics, University of Chicago, Eckhart Hall, 5734 S University Ave, Chicago, IL 60637.

E-mail: gabrielap@uchicago.edu.

A system of linear equations over a ring R is partition regular if for any finite coloring of R, the system has a monochromatic solution. In 1933, Rado [3] showed that an inhomogeneous system is partition regular over $\mathbb {Z}$ if and only if it has a constant solution. Following a similar approach, Byszewski and Krawczyk [1] showed that the result holds over any integral domain. In 2018, following a different approach, Leader and Russell [2] generalized this over any commutative ring R. We analyze some of these combinatorial results from a computability theoretic point of view, starting with a theorem by Straus [4] used in the work of [1] and [2] that generalizes an earlier result by Rado.

[1] B. Byszewski and E. Krawczyk, Rado’s theorem for rings and modules. Journal of Combinatorial Theory Series A , vol. 180 (2021), p. 105402, pp. 28.

[2] I. Leader and P. A. Russell, Inhomogeneous partition regularity. Electronic Journal of Combinatorics , vol. 27 (2020), no. 2, p. 4.

[3] R. Rado, Studien zur kombinatorik. Mathematische Zeitschrift , vol. 36 (1933), no. 1, pp. 424–470.

[4] E. G. Straus, A combinatorial theorem in group theory. Mathematics of Computation , vol. 29 (1975), pp. 303–309.

▸ORVAR LORIMER OLSSON, General plurivalent Boolean logics.

Department of Philosophy, Linguistics and Theory of Science; University of Gothenburg, Renströmsgatan 6, Gothenburg, Sweden.

E-mail: orval.lorimer.olsson@gu.se.

Multivalued logics are commonly described in terms of valuations into an algebra of truth values. In [3], by lifting the consideration of valuations into subsets of the same algebra, Priest defines what he calls the Plurivalent version of a logic. This process essentially constitutes taking the power-algebra [1] of truth values from the original logic and memberhood of the originally designated elements as the new designation. In the simplest example of this construction Priest can identify his own logic of paradox (LP), and a logic known as analytic logic (AL) as plurivalent logics on classical truth values of the two valued Boolean algebra [3]. Furthermore we note that, by changing the designation notion, strong Kleene three valued logic $(\mathrm {K}_3)$ can also be identified by the same algebra through similar memberhood conditions.

Continuing work towards general methods for logics with team semantics [2] I will in this presentation consider the power-algebras of arbitrary Boolean algebras and establish a sound and complete labelled natural deduction system for entailments of memberhood statements. This gives rise to the definition and presentation of substructural versions of the aforementioned logics, with proof systems for which additional rules can be added to obtain the original logic.

[1] C. Brink, Power structures. Algebra Universalis , vol. 30 (1993), pp. 177–216.

[2] F. Engström and O. L. Olsson, The propositional logic of teams, arXiv.2303.14022, 2023.

[3] G. Priest, Plurivalent logics. The Australasian Journal of Logic , vol. 11 (2014), no. 1.

▸NURLAN D. MARKHABATOV, On disintegrated models.

Faculty of Mechanics and Mathematics, L.N. Gumilyov Eurasian National University, Kazakhstan.

E-mail: markhabatov@gmail.com

This research was funded by the Science Committee of the Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP19677451, AP22782938).

[1] S. V. Sudoplatov, Approximations of theories. Siberian Electronic Mathematical Reports , vol. 17, (2020), pp. 715–725.

▸GUILLAUME MASSAS, Galileo’s paradox and purely Euclidean numerosities.

Logic and the Methodology of Science, University of California, Berkeley.

E-mail: gmassas@berkeley.edu.

Galileo [2] famously asked whether there are more natural numbers than square numbers. On the one hand, every square number is a natural number, while the converse is false, suggesting that there are strictly more natural numbers than squares. On the other hand, there is an obvious way to define a one-to-one correspondence between the two collections, obtained by mapping any natural number to its square, suggesting that they are, in fact, equinumerous. Galileo’s paradox is a striking example of a clash between two intuitive principles about sizes of infinite collections [4]. According to the Part-Whole Principle (PW), any proper subcollection of a collection A has size strictly less than the size of A. According to the Bijection Principle (BP), any two collections have the same size if and only if there is a one-to-one correspondence between them. While the modern notion of cardinality obeys both principles in the finite, Cantor famously adopted (BP) as the foundation of his transfinite arithmetic, thus rejecting (PW). However, the recently developed theory of numerosities [1] has been presented as a viable alternative to the Cantorian picture that is based on (PW) rather than on (BP).

In this talk, I will focus on numerosities for countable sets. I will argue that the current theory of numerosities faces some major issues because it mixes two distinct intuitions. The first one is the Euclidean Intuition that the whole is always greater than any of its proper parts. The second, which I call the Density Intuition, is the intuition that the size of a set of natural numbers is determined by the frequency with which its elements appear in the sequence of natural numbers. While the first intuition is compatible with a very natural invariance condition that one would want to impose on any adequate notion of size for sets, the second intuition (and therefore also the standard theory of numerosities) is not. I will propose an alternative theory that is based purely on the Euclidean Intuition and is, in some precise axiomatic sense, the best way to combine part-whole intuitions with invariance criteria. Time permitting, I will also give a semantic intuition for this theory of Purely Euclidean Numerosities that is based on possibility semantics for classical first-order logic [3].

[1] V. Benci and M. di Nasso, Numerosities of labelled sets: A new way of counting. Advances in Mathematics , vol. 173 (2003), pp. 50–67.

[2] G. Galilei, Discorsi e dimostrazioni matematiche intorno a due nuove scienze, Boringhieri, 1958.

[3] W. H. Holliday, Possibility semantics. Selected Topics from Contemporary Logics , vol. 2 (2021).

[4] P. Mancosu, Measuring the size of infinite collections of natural numbers: Was Cantor’s theory of infinite number inevitable? The Review of Symbolic Logic , vol. 2 (2009), no. 4, pp. 612–646.

▸VICTOR BARROSO-NASCIMENTO, LUIZ CARLOS PEREIRA AND ELAINE PIMENTEL, An ecumenical view of proof-theoretic semantics.

Philosophy Department, UERJ, Av. Marechal Rondon, Brazil.

E-mail: victorluisbn@gmail.com.

Philosophy Department, UERJ, Av. Marechal Rondon, Brazil.

E-mail: luiz@inf.puc-rio.br.

Computer Science Department, University College London, Gower St., UK.

E-mail: e.pimentel@ucl.ac.uk.

Debates concerning philosophical grounds for the validity of classical and intuitionistic logics often have the very nature of logical proofs as one of the main points of controversy. The intuitionist advocates for a strict notion of constructive proof, while the classical logician advocates for a notion which allows non-construtive proofs through reductio ad absurdum. A great deal of controversy still subsists to this day on the matter, as there is no agreement between disputants on the precise standing of non-constructive methods.

Two very distinct approaches to logic are currently providing interesting contributions to this debate. The first, oftentimes called logical ecumenism [1], aims to provide a unified framework in which two “rival” logics may peacefully coexist, thus providing some sort of neutral ground for the contestants. The second, proof-theoretic semantics [2], aims not only to elucidate the meaning of a logical proof, but also to provide means for its use as a basic concept of semantic analysis. Logical ecumenism thus provides a medium in which meaningful interactions may occur between classical and intuitionistic logic, whilst proof-theoretic semantics provides a way of clarifying what is at stake when one accepts or denies reductio ad absurdum as a meaningful proof method.

In this paper we show how to coherently combine both approaches by providing not only a medium in which classical and intuitionistic logics may coexist, but also one in which classical and intuitionistic notions of proof may coexist.

[1] D. Prawitz, Natural deduction: A proof-theoretical study , Dover Publications, 2006.

[2] P. Schroeder-Heister, A natural extension of natural deduction. The Journal of Symbolic Logic , vol. 49 (1984), pp. 1284–1300.

▸GIAN MARCO OSSO, The Galvin-Prikry theorem in the Weihrauch lattice.

Dipartimento di Scienze Matematiche, Informatiche e Fisiche, Università di Udine, Viale delle Scienze, 208, Località Rizzi, 33100 Udine, Italy.

E-mail: osso.gianmarco@spes.uniud.it.

I will address the classification of different fragments of the Galvin–Prikry theorem, an infinite dimensional generalization of Ramsey’s theorem, in terms of their uniform computational content (Weihrauch degree). This work can be seen as a continuation of [1], which focused on the Weihrauch classification of functions related to the Nash–Williams theorem, i.e., the restriction of the Galvin–Prikry theorem to open sets. We have shown that functions related to the Galvin–Prikry theorem for Borel sets of rank n are strictly between the $(n+1)$ th and nth iterate of the hyperjump operator $\mathsf {HJ}$ , which corresponds to $\Pi ^1_1$ - $\mathsf {CA}_0$ in the Weihrauch lattice. To establish this classification we obtain the following computability theoretic result (along the lines of [2] and [3]): a Turing jump ideal containing homogeneous sets for all $\Delta ^0_{n+1}(X)$ sets must also contain $\mathsf {HJ}^n(X)$ . Similar results also hold for Borel sets of transfinite rank. This is joint work with Alberto Marcone.

[1] A. Marcone and M. Valenti, The open and clopen Ramsey theorem in the Weihrauch lattice. The Journal of Symbolic Logic , vol. 86 (2021), no. 1, pp. 316–351.

[2] C. G. Jockush, Ramsey’s theorem and recursion theory. The Journal of Symbolic Logic , vol. 37 (1972), no. 2, pp. 268–280.

[3] S. G. Simpson, Sets which do not have subsets of every higher degree. The Journal of Symbolic Logic , vol. 43 (1978), no. 1, pp. 135–138.

▸LEONARDO PACHECO, Higher-order feedback computation.

Institute of Discrete Mathematics and Geometry, TU Wien, Vienna, Austria.

E-mail: leonardo.pacheco@tuwien.ac.at.

URL Address: leonardopacheco.xyz.

Feedback Turing machines are Turing machines which can query a halting oracle $h:\subseteq \omega \times \omega \to \{\downarrow ,\uparrow \}$ , which has information on the convergence or divergence of feedback computations. That is, given the code e for a feedback Turing machine and an input n the oracle h answers if the computation $\{e\}^h(n)$ converges or diverges. To avoid a contradiction by diagonalization, feedback Turing machines have two ways of not converging: they can diverge as standard Turing machines, or they can freeze. A feedback Turing machine freezes when it asks the halting oracle h about a pair $\langle {e,n}\rangle $ not in the domain of h.

Feedback Turing machines were first studied by Ackerman, Freer, and Lubarsky [1, 2]. They proved that the feedback computable sets are the $\Delta ^1_1$ sets and the feedback semi-computable sets are the $\Pi ^1_1$ sets. We can also show that the feedback semi-computable sets are the winning regions of Gale–Stewart games with $\Sigma ^0_1$ payoff [3].

A natural question to ask is: what about feedback Turing machines which can ask if computations of the same type converge, diverge, or freeze? These new machines are second-order feedback machines. Note that we must now have a new and stronger notion of freezing to avoid a contradiction by diagonalization. Having defined second-order feedback computation, it is now natural to ask: what about third-, fourth-, and higher-order feedback?.

We define $\alpha $ th order feedback Turing machines for each computable ordinal $\alpha $ . We also describe feedback computable and semi-computable sets using inductive definitions and Gale–Stewart games. Specifically, we prove the following level-by-level correspondence:

(This is joint work with Juan P. Aguilera and Robert S. Lubarsky).

[1] N. L. Ackerman, C. E. Freer, and R. S. Lubarsky, Feedback turing computability, and turing computability as feedback, 30th Annual ACM/IEEE Symposium on Logic in Computer Science (Kyoto, Japan), IEEE, 2015, pp. 523–534.

[2] , An introduction to feedback turing computability. Journal of Logic and Computation , vol. 30 (2020), no. 1, pp. 27–60.

[3] Yannis N. Moschovakis, Descriptive Set Theory , Mathematical Surveys and Monographs, 155, American Mathematical Society, 2009.

▸LÉON PROBST, Self-referential Gödel numberings and uniformity.

Institute of Philosophy, University of Italian Switzerland, Lugano, Switzerland.

E-mail: leon.probst@usi.ch.

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.

[1] Grabmayr, Balthasar and Visser, Albert, Self-Reference Upfront: A Study of Self-Referential Gödel Numberings. The Review of Symbolic Logic , vol. 16 (2023), no. 2, pp. 385–424.

▸PHILIPP PROVENZANO, MOJTABA MOJTAHEDI, FEDOR PAKHOMOV AND ALBERT VISSER, Reflection and induction for subsystems of HA.

Department of Mathematics: Analysis, Logic and Discrete, Ghent University, Belgium.

E-mail: Philipp.Provenzano@UGent.be.

E-mail: Mojtaba.Mojtahedi@UGent.be.

E-mail: Fedor.Pakhomov@UGent.be.

Department of Philosophy and Religious Studies, Utrecht University, The Netherlands.

E-mail: a.visser@uu.nl.

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.

[1] D. Leivant, The optimality of induction as an axiomatization of arithmetic 1. The Journal of Symbolic Logic , vol. 48 (1983), no. 1, pp. 182–184.

[2] H. Ono, Reflection principles in fragments of Peano arithmetic. Mathematical Logic Quarterly , vol. 33 (1987), no. 4, pp. 317–333.

▸MARTIN RITTER, Isomorphism relations on classes of c.e. algebras.

Institute of Discrete Mathematics and Geometry, TU Wien, Wiedner Hauptsraße 8-10, 1040 Vienna, Austria.

E-mail: martin.ritter@tuwien.ac.at.

This talk is about our ongoing work on isomorphism relations on classes of c.e. algebras. In this context a c.e. algebra is an algebra that is given as a quotient of the term algebra by a c.e. congruence relation. An isomorphism relation on such a class of c.e. algebras can, under reasonable conditions, be viewed as an equivalence relation on the natural numbers. This allows us to compare complexities of different isomorphism relations using known methods and results from the computability-theoretic study of equivalence relations. We use computable reducibility, a common method for comparing equivalence relations. Isomorphism relations can then be compared to well-studied equivalence relations on c.e. sets, like $=^{ce}$ , $E^{ce}_{min}$ , $E^{ce}_0$ , etc. In this talk we present a case study on finitely generated commutative semigroups. We show that the isomorphism relations on the classes of n-generated commutative semigroups, for natural numbers n, form a strictly ascending sequence in the hierarchy of computable reducibility and are all bounded by $=^{ce}$ . This is joint work with Luca San Mauro.

▸LUCA SAN MAURO, A new way of classifying word problems.

Department of Philosophy, University of Bari, Bari, Italy.

E-mail: lucafrancesco.sanmauro@uniba.it.

The study of word problems dates back to the work of Dehn in 1911. Given a recursively presented algebra A, the word problem of A is to decide if two words in the generators of A refer to the same element. Much is known about the complexity of word problems for familiar algebraic structures: e.g., the Novikov–Boone theorem, one of the most spectacular applications of computability to general mathematics, states that the word problem for finitely presented groups is unsolvable. Yet, the computability theoretic tools commonly employed to measure the complexity of word problems (e.g., Turing or m-reducibility) are defined for sets, while it is generally acknowledged that many computational facets of word problems emerge only if one interprets them as equivalence relations.

In this work, we revisit the world of word problems, with a special focus on groups and semigroups, through the lens of the theory of equivalence relations, which has grown immensely in recent decades. To do so, we employ computable reducibility, a natural effectivization of Borel reducibility.

This talk collects joint works with Uri Andrews, Valentino Delle Rose, Meng-Che Ho, and Andrea Sorbi.

▸SEBASTIAN G.W. SPEITEL, Carnap’s categoricity problem.

Institute of Philosophy, University of Bonn.

E-mail: sgwspeitel@uni-bonn.de.

Carnap [4] demonstrated that the usual axiomatisations of classical propositional and first-order logic fall short of ‘fully formalising’ these systems. In particular, while there is a tight correspondence between syntactic, proof-theoretic, and semantic, model-theoretic, explications of the notion of consequence for these systems, a similarly adequate correspondence between inferential and model-theoretic aspects of the meanings of their logical expressions is lacking. More precisely, Carnap showed that there is a significant mismatch between the intended model-theoretic values of the logical constants and the model-theoretic values actually determined by the usual rules of inference. The standard axiomatisations of classical propositional and first-order logic are, thus, not categorical for the intended model-theoretic values of the logical constants of these systems. This is Carnap’s (categoricity) problem.

Carnap’s problem has significant repercussions for a range of projects and positions in the philosophy of logic, language, and mathematics. Although Carnap’s original considerations focused on classical propositional and first-order logic, its consequences have since been investigated for other classes of logical expressions, including intuitionistic connectives [8], modal operators [2], as well as generalized [3] and higher-order quantifiers [7]. Furthermore, a variety of different solution-strategies have been advanced in the literature: from modifying the language or format of the consequence relation [9, 10], over re-interpretations of the notion of an inference rule [5, 6], towards adopting additional constraints on the space of admissible meanings [1, 3].

The goal of this talk is to survey these different solution-strategies with an eye towards their ability of solving Carnap’s problem in full generality and their resulting conception of (logical) meaning. An interesting upshot of this investigation concerns the, sometimes implicitly, adopted meaning-theoretic constraints by different ways of resolving Carnapian underdetermination. Moreover, Carnap’s problem raises interesting questions about what it takes to have completely grasped or characterised a logical notion, resembling a similar discussion in the philosophy of mathematics. This parallel will be explored further in the talk.

[1] D. Bonnay and D. Westerståhl, Compositionality solves Carnap’s problem. Erkenntnis , vol. 81 (2016), no. 4, pp. 721–739.

[2] , Carnap’s problem for modal logic. The Review of Symbolic Logic , vol. 16 (2023), no. 2, pp. 578–602.

[3] D. Bonnay and S. G. W. Speitel, The ways of logicality: Invariance and categoricity, The Semantic Conception of Logic. Essays on Consequence, Invariance, and Meaning (G. Sagi and J. Woods, editors), Cambridge University Press, 2021, pp. 55–79.

[4] R. Carnap, Formalization of Logic , Harvard University Press, 1943.

[5] J. W. Garson, What Logics Mean: From Proof Theory to Model-Theoretic Semantics , Cambridge University Press, 2013.

[6] V. McGee, Everything, Between Logic and Intuition: Essays in Honor of Charles Parsons (G. Sher and R. Tieszen, editors), Cambridge University Press, 2000, pp. 54–79.

[7] J. Murzi and B. Topey, Categoricity by convention. Philosophical Studies , vol. 178 (2021), no. 10, pp. 3391–3420.

[8] H. Tong and D. Westerståhl, Carnap’s problem for intuitionistic propositional logic. Logics , vol. 1 (2023), no. 4, pp. 163–181.

[9] I. Rumfitt, ‘Yes’ and ‘No’, Mind . vol. 109 (2000), no. 436, pp. 781–823.

[10] D. J. Shoesmith and T. Smiley, Multiple Conclusion Logic , Cambridge University Press, 1978.

▸MENGZHOU SUN, TIN LOK WONG AND YUE YANG, The Kaufmann–Clote question on end extensions of models of arithmetic.

Department of Mathematics, National University of Singapore, 10 Lower Kent Ridge Road, Singapore 119076.

E-mail: sunm07@u.nus.edu.

A general question in the model theory of arithmetic is:

Efforts over the past four decades have revealed answers to this question for all the well-known theories in arithmetic, i.e., the $\Sigma _m$ induction schemes $\mathrm I\Sigma _m$ and the $\Sigma _m$ collection schemes $\mathrm B\Sigma _m$ , except the following instance.

We present a positive answer to the Kaufmann–Clote question. The proof consists of a second-order ultrapower construction based on a low basis theorem. We will also include a survey on the answers related to the general question above.

[1] P. Clote, Partition relations in arithmetic, Methods in Mathematical Logic (C. A. Di Prisco, editor), Springer-Verlag, Berlin, 1985, pp. 32–68.

[2] M. Kaufmann, On existence of $\Sigma _n$ end extensions, Logic Year 1979–80 , (M. Lerman, J. H. Schmerl, and R. I. Soare, editors), vol. 859, Springer, Berlin, 1981, pp. 92–103.

▸DAVIDE SUTTO, A history of level theories: from ranks to levels.

Department of Philosophy, IFIKK, University of Oslo (UiO), 0351, Oslo, Norway.

E-mail: davide.sutto@ifikk.uio.no.

The paper presents a comprehensive history of the formalizations of the Iterative Conception of Set. First, I show how the core idea originated, even before Zermelo’s $V_\alpha $ s, in reflections on ranks appearing in Mirimanoff’s 1910s contributions and earlier notes by German mathematicians. Second, I emphasize the seminal role played by Tarski’s School in developing the notion of rank and further argue that the actual genesis of the conception is to be found in Tarski’s 1950s set theory seminars, later developed in [2] and [3]. Third, I focus on the crucial passage from the notion of rank to its more explicit characterization: levels. In the work of Tarski’s School we can find the first formulations of axiomatic theories of levels in purely set theoretic terms. This is relevant as I move forward to Shoenfield and Boolos, who rather outline stage theories, adopting stages as a further primitive. Finally, I close with the more recent contributions of Potter and Button, who revitalized the notion of level by making it more tractable.

[1] T. Button, Level theory, part 1: Axiomatizing the bare idea of a cumula- tive hierarchy of sets. Bulletin of Symbolic Logic , vol. 27 (2022), no. 4, pp. 436–460.

[2] R. Montague, D. Scott, and A. Tarski, An Axiomatic Approach to Set Theory , unpublished manuscript. [Archive Copy from the Bancroft Library: Alfred Tarski Papers, circa 1923-1985 (BANC MSS 84/69 c, Carton 4, Folder 29-30).].

[3] D. Scott, Axiomatizing Set Theory, Proceedings of Symposia in Pure Mathematics (UCLA, July 10-August 5, 1967), (Thomas J. Jech), vol. XIII, part II, American Mathematical Society, 1974, pp. 207–214.

▸ANDREA VOLPI, Largeness notions.

Department of Mathematics, Informatics and Physics, University of Udine, Via delle Scienze, 206, 33100 Udine UD, Italy.

E-mail: andrea.volpi@uniud.it.

This is joint work with Alberto Marcone and Antonio Montalbán. Finite Ramsey theorem states that fixed $n,m,k \in \mathbb {N}$ , there exists $N \in \mathbb {N}$ such that for each coloring of $[N]^n$ with k colors, there is a homogeneous subset H of N of cardinality at least m. Starting with the celebrated Paris–Harrington theorem, many Ramsey-like results obtained by replacing cardinality with different largeness notions have been studied. I will introduce the largeness notion defined by Ketonen and Solovay based on fundamental sequences of ordinals. Then I will describe an alternative and more flexible largeness notion using blocks and barriers. Finally, I will talk about how the latter can be used to study a more general Ramsey-like result.

▸KAROL WAPNIARSKI, Ontological assumptions in the history of western logic: from Aristotelian syllogistic to Boolean algebra.

Faculty of Philosophy, Adam Mickiewicz University, Poznań, Poland.

E-mail: wapniarski.karol@gmail.com.

The purpose of the talk is to provide a thorough account of the issue of empty terms and ontological assumptions as they play throughout the history of Western logic, beginning with Aristotelian syllogistic and going up till the Boolean algebra and the emergence of modern formal logic. Modern formal logic, using the notion of the universe of discourse, does not allow for constructing interpretations of formal languages for empty universes. In contemporary discussions, it is widely assumed that the Aristotelian syllogistic did not allow for the use of empty terms as well. Upon closer examination, this view does not reflect the historical reality, and the issue of empty terms is much more complex. Throughout history, it has been extensively discussed both in relation to categorical statements and the Square of Opposition. In the paper, I relate these discussions. I assert 1) that the (non)emptiness of terms did not emerge as an issue in Aristotelian logic, and the dominant modern interpretation stems from the development of formal logic and attempts to render syllogistic using modern notation, 2) that the interest of Arabic philosophers in the issue can be explained by different ways of expressing existence and attribution in Indo-European and Semitic languages, 3) that the conditional treatment of existential assumptions proposed by Ockham serves as the origins of the universe of discourse idea. I end by asserting that, firstly, throughout history we can observe a rising awareness of empty terms as an issue that needs to be addressed, secondly, in parallel to it, we can trace the origins of the modern universe of discourse idea.

▸JIN WEI, Constructive version of Herbrand’s theorem for first-order Łukasiewicz logic.

Department of Mathematics, University of Pennsylvania, 209 S 33rd St, Philadelphia, PA 19104, USA.

E-mail: sapeaude@sas.upenn.edu.

Matthias Baaz and George Metcalfe [1] provided a hypersequent calculus for infinite Łukasiewicz logic which is sound and complete with respect to $[0,1]$ -truth valued semantics and admits cut elimination. This result is further extended to first-order Łukasiewicz logic [2]. However, the cut elimination proof passes through semantics and the constructive information is missing. In particular, a proof with cut does not lead directly to a cut-free proof other than guarantees the existence of one.

The core ingredient of their proof is an approximate version of Herbrand’s theorem for first-order Łukasiewicz logic where a compactness argument is being used. Since Herbrand’s theorem is essentially a $\Pi _2$ -statement, proof mining technique should be applicable here, provide a quantitative version of the theorem, and give an explicit upper bound for term witnesses of existence quantifiers. In this talk, I will describe my current progress in finding a constructive version of approximate Herbrand’s theorem for first-order Łukasiewicz logic. It will also be mentioned how this will contribute to a ultimate syntactic cut elimination proof, as well as some potential applications to continuous model theory.

[1] M. Baaz and G. Metcalfe, Herbrand’s theorem, skolemization and proof systems for first-Order Łukasiewicz logic. Journal of Logic and Computation , vol. 20 (2010), no. 1, pp. 35–54.

[2] G. Metcalfe, N. Olivetti, and D. Gabbay, Sequent and hypersequent calculi for abelian and Łukasiewicz logics. ACM Transactions on Computational Logic , vol. 6 (2005), no. 3, pp. 578–613.

[3] P. Hájek, Metamathematics of Fuzzy Logic , Kluwer, 1998.

[4] U. Kohlenbach and P. Oliva, Proof mining: A systematic way of analysing proofs in mathematics. Proceedings of the Steklov Institute of Mathematics , vol. 9 (2002), no. 31.

▸ANDREAS WEIERMANN, Monadic second order limit laws for natural well orderings.

Department of Mathematics WE16, Ghent University, Krijgslaan 281 S8, 9000 Ghent, Belgium.

E-mail: Andreas.Weiermann@UGent.be.

We prove monadic second order limit laws for ordinals stemming from segments of some prominent proof-theoretic ordinals like $\omega ^\omega ,\varepsilon _0,\Gamma _0,\ldots $ . The results are based on a combination of automata theoretic results, tree enumeration theory and Tauberian methods. We believe that our results will hold in very general contexts.

Some results have been obtained jointly with Alan R. Woods (who unfortunately passed away in 2011).

Abstracts of talks presented by title

▸BEIBUT KULPESHOV AND SERGEY SUDOPLATOV, On non-essential expansions of quite o-minimal theories.

Institute of Mathematics and Mathematical Modeling, Kazakh-British Technical University, Almaty, Kazakhstan.

E-mail: b.kulpeshov@kbtu.kz.

Sobolev Institute of Mathematics, Novosibirsk State Technical University, Novosibirsk, Russia.

E-mail: sudoplat@math.nsc.ru.

The present lecture concerns the notion of weak o-minimality originally studied by H.D. Macpherson, D. Marker and C. Steinhorn in [1]. A weakly o-minimal structure is a linearly ordered structure $M=\langle M,=,<,\ldots \rangle $ such that any definable (with parameters) subset of M is a finite union of convex sets in M.

Quite o-minimal theories were introduced in [2]. Let T be a weakly o-minimal theory, $M\models T$ , $A\subseteq M$ , $p,q\in S_1(A)$ non-algebraic. We say that p is quite orthogonal to q ( $p\perp ^q q$ ) if there is no A–definable bijection $f: p(M)\to q(M)$ . We say that a weakly o-minimal theory is quite o-minimal if the notions of weak and quite orthogonality coincide for 1-types over arbitrary subsets of models of the given theory.

This research has been funded by Science Committee of Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP19674850), and in the framework of the State Contract of the Sobolev Institute of Mathematics, Project No. FWNF-2022-0012.

[1] H. D. Macpherson, D. Marker, and C. Steinhorn, Weakly o-minimal structures and real closed fields. Transactions of the American Mathematical Society , vol. 352 (2000), no. 12, pp. 5435–5483.

[2] B. Sh. Kulpeshov, Convexity rank and orthogonality in weakly o-minimal theories, News of the National Academy of Sciences of the Republic of Kazakhstan, physical and mathematical series , vol. 227 (2003), pp. 26–31.

▸JOSÉ M. MÉNDEZ AND GEMMA ROBLES, Rules of proof, rules of inference, Ackermann’s $\gamma $ and the logic B.

Universidad de Salamanca. Edificio FES, Campus Unamuno, 37007, Salamanca, Spain.

E-mail: sefus@usal.es.

URL Address: https://sites.google.com/site/sefusmendez.

Dpto. de Psicología, Sociología y Filosofía, Universidad de León, Campus Vegazana, s/n, 24071, León, Spain.

E-mail: gemma.robles@unileon.es.

URL Address: https://gemmarobles.github.io.

Ackermann’s $\gamma $ , i.e., Disjunctive Syllogism, is the third rule of his system $\Pi ^{\prime }$ (cf. [1]); B is Routley and Meyer’s basic relevant logic (cf. [3]). Given a logic L, a rule of proof is only applicable to premises which are L-theorems; a rule of inference can be applicable to no matter what L-formulas.

In [2], it is shown how to add $\gamma $ to B if this logic is reinforced with the “Principle of Excluded Middle”. The aim of this paper is to strengthen this result by indicating how $\gamma $ can be added to a certain weak restriction of B. Also, it will be discussed if $\gamma $ can be added as a rule of inference or only as a rule of proof.

Acknowledgements. This work is funded by the Spanish Ministry of Science and Innovation MCIN/AEI/10.13039/501100011033 [Grant PID2020-116502GB-I00].

[1] W. Ackermann, Begründung einer strengen Implikation. The Journal of Symbolic Logic , vol. 21 (1956), no. 2, pp. 113–128.

[2] G. Robles and J. M. Méndez, A Routley-Meyer type semantics for relevant logics including Br plus the Disjunctive Syllogism. Journal of Philosophical Logic , vol. 39 (2010), no. 2, pp. 139–158.

[3] R. Routley, R. K. Meyer, V. Plumwood, and R. T. Brady, Relevant logics and their rivals, volume 1 , Ridgeview Publishing, 1982.

▸NICHOLAS PISCHKE, Proof mining and probability theory.

Department of Mathematics, Technische Universität Darmstadt, Schlossgartenstraße 7, 64289 Darmstadt, Germany.

E-mail: pischke@mathematik.tu-darmstadt.de.

On the surface, the theory of probability measures requires the use of proof theoretically strong principles to already develop some of the most basic notions. Contrary to these apparent limitations, we present a recent approach for extending the program of proof mining to this area. This approach relies crucially on two main ingredients: (1) We identify the theory of probability contents (i.e., finitely additive $[0,1]$ -valued functions defined on algebras of sets) as the mathematical finitary core of many arguments from probability theory and use this to initially define a suitable system for this proof-theoretically more accessible fragment. (2) Bootstrapped on this system, we employ intensional methods to deal with the high quantifier complexity of the predicates defining the other main objects of concern from probability theory, like e.g., infinite unions and Lebesgue integrals, etc. These systems are then amenable to proof mining metatheorems which guarantee the existence of (and provide a method for extracting) computable bounds for non-effectively proven existence statements. Further, for all these systems, we employ a novel extended notion of majorizability in the context of these metatheorems that guarantees that these extractable bounds are highly uniform regarding most parameters like e.g., the probability measure, the sample space and the event space, etc., and as such these metatheorems provide for the first time a logical explanation of the uniformities already observed in practice in the context of a few well-known ad hoc case studies preceding these metatheorems due to Avigad, Dean and Rute as well as Oliva and Arthan. This is joint work with Morenikeji Neri [1].

[1] M. Neri and N. Pischke, Proof mining and probability theory, arXiv:2403.00659, 2024, 47pp.

▸GEMMA ROBLES, Ternary relational semantics for relevant logics including BM $^{\text {d}}$ and included in R when supplemented with Disjunctive Syllogism.

Dpto. de Psicología, Sociología y Filosofía, Universidad de León, Campus Vegazana, s/n, 24071, León, Spain.

E-mail: gemma.robles@unileon.es.

URL Address: https://gemmarobles.github.io.

System R (“Relevance”) is Anderson and Belnap’s logic of relevant implication (cf. [1]); BM $^{\text {d}}$ is Sylvan and Plumwood’s minimal De Morgan Logic (cf. [4]) plus the disjunctive metarule MR (cf. [2] and references therein). By ternary relational semantics (TRS), we refer to that defined by Routley and Meyer (cf. [3] and references therein).

As known, the spectrum of logics delimited by BM $^{\text {d}}$ and R consists solely of relevant logics in the sense that they enjoy the variable-sharing property.

The aim of this paper is to define TRS for some prominent logics in the aforesaid spectrum when they are supplemented with the (full) rule Disjunctive Syllogism.

Acknowledgements. This work is funded by the Spanish Ministry of Science and Innovation MCIN/AEI/10.13039/501100011033 [Grant PID2020-116502GB-I00].

[1] A. R. Anderson and N. D. Jr. Belnap, Entailment. The logic of relevance and necessity, volume I , Princeton University Press, 1975.

[2] R. T. Brady, Universal logic , CSLI, Stanford, CA, 2006.

[3] R. Routley, R. K. Meyer, V. Plumwood, and R. T. Brady, Relevant logics and their rivals , vol. 1, Ridgeview Publishing, 1982.

[4] R. Sylvan and V. Plumwood, Non-normal Relevant Logics, Relevant Logics and Their Rivals, volume II (R. T. Brady, editor), Ashgate, 2003, pp. 10–16.