Logic Colloquium 2023, the annual European Summer Meeting of the Association of Symbolic Logic, was held at the University of Milan, June 5 through June 9, 2023. The conference was held in person at the Headquarter Educational Sector of the University of Milan with 220 registered participants. ASL travel grants were awarded to 36 graduate students and recent PhDs.

Funding for the conference was provided by the Association for Symbolic Logic; the National Science Foundation of the United States; numerous departments at the Università degli Studi di Milano including Dipartimento di Filosofia, Dipartimento di Matematica, Dipartimento di Informatica, and Dipartimento di Studi Storici; Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni; Associazione Italiana di Logica e sue Applicazioni; BRIO – BIAS, RISK, OPACITY in AI (PRIN Project no. 2020SSKZ7R); DHST/DLMPST Commission for the History and Philosophy of Computing; the Italian Society for Logic and the Philosophy of Science; and Dipartimento di Matematica e Fisica, Università degli Studi della Campania “Luigi Vanvitelli”.

The success of the meeting owes a great deal to the enthusiasm and hard work of the Local Organizing Committee chaired by Giuseppe Primiero and composed of Stefano Aguzzoli, Greta Coraglia, Esther Corsi, Marcello D’Agostino, Francesca Doneda, Giovanni Duca, Camillo Fiorentini, Miriam Franchella, Francesco Genco, Silvio Ghilardi, Hykel Honsi, Ekaterina Kubyshkina, Costanza Larese, Lorenzo Luperi Baglini, Chiara Manganini, Vincenzo Marra, Alberto Momigliano and Alberto Termine.

The Program Committee was chaired by Paola D’Aquino (Università della Campania “Luigi Vanvitelli”) and consisted of Matthias Aschenbrenner (University of Wien), Jan Krajicek (Charles University), Aleksandra Kwiatkowska (Münster University and Wroclaw University), Paulo Oliva (Queen Mary University), Giuseppe Primiero (Università di Milano) and Philip Welch (Bristol University).

The program included two tutorial courses, eight invited lectures, eighteen invited lectures in six special sessions (applied proof theory; computability theory; logic and computation; logic and philosophy; model theory; and set theory), and 139 contributed talks. The following tutorial courses were given.

Floris van Doorn (University of Paris-Saclay), Interactive theorem proving in Lean.

Itay Kaplan (Hebrew University), Machine learning and model theory.

The following invited plenary lectures were presented.

Gal Binyamini (Weizmann Institute of Science), Unlikely interactions: a mathematical theory of strange coincidences.

Nicola Gambino (University of Manchester), Two-dimensional categorical logic.

Gabriel Goldberg (University of California Berkeley), Large cardinals and the Ultrapower Axiom.

Martino Lupini (University of Bologna), Definable refinements of classical algebraic invariants.

Igor C. Oliveira (University of Warwick), Meta-mathematics of computational complexity theory.

Francesca Poggiolesi (University of Paris 1), Explanatory derivations in first-order logic.

Viorica Sofronie-Stokkermans (University of Koblenz), On symbol elimination in theory extensions and applications to parametric verification.

Zoltá Vidnyánszky (Eötvös University), Finite and infinite: an interplay between distributed computing and Borel combinatorics.

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

For the Program Committee

Paola D’Aquino

Abstract of invited tutorials

▸FLORIS VAN DOORN, Interactive theorem proving in Lean.

Mathematics Department, University of Paris-Saclay, rue Michel Magat, 91405 Orsay, France.

E-mail: fpvdoorn@gmail.com.

Do you want to try to prove some theorems in a computer proof assistant? Or do you want to learn the latest version of the Lean Theorem Prover? You will be able to do this in this tutorial. Please bring your laptop.

Lean is an interactive theorem prover that can be used to verify results in modern mathematics, such as a recent result by the Field’s medalist Peter Scholze in condensed mathematics. Lean has a rapidly growing library of formalized mathematics, containing most of the material found in a typical undergraduate curriculum and various more advanced topics. Recently a new version of Lean has been released. This version, called Lean 4, besides being a proof assistant is a fully-fledged programming language, and most of the code for Lean 4 itself was developed in Lean 4.

In this tutorial, I will be giving an hands-on introduction to using Lean. During most of the tutorial, you will be proving results in Lean yourself, using a series of carefully chosen exercises to learn how to formalize proofs quickly. We will be using the online platform Gitpod to run Lean in the cloud, so that you don’t have to install anything and it will run smoothly on less powerful machines.

▸ITAY KAPLAN, Machine learning and model theory.

Einstein Institute of Mathematics, The Hebrew University of Jerusalem, Givat Ram. Jerusalem, 9190401, Israel.

E-mail: kaplan@math.huji.ac.il.

I will give an overview of some connections between certain concepts in the theory of machine learning and notions in model theory. These connections were discovered and studied by many people in recent years, and lead to ideas and surprising results going both directions (from model theory to machine learning and vice versa).

I will not assume any knowledge in model theory or machine learning.

Abstracts of invited plenary lectures

▸GAL BINYAMINI, Unlikely intersections: a mathematical theory of strange coincidences.

Department of Mathematics, Weizmann Institute of Science, Israel.

E-mail: gal.binyamini@weizmann.ac.il.

An “unlikely intersection” problem is one where the number of constraints strictly exceeds the degrees of freedom. For such problems, the existence of a solution can be thought of as an unlikely “coincidence”. A general paradigm in this area is that if a system exhibits many coincidences, then there must be some hidden structure in the system that forces them to occur – things happen for a reason.

Many classical problems in arithmetic geometry can be viewed as unlikely intersection problems. I’ll discuss some of these examples along with other unlikely intersection problems that come up in analysis and dynamics. Surprisingly, many of these problems - even those having seemingly nothing to do with algebraic data - often turn out to be fundamentally linked to the study of integer and rational points in certain sets. I’ll explain how logic and model theory facilitate this unexpected translation and provide very powerful tools in pursuit of the general paradigm above.

▸NICOLA GAMBINO, Two-dimensional categorical logic.

Department of Mathematics, University of Manchester, United Kingdom.

E-mail: nicola.gambino@manchester.ac.uk.

Categorical logic, founded by Lawvere in the 1960s, is generally concerned with the interplay between logic and category theory, with applications in both directions. In recent years, motivation from various angles, including theoretical computer science, has led to first steps in the creation of two-dimensional categorical logic, in which ordinary set-based structures are replaced by category-based ones (e.g. equivalence relations are replaced by groupoids), very much in analogy with the research program of categorification in algebra.

After reviewing the basics of categorical logic and outlining the key aspects of two-dimensional categorical logic, I will focus on an illustrative example, namely the 2-category of analytic functors, introduced in [3] and studied further in [4]. This 2-category possesses a wealth of structure, thus giving a good indication of the potential and complexity of two-dimensional categorical logic. In particular, it provides a model of the differential $\lambda $ -calculus [1], an extension of the $\lambda $ -calculus with a differential operator, in which it is possible to approximate $\lambda $ -terms by a form of the Taylor series expansion [2].

[1] T. Ehrhard and L. Regnier, The differential lambda-calculus, Theoretical Computer Science , vol. 309 (2003), pp. 1–41.

[2] , Uniformity and the Taylor expansion of ordinary lambda terms, Theoretical Computer Science , vol. 403 (2008), no. 2–3, pp. 347–372.

[3] M. Fiore, N. Gambino, M. Hyland and G. Winskel, The cartesian closed bicategory of generalised species of structures, Journal of the London Mathematical Society , vol. 77 (2008), no. 2, pp. 203–220.

[4] N. Gambino and A. Joyal, On operads, bimodules and analytic functors, Memoirs of the American Mathematical Society , vol. 249 (2017), no. 1184, pp. 1–110.

▸GABRIEL GOLDBERG, Large cardinals and the Ultrapower Axiom.

Department of Mathematics, University of California Berkeley, United States.

E-mail: ggoldberg@berkeley.edu.

Gödel’s constructible universe L provides a canonical model of ZFC in which one can study classical set theory without encountering unsolvable problems: typically, one cannot expect a given set theoretic question to be answerable assuming just the ZFC axioms, but one can always answer the relativization of the question to L. In one respect, however, L is defective: some of the most commonly used set theoretic hypotheses, large cardinal axioms, do not hold in L, so the constructible universe cannot be used to understand them. One of major projects in modern set theory is the inner model program, which seeks to construct canonical models generalizing of the constructible universe and satisfying large cardinal axioms. Such generalizations have been obtained for large cardinal axioms well into the hierarchy of Woodin cardinals, but it remains open whether it is possible to extend the pattern further – for example, to supercompact cardinals. The subject of this talk is the Ultrapower Axiom (UA), a set theoretic principle that abstracts some of the large cardinal combinatorics of canonical models of set theory. UA holds in any model built by anything like the current methodology of inner model theory, so by developing the theory of supercompact cardinals under the assumption of UA, one can obtain information about how to build canonical models at this level, or perhaps rule out that such a model exists at all. I’ll discuss the theory of supercompact cardinals under UA developed in my PhD thesis and more recent results applying these ideas to other problems in set theory.

▸MARTINO LUPINI, Definable refinements of classical algebraic invariants.

Department of Mathematics, University of Bologna. Italy.

E-mail: martino.lupini@unibo.it.

In this talk I will explain how methods from logic allow one to construct refinements of classical algebraic invariants that are endowed with additional topological and descriptive set-theoretic information. This approach brings to fruition initial insights due to Eilenberg, Mac Lane, and Moore (among others) with the additional ingredient of recent advanced tools from logic. I will then present applications of this viewpoint to invariants from a number of areas in mathematics, including operator algebras, group theory, algebraic topology, and homological algebra.

▸IGOR C. OLIVEIRA, Meta-mathematics of computational complexity theory.

Department of Computer Science, University of Warwick, UK.

E-mail: igor.oliveira@warwick.ac.uk.

Despite significant efforts from computer scientists and mathematicians, the P vs. NP problem and other fundamental questions about the complexity of computations remain out of reach for existing techniques. The difficulty of making progress on such problems has motivated a number of researchers to investigate the logical foundations of computational complexity.

Over the last few decades, several works at the intersection of logic and complexity theory showed that certain fragments of Peano Arithmetic collectively known as Bounded Arithmetic can formalize a large fraction of results from algorithms and complexity (e.g., the PCP Theorem [6] and complexity lower bounds against restricted classes of Boolean circuits [5]). It is natural to consider if the same theories can settle longstanding problems about the inherent difficulty of computations (see [7, 8, 3] for some early papers on this topic).

In this talk, I will discuss the unprovability of certain statements of interest to complexity theory in theories of Bounded Arithmetic [1, 2, 4] and mention a few related open problems.

[1] Bydzovsky, Jan and Krajícek, Jan and Oliveira, Igor C., Consistency of circuit lower bounds with bounded theories, Logical Methods in Computer Science , vol. 16 (2020), no. 2.

[2] Carmosino, Marco and Kabanets, Valentine and Kolokolova, Antonina and Oliveira, Igor C., LEARN-uniform circuit lower bounds and provability in bounded arithmetic, Symposium on Foundations of Computer Science (FOCS’2021) .

[3] Cook, Stephen A. and Krajíček, Jan, Consequences of the provability of $\mathsf {NP} \subseteq \mathsf {P}/\mathsf {poly}$ , Journal of Symbolic Logic , vol. 72 (2007), no. 4, pp. 1353–1371.

[4] Li, Jiatu and Oliveira, Igor C., Unprovability of strong complexity lower bounds in bounded arithmetic, Symposium on Theory of Computing (STOC’2023) .

[5] Müller, Moritz and Pich, Ján, Feasibly constructive proofs of succinct weak circuit lower bounds, Annals of Pure and Applied Logic , vol. 171 (2020), no. 2.

[6] Pich, Ján, Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic, Logical Methods in Computer Science , vol. 11 (2015), no. 2.

[7] Razborov, Alexander A., Bounded arithmetic and lower bounds in Boolean complexity, Feasible Mathematics II (Clote, Peter and Remmel, Jeffrey, editors), Birkhäuser, 1995, pp. 344–386.

[8] , Unprovability of lower bounds on circuit size in certain fragments of bounded arithmetic, Izvestiya: Mathematics , vol. 59 (1995), no. 1, pp. 205.

▸FRANCESCA POGGIOLESI, Explanatory derivations in first-order logic.

IHPST, UMR 8590, Université Paris 1 Panthéon-Sorbonne.

E-mail: poggiolesi@gmail.com.

To explain phenomena in the world, to answer the question “why” rather than the question “what”, is one of the central human activities and one of the main goals of rational inquiry. There are several types of explanation: one can explain by drawing an analogy, as one can explain by dwelling on the cause of a certain phenomenon (see e.g. see [4]). Amongst these different kinds of explanation, in the last decade philosophers have become receptive to those explanations which explain by providing the reasons why a statement is true; these explanations are called “non-causal” or “conceptual” explanations (e.g. see [1]). Conceptual explanations derive their explanatory power from a network of conceptual relations and for this feature, they are prime facie a natural object for logical analysis. The main aim of the talk is to propose a logical account of conceptual explanations. We will do so by using the resources of proof theory, in particular the sequent calculus, and by introducing the novel notion of formal explanation in first-order logic (i.e. we will extend and enrich the work developed in [2], [3]). The results we provide not only shed light on conceptual explanations themselves, but also on the role that logic and logical tools might play in the burgeoning field of inquiry concerning explanation.

[1] Lange, M., Because Without Cause: Non-causal Explanations in Science and Mathematics , Oxford University Press, 2017.

[2] Poggiolesi, F., On defining the notion of complete and immediate formal grounding, Synthese , vol. 193, pp. 3147-3167, 2016.

[3] , On constructing a logic for the notion of complete and immediate formal grounding, Synthese , vol. 195, pp. 1231-1254, 2018.

[4] Woodward, J., Making Things Happen: A Theory of Causal Explanation , Oxford University Press, 2004.

▸VIORICA SOFRONIE-STOKKERMANS, On symbol elimination in theory extensions and applications to parametric verification.

University of Koblenz, Universitätsstr. 1, Koblenz, Germany.

E-mail: sofronie@uni-koblenz.de.

We present a method proposed in [1] which, given a theory ${\mathcal T}_0$ allowing quantifier elimination, an extension ${\mathcal T}_0 \cup {\mathcal K}$ of ${\mathcal T}_0$ with additional function symbols $\Sigma _1$ whose properties are axiomatised by a set ${\mathcal K}$ of clauses, a set of parameters $\Sigma _{\mathsf {par}} \subseteq \Sigma _1$ , and a set G of ground clauses, computes a universal formula $\Gamma $ containing no functions in $\Sigma _1 \backslash \Sigma _{\mathsf {par}}$ with ${\mathcal T}_0 \cup {\mathcal K} \cup \Gamma \cup G \models \perp $ in a hierarchical way, relying on methods for quantifier elimination in ${\mathcal T}_0$ . (If ${\mathcal T}_0$ does not allow quantifier elimination but has a model completion which does, we can use quantifier elimination in the model completion.)

We identify situations under which $\Gamma $ is the weakest universal formula with the property above, and explain how we used this method for the verification of parametric systems: for generating (weakest) constraints on parameters under which certain properties are guaranteed to be inductive invariants [2]; for iteratively strengthening properties to obtain inductive invariants [3]; in problems from wireless research theory [4].

[1] Viorica Sofronie-Stokkermans, On interpolation and symbol elimination in theory extensions, Logical Methods in Computer Science , vol. 14 (2018), no. 3.

[2] , Parametric systems: Verification and synthesis, Fundamenta Informaticae vol. 173 (2020), no. 2-3, pp. 91–138.

[3] Dennis Peuter, Viorica Sofronie-Stokkermans, On invariant synthesis for parametric systems, Automated Deduction - CADE-27 - 27th International Conference on Automated Deduction, Proceedings (Natal, Brazil), (Pascal Fontaine, editor), Lecture Notes in Computer Science 11716, Springer, 2019, pp. 385–405.

[4] , Symbol elimination and applications to parametric entailment problems, Frontiers of Combining Systems - 13th International Symposium, FroCoS-2021, Proceedings (Birmingham, UK) (Boris Konev and Giles Reger, editors), Lecture Notes in Computer Science 12941, Springer, 2021, pp. 43–62.

▸ZOLTÁN VIDNYÁNSZKY, Finite and infinite: an interplay between distributed computing and Borel combinatorics.

Institute of Mathematics, Eötvös University, Budapest, Hungary.

E-mail: zoltan.vidnyanszky@ttk.elte.hu.

The field of Borel combinatorics investigates definable graphs on Polish spaces and aims at generalizing concepts of finite combinatorics to this realm. In the past couple of years a rich variety of connections have been found to the theory of distributed computing, in fact, it is often possible to prove transfer theorems between the two areas.

In my talk, I will survey some of these connections, focusing on the complexity related aspects of the two fields.

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

▸HORAŢIU CHEVAL, Proof mining, applications to optimization, and interactive theorem proving.

Faculty of Mathematics and Computer Science, University of Bucharest, Str. Academiei 14 010014, Bucharest.

E-mail: horatiu.cheval@unibuc.ro.

The research program of proof mining [3] is concerned with analyzing non-constructive mathematical proofs in order to extract additional quantitative (like effective bounds) or qualitative information (like the uniformity of the bounds or the weakening of the premises) from them. The analysis is guided by proof-theoretical instruments like Gödel’s functional interpretation and Kohlenbach’s monotone version thereof. In this way, theoretical guarantees on the extractability of such information can be given, in the form of general logical metatheorems.

We will begin by giving a brief introduction into the logical machinery behind proof mining. Then, we will present some new results in optimization and nonlinear analysis obtained in this context, concerning modified and generalized versions of the well-established Mann and Halpern iterations. These are joint work with Ulrich Kohlenbach and Laurenţiu Leuştean and can be found in [1, 2].

Finally, we will discuss the formalization of some of these results in the Lean theorem prover and our progress towards implementing the aforementioned logical instruments and metatheorems in Lean.

[1] Horaţiu Cheval and Laurenţiu Leuştean, Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration, Optimization Methods and Software , vol. 37 (2022), no. 6, pp. 2225–2240.

[2] Horaţiu Cheval, Ulrich Kohlenbach and Laurenţiu Leuştean, On modified Halpern and Tikhonov-Mann iterations, Journal of Optimization Theory and Applications , to appear.

[3] Ulrich Kohlenbach, Applied Proof Theory: Proof Interpretations and their Use in Mathematics , Springer Monographs in Mathematics, Springer-Verlag, 2008.

▸MORENIKEJI NERI, A metastable Kronecker’s lemma with applications to the large deviations in the strong law of large numbers.

Department of Computer science, University of Bath, Claverton Down, United Kingdom.

E-mail: mn728@bath.ac.uk.

Let $x_1, x_2,\ldots $ be a sequence of real numbers such that $\sum _{i=1}^\infty x_i < \infty $ and let $0< a_1 \le a_2 \le \ldots $ be such that $a_n \to \infty $ . Kronecker’s lemma states,

as $n \to \infty $

By applying Godel’s Dialectica interpretation, we obtain a finitization of this result as well as the quantitative content of the classical proof of this result in the form of a rate of metastability.

We are then able to use our quantitative results to obtain new rates for the convergence in the strong law of large numbers, for both totally independent (a classic result of Kolmagorov) and pairwise independent sequences of random variables whose distributions are not assumed to be identical, thus, contributing to the study of large deviations in the strong law of large numbers. Furthermore, we are able to better existing rates found in [2].

Lastly, we present a contribution to computability theory, by constructing a sequence of rational numbers that satisfy the premise of Kronecker’s lemma but do not converge with a computable rate of convergence (similar to the famous construction of Specker [4]). Thus, we are able to demonstrate the ineffectiveness of Kronecker’s lemma. We then show how this ineffectiveness trickles down to the law of large numbers by constructing a sequence of computable random variables, that satisfy the premise of the laws of large numbers we shall study, whose averages do not converge with computable rates.

Our work can be seen as a contribution to the proof mining program, which aims to give a computational interpretation to prima facie non-effective proofs through the application of tools from logic. Our work builds on the new and exciting work on proof mining in probability/measure theory, in particular, [1] and [3].

[1] J. Avigad and P. Gerhardy and H. towsner, Local stability of ergodic averages, Transactions of the American Mathematical Society , vol. 362, no. 1, pp. 261–288.

[2] , A simple proof of the strong law of large numbers with rates, Bulletin of the Australian Mathematical Society , vol. 97, no. 3, pp. 513–517.

[3] J. Avigad and E. Dean and J. Rute, A metastable dominated convergence theorem, Journal of Logic and Analysis , vol. 4, pp. 3–19.

[4] E. Specker, Nicht Konstruktiv Beweisbare Sätze der Analysis, Journal of Symbolic Logic , vol. 14, no. 3, pp. 145–158.

▸NICHOLAS PISCHKE, Intensional methods in applied proof theory.

Department of Mathematics, TU Darmstadt, Schlossgartenstr. 7, 64289 Darmstadt, Germany.

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

The logical substrate of applied proof theory in its modern form are the so-called logical metatheorems that classify (and allow for the extraction of) the computational content of mathematical theorems in various areas of pure and applied mathematics (see [3, 4, 5]). In the context of such metatheorems, one (necessarily) has to restrict the extensionality principles allowed in the underlying formal systems (i.e. in general only a weak rule of extensionality will be allowed, see the discussion in [5]). This normally poses only minor problems in actual applications as most objects treated by these systems are naturally extensional. In recent work however, areas of applications have emerged where extensionality issues already occur at the level of the definitions of the most basic objects. I will discuss some recent approaches to logical metatheorems and their underlying systems which crucially rely on the use of intensional objects to avoid such extensionality issues. In particular, I will illustrate the versatile applicability of such intensional approaches by discussing their use in treating set-valued operators [2] (with the prominent examples of accretive and monotone operators in Banach and Hilbert spaces, respectively) as well as dual spaces for general normed spaces and notions from convex analysis like gradients and conjugate functions [1].

[1] N. Pischke, Proof mining for the dual of a Banach space with extensions for Fréchet-differentiable functions, submitted.

[2] , Logical metatheorems for accretive and (generalized) monotone set-valued operators, Journal of Mathematical Logic , to appear.

[3] P. Gerhardy and U. Kohlenbach, General logical metatheorems for functional analysis, Transactions of the American Mathematical Society , vol. 360 (2008), pp. 2615–2660.

[4] U. Kohlenbach, Some logical metatheorems with applications in functional analysis, Transactions of the American Mathematical Society , vol. 357 (2005), no. 1, pp. 89–128.

[5] , Applied Proof Theory: Proof Interpretations and their Use in Mathematics , Springer Monographs in Mathematics, Springer-Verlag Berlin Heidelberg, 2008.

Abstracts of invited talks in the Special Session on Computability Theory

▸ELVIRA MAYORDOMO, Extensions of the point to set principle.

Departamento de Informática e Ingeniería de Sistemas, Instituto de Investigación en Ingeniería de Aragón, Universidad de Zaragoza, Iowa State University.

E-mail: elvira@unizar.es.

URL: http://webdiis.unizar.es/~elvira/.

Effective and resource-bounded dimensions were defined by Lutz in [5] and [4] and have proven to be useful and meaningful for quantitative analysis in the contexts of algorithmic randomness, computational complexity and fractal geometry (see the surveys [1, 6, 2, 12] and all the references in them).

The point-to-set principle (PSP) of J. Lutz and N. Lutz [8] fully characterizes Hausdorff and packing dimensions in terms of effective dimensions in the Euclidean space, enabling effective dimensions to be used to answer open questions about fractal geometry, with already an interesting list of geometric measure theory results (see [3,11] and more recent results in [7, 14, 16, 15]).

In this talk I will review the point-to-set principles focusing on its recent extensions to separable spaces [9] and to Finite-State dimensions [13], and presenting open questions on the oracle and oracle access in PSP.

[1] R. G. Downey and D. R. Hirschfeldt, Algorithmic randomness and complexity , Springer-Verlag, 2010.

[2] J. M. Hitchcock, J. H. Lutz, and E. Mayordomo, The fractal geometry of complexity classes, SIGACT News Complexity Theory Column , vol. 36 (2005), pp. 24–38.

[3] J. Lutz and N. Lutz, Who asked us? How the theory of computing answers questions about analysis, Complexity and Approximation: In Memory of Ker-I Ko (Ding-Zhu Du and Jie Wang, editors), Springer, 2020, pp.48–56.

[4] J. H. Lutz, Dimension in complexity classes, SIAM Journal on Computing , vol. 32 (2003), no. 5, pp.1236–1259.

[5] , The dimensions of individual strings and sequences, Information and Computation , vol. 187 (2003), no. 1, pp. 49–79.

[6] , Effective fractal dimensions, Mathematical Logic Quarterly , vol. 51 (2005), no. 1, pp. 62–72.

[7] , The point-to-set principle, the continuum hypothesis, and the dimensions of hamel bases, Computability , to appear.

[8] J. H. Lutz and N. Lutz, Algorithmic information, plane Kakeya sets, and conditional dimension, ACM Transactions on Computation Theory , vol. 10 (2018), article 7.

[9] J. H. Lutz, N. Lutz, and E. Mayordomo, Dimension and the structure of complexity classes, Theory of Computing Systems , to appear.

[10] , Dimension and the structure of complexity classes, arXiv:2109.05956.

[11] J. H. Lutz and E. Mayordomo, Algorithmic fractal dimensions in geometric measure theory, Handbook of Computability and Complexity in Analysis (V. Brattka and P. Hertling, editors), Springer-Verlag, 2021, 271–302.

[12] E. Mayordomo, Effective fractal dimension in algorithmic information theory, New Computational Paradigms: Changing Conceptions of What is Computable , Springer-Verlag, 2008, pp. 259–285.

[13] , A point to set principle for finite-state dimension, arXiv:2208.00157.

[14] T. Slaman, On capacitability for co-analytic sets, New Zealand Journal of Mathematics , vol. 52 (2022), pp. 865–869.

[15] D. Stull, Optimal oracles for point-to-set principles, 39th International Symposium on Theoretical Aspects of Computer Science (STACS 2022) (P. Berenbrink and B. Monmege, editors), Leibniz International Proceedings in Informatics, vol. 219, 2022, pp. 57:1–57:17.

[16] D. M. Stull, The dimension spectrum conjecture for planar lines, 49th International Colloquium on Automata, Languages, and Programming (ICALP2022) (M. Bojańczyk, E. Merelli, and D. P. Woodruff, editors), Leibniz International Proceedings in Informatics, vol. 229, 2022, pp. 133:1–133:20.

▸KENG MENG NG, Classifications in effective topology and computable analysis.

Division of Mathematical Sciences, Nanyang Technological University, Singapore.

E-mail: kmng@ntu.edu.sg.

We discuss some recent work on effective topological spaces and some attempts to classify spaces using computablity notions. We discuss notions such as universality, metrisability and presentability from the effective point of view. We also discuss how to calibrate spaces via a degree theoretic approach.

▸MANLIO VALENTI, On the structure of Weihrauch degrees.

Department of Mathematics, University of Wisconsin - Madison, United States.

E-mail: manlio.valenti@wisc.edu.

Despite recent efforts, there are still several unanswered questions about the algebraic structure of the Weihrauch lattice. In this talk, we will explore some of these questions. After a brief introduction on Weihrauch/Medvedev degrees, we will present some recent results about the existence of chains in the Weihrauch degrees and provide a characterization for when “long” chains have an upper bound. This is also related to the problem of determining the cofinality of the degrees. We will show that, while for the Medvedev degrees the existence of a cofinal chain is equivalent to CH, for the Weihrauch degrees it is provable in ZFC that there are no cofinal chains. Finally, we will discuss some results on the extendibility of antichains and provide some sufficient conditions for antichains to be extendible. All these results showcase how, despite the close interplay between Medvedev and Weihrauch reducibility, the two lattices have a very different structure.

This is joint work with Steffen Lempp and Alberto Marcone.

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

▸ANUPAM DAS, Fixed points and circularity in logic and computation.

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

E-mail: a.das@bham.ac.uk.

Classical approaches to logic and computation typically restrict induction and recursion principles, relating logical constraints to resource bounds. However such approaches offer only a ‘black box’ treatment induction and recursion, admitting no finer logical or computational decomposition. Contrast this with, say, the use of an $\omega $ -rule in proof theory, recovering a metalogical analysis at the cost of finite presentability. However there is another, perhaps more drastic, approach: circular reasoning. Here the dependency graph of a proof need not be well-founded but is typically regular, akin to low-level computational models with loops while nonetheless enjoying excellent metalogical properties. Logical soundness (or computational totality) is guaranteed by an external condition inspired by $\omega $ -automaton theory.

In this talk I will survey some recent advances at the interface of proof theory and computation via cyclic proofs. At one end, complexity theory, I will show how ideas from Implicit Computational Complexity induce natural combinatorial properties on non-wellfounded proofs that yield expressive characterisations of (non-uniform) complexity classes. At the other end, recursion theory, I will show how circular systems have allowed us to calibrate the computational expressivity of (co)recursion in typed programming languages.

This talk is based on the references below, several of which are joint work with Gianluca Curzi.

[1] Anupam Das, A circular version of Gödel’s T and its abstraction complexity, arXiv:2012.14421, 2020.

[2] , On the logical strength of confluence and normalisation for cyclic proofs, 6th International Conference on Formal Semantics for Computation and Deducation (FSCD 2021) (Buenos Aires, Argentina), (Naoki Kobayashi, editor), vol. 195, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021, pp. 29:1–29:23.

[3] Gianluca Curzi and Anupam Das, Cyclic implicit complexity, LICS’22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (Haifa, Israel), (Christel Baier, editor), Association for Computing Machinery, 2022, pp. 19:1–19:13.

[4] , Non-uniform complexity via non-wellfounded proofs, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023) (Warsaw, Poland), (Bartek Klin and Elaine Pimentel, editors), vol. 252, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023, pp. 16:1–16:18.

[5] , Computational expressivity of (circular) proofs with fixed points, arXiv:2302.14825v1, 2023.

▸JÁN PICH, Towards $\mathsf {P}\ne \mathsf {NP}$ from Extended Frege lower bounds.

Department of Computer Science, University of Oxford, United Kingdom.

E-mail: jan.pich@cs.ox.ac.uk.

The proof complexity approach to the $\mathsf {P}$ versus $\mathsf {NP}$ problem, sometimes refereed to as the Cook-Reckhow program, proceeds by proving lower bounds on lengths of proofs of tautologies in increasingly powerful proof systems - $\mathsf {NP}\ne \mathsf {coNP}$ (and hence $\mathsf {P}\ne \mathsf {NP}$ ) if and only if all propositional proof systems have hard sequences of tautologies that require superpolynomial proof size. A problem with the approach is that we do not know if we ever reach the point of proving a superpolynomial lower bound for all proof systems, if we focus only on concrete ones. In particular, even if we prove lower bounds on lengths of proofs in strong propositional proof systems such as Extended Frege, we might not be able to conclude that $\mathsf {P}\ne \mathsf {NP}$ . In this talk we will connect this issue to several classical questions in complexity theory such as the problem of basing the security of cryptography on $\mathsf {P}\ne \mathsf {NP}$ .

▸ROBERT ROBERE, On propositional proofs and total search problems.

School of Computer Science, McGill, 3480 University Street, Montréal, Canada.

E-mail: robere@cs.mcgill.ca.

Recent work has illustrated a deep relationship between the theories of propositional proof systems and total NP search problems (TFNP). The basic correspondence allows us to associate a total search problem S with each propositional proof system P such that the following holds: for every tautology T, T has a short proof in P if and only if proving T can be “efficiently reduced” to proving the totality of S. This allows us to define a theory of reducibility for proof systems that is analogous to classical reducibility in complexity theory, and it has led to the resolution of a number of open problems in both proof complexity and the theory of TFNP. In this talk we will introduce and survey this recent work.

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

▸CAROLIN ANTOS, Formal concepts, defectiveness and pluralism.

Department of Philosophy, University of Konstanz, Universitätsstraße 10, 78464 Konstanz, Germany.

E-mail: carolin.antos-kuby@uni-konstanz.de.

Formal concepts seem to require a different treatment than concepts from the empirical sciences. It is often assumed that their stability and fixedness makes them impervious against problems occurring with concept change, defectiveness or concept pluralism. In this talk I show how defectiveness can occur in formal concepts without giving up the claim that they are stable and fixed. I will also show how this can lead to a form of concept pluralism in formal contexts.

▸LUCA TRANCHINI, Intensional aspects of proof-theoretic semantics.

Faculty of Computer Science, Tübingen University, Germany.

E-mail: luca.tranchini@gmail.com.

In spite of significant mathematical results, comparatively little attention has been devoted to the notion of identity of proofs in the philosophical literature. I argue that this is unfortunate, as identity of proofs is a powerful tool to investigate intensional aspects of meaning, provided that meaning is characterized in terms of inference rules. To substantiate this claim I summarize the results of two lines of research (pursued in joint work with Paolo Pistone and Peter Schoeder-Heister respectively) in which identity of proofs has been applied to the study of the notion of harmony and of paradoxes. I conclude by briefly discussing some open problems and questions of mathematical, historical and philosophical nature concerning identity of proofs.

▸JACK WOODS, Prospects for modest inferentialism.

University Academic Fellow in Mathematical Philosophy, University of Leeds, United Kingdom.

E-mail: j.woods@leeds.ac.uk.

In this paper I will argue that the combination of two insights from Prior, (1) that there are tonkish sets of natural deduction rules, and (2) that model theoretic accounts of meaning should be viewed as models of underlying intuitive meaning, together show that an otherwise promising form of inferentialism will not work. In particular, I argue that there is no way to formulate conditions on the intuitive meaning of the connectives which simultaneously (a) allow the natural deduction rules to specify the correct particular model theoretic meanings of connectives like conjunction, negation, disjunction, and the conditional while (b) not tacitly specifying the meaning of some of these connectives independently of the natural deduction rules. The upshot of this is that modest forms of inferentialism are unworkable. This is no idle result; philosophers have been repeatedly tempted by this position, even if under slightly different guises.

Abstracts of invited talks in the Special Session on Model Theory

▸VAHAGN ASLANYAN, The Existential Closedness with Derivatives conjecture for the j-function.

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

E-mail: vahagn.aslanyan@manchester.ac.uk.

I will discuss the Existential Closedness conjecture for the modular j-function together with its first two derivatives. It is about the solvability of systems of equations involving $j, j', j"$ in the complex numbers and is an analogue of Zilber’s Exponential Closedness conjecture which is about solvability of equations involving complex exponentiation. I will then explain why these two conjectures are qualitatively different, and what current approaches and partial results are known. I will also show that the Existential Closedness with Derivatives conjecture is significantly harder than its version for j without derivatives. If time permits, I will say a few words about the Modular Zilber-Pink with Derivatives conjecture and how it is related to Existential Closedness with Derivatives.

▸ULLA KARHUMÄKI, Groups of finite Morley rank and supertight automorphisms.

Department of Mathematics and Statistics, University of Helsinki, Finland.

E-mail: ulla.karhumaki@helsinki.fi.

After Morley proved his celebrated Categoricity theorem in 1965, a certain notion of dimension—today called the Morley rank—was recognised fundamental in model theory. This notion generalises the algebraic Zariski dimension and thus the class of groups of finite Morley rank generalises the class of algebraic groups over algebraically closed fields. Another class of groups studied by model theorists is that of pseudofinitegroups. These are groups whose first-order theory only contains sentences which hold in some finite group. It is known that infinite simple pseudofinite groups are (twisted) Chevalley groups over pseudofinite fields and it is conjectured that infinite simple groups of finite Morley rank are Chevalley groups over algebraically closed fields; this conjecture is called the Cherlin-Zilber conjecture.

In her PhD thesis, Uğurlu Kowalski captured the algebraic behaviour of an infinite power of the Frobenius automorphism into the notion of supertight automorphism and suggested a new approach towards the Cherlin-Zilber conjecture. She proved that an infinite simple group of finite Morley rank with a supertight automorphism whose fixed point subgroups are pseudofinite contains an infinite simple pseudofinite subgroup so that the definable closure of this subgroup is the ambient group of finite Morley rank. We will see that if the Lie rank of the simple pseudofinite subgroup is one, then the group of finite Morley rank is algebraic and that, under suitable assumptions, if the Lie rank of the simple pseudofinite subgroup is greater or equal to three, then the group of finite Morley rank is again algebraic. The former result is joint work with Pınar Uğurlu Kowalski and the latter result is joint work with Adrien Deloro and Pınar Uğurlu Kowalski.

▸KONSTANTINOS KARTAS, Beyond the Fontaine-Wintenberger theorem.

Sorbonne Université, Université Paris Cité, CNRS, Institut de Mathématiques de Jussieu-Paris Rive Gauche, Campus Pierre et Marie Curie, case 247, 4 place Jussieu, 75252 Paris cedex 5, France.

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

The idea that p-adic fields are in many ways similar to power series fields over finite fields has been highly influential in arithmetic. This philosophy has had two formal justifications, which were also used to transfer certain results across the two worlds. On one hand, the classical work by Ax-Kochen/Ershov in the’ 60s achieves a transfer principle when $p\to \infty $ . On the other hand, Scholze’s recent theory of perfectoid spaces works for fixed p but in the presence of high (and wild) ramification. I will first review those two methods and then mention some recent joint work with Franziska Jahnke in which we use model-theoretic tools to uncover certain new phenomena in perfectoid arithmetic.

Abstracts of invited talks in the Special Session on Set Theory

▸TAKEHIKO GAPPO, Chang-type models of determinacy.

Institute of Discrete Mathematics and Geometry, TU Wien, Wiedner Hauptstrasse 8-10/104, 1040 Vienna, Austria.

E-mail: takehiko.gappo@tuwien.ac.at.

URL: https://sites.google.com/view/takehikogappo/home.

In [1], a new model of the Axiom of Determinacy was introduced by Grigor Sargsyan. This model is “Chang-type,” in the sense that it contains $\delta ^{\omega }$ for some ordinal $\delta>\Theta $ . First we will present two recent results using such a Chang-type model of determinacy. One is the proof of determinacy in the Chang model from a hod mouse with a Woodin limit of Woodin cardinals, and the other is a consistency result on $\omega $ -strongly measurable cardinals in HOD. We will also introduce a Chang-type model of determinacy with supercompact measures, which extends the result of [1]. This talk is based on several joint works with Navin Aksornthong, James Holland, Sandra Müller, and Grigor Sargsyan.

[1] Grigor Sargsyan, Covering with Chang models over derived models, Advances in Mathematics , vol. 384 (2021), no. 107717.

▸ANDREAS LIETZ, Forcing “ $\mathrm {NS}_{\omega _1}$ is $\omega _1$ -dense” from large cardinals.

Instut für Mathematische Logik und Grundlagenforschung, Universität Münster, Einsteinstrasse 62, 48149 Münster, Germany.

E-mail: andreas.lietz.de@gmail.com.

An ideal I on $\omega _1$ is $\omega _1$ -dense if $(\mathcal P(\omega _1)-I)/I$ with the order induced by inclusion has a dense subset of size $\omega _1$ . Using his $\mathbb {P}_{\mathrm {max}}$ -variation $\mathbb {Q}_{\mathrm {max}}$ , W. Hugh Woodin [1] has shown that ZFC+“ $\mathrm {NS}_{\omega _1}$ is $\omega _1$ -dense” holds in generic extensions of canonical determinacy models. Assuming there is an inaccessible cardinal $\kappa $ which is a limit of ${<}\kappa $ -supercompact cardinals, we show that there is a stationary set preserving forcing $\mathbb {P}$ so that

This answers a question of Woodin [1]. To do so, we introduce a forcing axiom $\mathrm {QM}$ and force it true from large cardinals using two new iteration theorems which allow for destroying stationary sets. We then prove that $\mathrm {QM}$ implies the $\mathbb {Q}_{\mathrm {max}}$ -version of Woodin’s $(*)$ -axiom by modifying methods of Asperó–Schindler [2] from their proof of “ $\mathrm {MM}^{++}$ implies $(*)$ ”. Along the way we get a few other new implications of the form “ $\mathrm {MM}^{++}$ implies $(*)$ ”.

[1] W. Hugh Woodin, The Axiom of Determinacy, Forcing Axioms, and the Nonstationary Ideal , De Gruyter Series in Logic and its Applications, De Gruyter, Berlin, 2010.

[2] David Asperó and Ralf Schindler, Martin’s Maximum $^{++}$ implies Woodin’s axiom $(*)$ , Annals of Mathematics, Second Series , vol. 193 (2021), no. 3, pp. 793–835.

▸ZHIXING YOU, How far is almost strong compactness from strong compactness.

Department of Mathematics, Bar-Ilan University, Ramat-Gan 5290002, Israel.

E-mail: zhixingy121@gmail.com.

In the paper [1], Bagaria and Magidor introduced the notion of almost strong compactness. Here an uncountable cardinal $\kappa $ is almost strongly compact iff for every set I, every $\kappa $ -complete filter on I can be extended to a $\delta $ -complete ultrafilter on I for every uncountable $\delta <\kappa $ . Boney and Brooke-Taylor asked whether the least almost strongly compact cardinal, say $\kappa $ , is strongly compact. Goldberg [2] gives a positive answer for this question in the case $\mathrm {SCH}$ holds from below and $\kappa $ has uncountable cofinality. In this talk, we will give a negative answer for the general case by answering a relavant question of Bagaria and Magidor. This is joint work with Jiachen Yuan, [3].

[1] Joan Bagaria and Menachem Magidor, Group radicals and strongly compact cardinals, Transactions of the American Mathematical Society , vol. 366 (2014), no. 4, pp. 1857–1877.

[2] Gabriel Goldberg, Some combinatorial properties of ultimate L and V, arXiv:2007.04812, 2020.

[3] Zhixing You and Jiachen Yuan, How far is almost strongly compact cardinal from strongly compact cardinal, Journal of Mathematical Logic , to appear, 2023.

Abstract of Contributed Talks

▸STEVE AWODEY, Homotopy type theory: Ten years after.

Departments of Philosophy and Mathematics, Carnegie Mellon University, 5000 Forbes Ave., Pittsburgh, PA, 15213, USA.

E-mail: awodey@cmu.edu.

URL: https://awodey.github.io.

In the 10 years since the IAS Program on Univalent Foundations, which culminated in the release of the HoTT Book [10], substantial progress has been made in the field of homotopy type theory on several fronts, including solutions to leading open problems with both logical and mathematical significance. In work by Coquand et al. [4], the simplicial model of univalence [5] was shown have a constructive counterpart, verifying Voevodsky’s canonicity conjecture. A computational proof assistant [8] was engineered on this basis, and in 2022 was used to finally compute “Brunerie’s number” [6], finishing the formal verification of a proof that was begun at the IAS of the calculation of the fourth homotopy group of the 3-sphere, $\pi _4(S^3)$ [3].

The homotopical semantics of Martin-Löf type theory originated with [2], and was conjectured at the time by the author to provide an internal logic for higher toposes [7]. This was established by Shulman [9] in 2019, giving semantics for HoTT in all Grothendieck $\infty $ -toposes. This talk will report on current research relating the constructive models underlying the new generation of computational proof assistants with the classical homotopy theory of higher toposes [1].

[1] Steve Awodey, Cartesian cubical model categores, July 2023, (arXiv:2305.00893).

[2] Steve Awodey and Michael Warren, Homotopy theoretic models of identity types, Mathematical Proceedings of the Cambridge Philosophical Society , 2009.

[3] Guillaume Brunerie, On the homotopy groups of spheres in homotopy type theory, June 2016, (arXiv:1606.05916).

[4] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg, Cubical type theory: a constructive interpretation of the univalence axiom, 21st International Conference on Types for Proofs and Programs , May 2015, Tallinn, Estonia, pp. 129–162.

[5] Chris Kapulkin and Peter LeFanu Lumsdaine, The simplicial model of univalent foundations (after Voevodsky), Journal of the European Mathematical Society , 2021.

[6] Axel Ljungström, The Brunerie number is -2, Homotopy Type Theory (online) , June 2022, homotopytypetheory.org/2022/06/09/the-brunerie-number-is-2.

[7] Jacob Lurie, Higher topos theory, Princeton University Press , 2009.

[8] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel, Cubical Agda: A dependently typed programming language with univalence and higher inductive types, Proceedings of the ACM on Programming Languages , 3:87:1–29, August 2019.

[9] Michael Shulman, All $(\infty ,1)$ -toposes have strict univalent universes, April 2019, (arXiv:1904.07004).

[10] The Univalent Foundations Program, Homotopy type theory: the univalent foundations of mathematics , The Institute for Advanced Study, 2013, homotopytypetheory.org/book.

▸GUILLERMO BADIA, RONALD FAGIN AND CARLES NOGUERA, Completeness theorems for first-order real-valued logics with multidimensional sentences.

School of Historical and Philosophical Inquiry, University of Queensland, Brisbane, Australia.

E-mail: g.badia@uq.edu.au.

URL: https://sites.google.com/site/guillermobadialogic/home.

IBM Research - Almaden, IBM, San José, California.

E-mail: fagin@us.ibm.com.

URL: https://research.ibm.com/people/ron-fagin.

Department of Information Engineering and Mathematics, University of Siena, Siena, Italy.

E-mail: carles.noguera@unisi.it.

URL: https://sites.google.com/view/carlesnoguera/.

Many-valued logics in general, and real-valued logics in particular, usually focus on a notion of consequence based on preservation of full truth, typically represented by the value $1$ in the semantics given in the real unit interval $[0,1]$ . In a recent paper [1], Ronald Fagin, Ryan Riegel, and Alexander Gray have introduced a new paradigm that allows to deal with inferences in propositional real-valued logics based on a rich class of sentences, multi-dimensional sentences, that talk about combinations of any possible truth-values of real-valued formulas. They have given a sound and complete axiomatization that tells exactly when a collection of combinations of truth-values of formulas imply another combination of truth-values of formulas. In this talk, we will extend their work to the first-order (as well as modal) logic of multi-dimensional sentences. We will give axiomatic systems and prove corresponding completeness theorems, first assuming that the structures are defined over a fixed domain, and later for the logics of varying domains. As a by-product, we will also obtain a 0-1 law for finitely-valued versions of these logics.

[1] Ronald Fagin, Ryan Riegel and Alexander Gray, Foundations of Reasoning with Uncertainty via Real-valued Logics, 2021, arXiv:2008.02429v2.

▸GUILLERMO BADIA AND DAVID C. MAKINSON, First-order friendliness.

School of Historical and Philosophical Inquiry, University of Queensland, Brisbane, Australia.

E-mail: g.badia@uq.edu.au.

https://sites.google.com/site/guillermobadialogic/.

School of Historical and Philosophical Inquiry, University of Queensland, Brisbane, Australia.

E-mail: d.makinson@uq.edu.au.

URL: https://sites.google.com/site/davidcmakinson/.

The relation of logical friendliness, introduced in the propositional context in [1], has a very straightforward definition as a $\forall \exists $ version of the fundamental $\forall \forall $ notion of consequence. Specifically, if $\Gamma $ is a set of formulae of classical propositional logic and $\phi $ is a formula of the same, $\Gamma $ is said to be friendly to $\phi $ iff for every valuation v on the propositional variables occurring in formulae of $\Gamma $ , if $v(\gamma )=1$ for all $\gamma \in \Gamma $ then there is an extension of v to a valuation $v'$ covering also any remaining variables in $\phi $ such that $v(\phi ) = 1$ . It is thus a weakening of classical consequence and if the existential quantifier in its definition is replaced by a universal one, it reverts to the classical relation.

So defined, friendliness has a number of interesting features. While lacking some familiar properties of classical consequence, it satisfies some others in full, as well as yielding ‘local’ versions of yet others, as shown in [1]. However, if we seek to extend the definition from the propositional to the first-order context, a number of options arise due to the greater complexity of the notion of a first-order model, with its ingredients of domain of discourse, values for individual constants, values for predicate and function letters, and the equality relation. The various options generate distinct relations, which differ in their behaviour. Indeed, two of the lessons of the present paper are that the concept of friendliness is less robust in the first-order context than in the propositional one and that even the seemingly best behaved of the possible first-order options is less regular than its propositional counterpart, notable with respect to compactness, axiomatizability and interpolation.

The full paper, published by The Review of Symbolic Logic, is available online at https://doi.org/10.1017.S175502032300014X.

[1] D. Makinson, Friendliness and sympathy in logic, Logica Universalis (2nd Edition), (JY Beziau, editor), Birkhauser Verlag, 2007, pp. 195–224.

▸PHILIPPE BALBIANI AND TINKO TINCHEV, Modal definability in Euclidean modal logics.

Toulouse Institute of Computer Science Research, CNRS – Toulouse University, 118 Route de Narbonne, F-31062 Toulouse cedex 9, France.

E-mail: philippe.balbiani@irit.fr.

Faculty of Mathematics and Informatics, Sofia University St. Kliment Ohridski, Blvd. James Bourchier 5, Sofia 1164, Bulgaria.

E-mail: tinko@fmi.uni-sofia.bg.

A Kripke frame $(W,R)$ is called Euclidean if the accessibility relation R satisfies the condition: for all $s,t,u\in W$ , if $sRt$ and $tRu$ then $tRu$ and $uRt$ . A modal logic L is called Euclidean if it is determined by a nonempty class of Euclidean frames, i.e. if L is an extension of the modal logic $K5$ . For every logic L, let $Fr(L)$ be the class of all frames validating the theorems of L. A sentence A from the first-order language with equality and one binary predicate symbol is modally definable with respect to some class of frames if there is a modal formula $\varphi $ from the classical propositional modal language such that A and $\varphi $ are valid in the same frames from the class. Modal definability in a logic L problem asks whether there exists an algorithm that recognizes all modally definable with respect to $Fr(L)$ sentences. Correspondence problem in a logic L asks whether there exists an algorithm that for any sentence A and any modal formula $\varphi $ recognizes whether A and $\varphi $ are valid in the same frames from $Fr(L)$ .

In this talk we present all Euclidean modal logics L such that the modal definability in L is decidable problem. We demonstrate also that these logics are exactly the Euclidean logics in which the correspondence problem is decidable.

▸AINUR BASHEYEVA AND SVETLANA LUTSAK $^{*}$ , On quasivarieties generated by some finite modular lattices.

Department of Algebra and Geometry, L.N. Gumilev Eurasian National University, 13 Kazhymukan, 010008, Astana, Kazakhstan; Department of Computational and Data Science, Astana IT University, 55/11 Mangilik El Avenue, 010000, Astana, Kazakhstan.

E-mail: basheyeva3006@gmail.com.

Department of Mathematics and Computer Science, M. Kozybayev North Kazakhstan University, 86 Pushkin, 150000, Petropavlovsk, Kazakhstan.

E-mail: sveta_lutsak@mail.ru.

In 1970 R. McKenzie [1] proved that any finite lattice has a finite basis of identities. However the similar result for quasi-identities is not true. That is, there is a finite lattice that has no finite basis of quasi-identities (V.P. Belkin 1979 [2]). The problem “Which finite lattices have finite bases of quasi-identities?”was suggested by V.A. Gorbunov and D.M. Smirnov in 1979 [3]. In 1984 V.I. Tumanov [4] found a sufficient condition consisting of two parts under which the locally finite quasivariety lattice has no finite (independent) basis of quasi-identities. Also he conjectured that a finite (modular) lattice has a finite basis of quasi-identities if and only if a quasivariety generated by this lattice is a variety. In general, the conjecture is not true. In 1989 W. Dziobiak [5] found a finite lattice that generates finitely axiomatizable proper quasivariety. Also we would like to note that Tumanov’s problem is still unsolved for modular lattices.

The main goal of this work is to present the specific finite modular lattice $\mathcal {L}$ that does not satisfy all conditions of Tumanov’s theorem but the quasivariety $\mathbf {Q}(\mathcal {L})$ generated by this lattice is not finitely based (has no finite basis of quasi-identities). The main result of the work is proved in [6].

The first author is funded by the Science Committee of the Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP13268735). The second author is funded by the Science Committee of the Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP09058390).

[1] R. McKenzie, Equational bases for lattice theories, Mathematica Scandinavica , vol. 27 (1970), pp. 24–38.

[2] V.P. Belkin, Quasi-identities of finite rings and lattices, Algebra and Logic , vol. 17 (1979), pp. 171–179.

[3] V.A. Gorbunov and D.M. Smirnov, Finite algebras and the general theory of quasivarieties, Colloquia Mathematica Societatis Janos Bolyai. Finite Algebra and Multipli-valued Logic , vol. 28 (1979), pp. 325–332.

[4] V.I. Tumanov, On finite lattices having no independent bases of quasi-identities, Mathematical Notes , vol. 36 (1984), pp. 625–634.

[5] W. Dziobiak, Finitely generated congruence distributive quasivarieties of algebras, Fundamenta Mathematicae , vol. 133 (1989), pp. 47–57.

[6] A.O. Basheyeva and S.M. Lutsak, On quasi-identities of finite modular lattices. II, Bulletin of the Karaganda University. Mathematics series , vol. 110 (2023), no. 2, pp. 45–52.

▸GAIA BELARDINELLI AND THOMAS BOLANDER, Attention! Dynamic epistemic logic models of (in)attentive agents.

Department of Communication, University of Copenhagen, Karen Blixens Plads 8, building 16, 1st floor, DK-2300 Copenhagen S, Denmark.

E-mail: belardinelli@hum.ku.dk.

DTU Compute, Technical University of Denmark, Richard Petersens Plads, DK-2800 Lyngby, Denmark.

E-mail: tobo@dtu.dk.

Attention is the crucial cognitive ability that limits and selects what information we observe. Previous work by Bolander et al. [1] proposes a model of attention based on dynamic epistemic logic (DEL) where agents are either fully attentive or not attentive at all. While introducing the realistic feature that inattentive agents believe nothing happens, the model does not represent the most essential aspect of attention: its selectivity. Here, we propose a generalization that allows for paying attention to subsets of atomic formulas. We introduce the corresponding logic for propositional attention, and show its axiomatization to be sound and complete. We then extend the framework to account for inattentive agents that, instead of assuming nothing happens, may default to a specific truth-value of what they failed to attend to (a sort of prior concerning the unattended atoms). This feature allows for a more cognitively plausible representation of the inattentional blindness phenomenon, where agents end up with false beliefs due to their failure to attend to conspicuous but unexpected events. We prove the extended logic to be sound and complete as well. Both versions of the model define attention-based learning through appropriate DEL event models based on a few and clear edge principles. While the size of such event models grow exponentially both with the number of agents and the number of atoms, we introduce a new logical language for describing event models syntactically and show that using this language our event models can be represented linearly in the number of agents and atoms. Furthermore, representing our event models using this language is achieved by a straightforward formalisation of the aforementioned edge principles.

The full paper is available here: https://arxiv.org/abs/2303.13494

[1] Thomas Bolander, Hans van Ditmarsch, Andreas Herzig, Emiliano Lorini, Pere Pardo, and François Schwarzentruber, Announcements to Attentive Agents, Journal of Logic, Language and Information , vol. 25 (2016), pp. 1–35.

▸LUCA BELLOTTI, Notes on the (un)provability of consistency.

Department CFS (Philosophy), University of Pisa - Via Paoli 15, 56126 Pisa, Italy.

E-mail: luca.bellotti@unipi.it.

We present a few remarks on the classic problem of the unprovability of consistency of some important formal systems and on some ways to (partially) circumvent it which have been proposed. We consider the impossibility of certain constructive consistency proofs for set theory, the role of local set-theoretic reflection principles and of partial or indirect consistency statements for arithmetic, with a final remark on so-called Whiteley sentences.

▸JOSÉ MIGUEL BLANCO AND FÉLIX CUADRADO, Formal modelling of distributed temporal graphs algorithms: the case of Raphtory.

Universidad Politécnica de Madrid, Av. Complutense 30, 28040, Madrid, Spain.

E-mail: josemiguel.blanco@upm.es.

URL: https://sites.google.com/view/jmblancos.

E-mail: felix.cuadrado@upm.es.

The rise of temporal graphs has also produced many tools to delve into their analytics and provide real-time support for decision-making. Nevertheless, these tools are based on complex underlying models whose behaviour needs to be ensured so no unexpected side-effects or ill behaviour happens. For that matter formal modelling is an option that has been used extensively, ensuring results like the decidability of the system or enabling the possibility of performing a model check.

Thus, the main aim of this communication is to provide the formal modelling of Raphtory, an open-source platform for distributed real-time temporal graph analytics [1]. For that matter we will make use of Routley-Meyer semantics [2] as they are one of the best tools to model distributed systems, and we will extend them by introducing a time-flow with branching time operators. All this will allow us to obtain a perfect representation of Raphtory and derive its properties.

Acknowledgements. This work has been supported by the Madrid Government (Comunidad de Madrid-Spain) under the Multiannual Agreement with Universidad Politécnica de Madrid in the line Support for R&D projects for Beatriz Galindo researchers, in the context of the V PRICIT (Regional Programme of Research and Technological Innovation).

[1] Benjamin Steer, Félix Cuadrado and Richard Clegg, Raphtory: Streaming analysis of distributed temporal graphs, Future Generation Computer Systems , vol. 102 (2020), pp. 453–464.

[2] Richard Routley, Robert K. Meyer, Ross T. Brady and Valerie Plumwood, Relevant Logics and Their Rivals, vol. 1 , Ridgeview Publishing Company, 1982.

▸SAMUEL BRAUNFELD, ANUJ DAWAR, IOANNIS ELEFTHERIADIS AND ARIS PAPADOPOULOS, Monadic NIP in monotone classes of relational structures.

Charles University (IUUK), Praha, Czech Republic.

E-mail: sbraunfeld@iuuk.mff.cuni.cz.

Department of Computer Science and Technology, University of Cambridge, UK.

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

Department of Computer Science and Technology, University of Cambridge, UK.

E-mail: ie257@cam.ac.uk.

School of Mathematics, Univesity of Leeds, UK.

E-mail: mmadp@leeds.ac.uk.

We prove that for any monotone class of finite relational structures, the first-order theory of the class is NIP in the sense of stability theory if, and only if, the collection of Gaifman graphs of structures in this class is nowhere dense. This generalises to relational structures a result previously known for graphs and answers an open question posed by Adler and Adler in [1].

The result is established by the application of Ramsey-theoretic techniques and shows that the property of being NIP is highly robust for monotone classes. We also show that the model-checking problem for first-order logic is intractable on any class of monotone structures that is not (monadically) NIP. This is a contribution towards the conjecture of Bonnet et al. from [2] that the hereditary classes of structures admitting fixed-parameter tractable model-checking are precisely those that are monadically NIP.

[1] Hans Adler and Isolde Adler, Interpreting nowhere dense graph classes as a classical notion of model theory, European Journal of Combinatorics , vol. 36 (2014), pp. 322–330.

[2] Bonnet, Édouard and Giocanti, Ugo and de Mendez, Patrice Ossona and Simon, Pierre and Thomassé, Stéphan and Toruńczyk, Szymon, Twin-width IV: ordered graphs and matrices, 2021, arXiv:2102.03117.

▸SELMER BRINGSJORD, NAVEEN SUNDAR GOVINDARAJULU AND ALEXANDER BRINGSJORD, Three-dimensional hypergraphical natural deduction.

Rensselaer AI & Reasoning Lab, Department of Computer Science and Department of Cognitive Science, Rensselaer Polytechnic Institute, Troy NY USA.

E-mail: selmer.bringsjord@gmail.com.

Rensselaer AI & Reasoning Lab, and Department of Cognitive Science, Department of Cognitive Science, Rensselaer Polytechnic Institute, Troy NY USA.

E-mail: naveen.sundar.g@gmail.com.

Motalen Labs, Troy NY USA.

E-mail: alexanderbringsjord@gmail.com.

As is widely known, natural deduction was first presented in 1934, independently by Gentzen [2] and Jáśkowski [3]; this event gave rise to three fundamental and fundamentally different ways of rendering such deduction precise, a trio that firmly persists to the present day. Gentzen gave a tree format for natural deduction; Jáśkowski gave a box-based one, and a tabular, “bookkeeping” one. (Pelletier [4] credits Suppes with a fourth way, but this is controversial, since Suppes’ innovation is a formalism for tracking suppositions that remain in force as a proof proceeds in Jáśkowskian tabular fashion.) We first briefly review the three natural-deduction ways, and show our expansion of Genzen’s trees into a novel system based on (usually directed, acyclic) hypergraphs. (Hypergraphs are covered e.g. in [1] and — more recently — in [5].) We next show that our system (in two-dimensional mode) is implemented and integrated with automated reasoners (= “oracles”), via specimen formal proofs that range over third-order logic, with additional optional modal operators available for the alethic, epistemic, deontic cases etc. We then explain that the three original specifications for natural deduction, despite their differences, are most assuredly in any case two-dimensional: each element therein is located somewhere in a backdrop of an x and a y axis, as in simple, discrete Euclidean two-space. We then reveal how natural deduction in our hypergraphical environment can be better expressed in three-dimensional hypergraphs. Our 3D hypergraphical proofs use a third z axis on which formulae in nodes can be located, to and from which run inferential arcs. This third dimension, as we explain and show in relevant proofs, can be interpreted, within proof-theoretic semantics, as e.g. determining the degree of “prominence” of formulae and inferential links in a given proof.

We conclude with some remarks about connections we perceive between 3D hypergraphical natural reasoning and the dream of Leibniz to find a rigorous universal reasoning system. Leibniz dreamed of an interoperating pair: (i) the calculus ratiocinator, the machine or mechanical system, which brings information expressed in (ii) the universal rational calculus, or characteristica universalis, to life. Our system, we claim, realizes this dream.

[1] Claude Berge, Graphs and Hypergraphs , North-Holland, 1973.

[2] Gerhard Gentzen, Untersuchungen über das logische Schliezen I & II, Mathematische Zeitschrift , vol. 39 (1934), pp. 176–210, 405–431.

[3] Stanislaw Jáśkowski, On the Rules of Suppositions in Formal Logic, Studia Logica , vol. 1 (1934), no. 1, pp. 5–32.

[4] Francis Pelletier, A Brief History of Natural Deduction, History and Philosophy of Logic , vol. 20 (1999), pp. 1–31.

[5] Vitaly Voloshin, Introduction to Graph and Hypergraph Theory , Nova Kroshka, 2013.

▸GABRIELE BURIOLA, PETER SCHUSTER AND ANDREAS WEIERMANN, Proof-theoretic relations between Higman’s and Kruskal’s theorems.

Dept. of Computer Science, University of Verona, Italy.

E-mail: Gabriele.Buriola@UniVr.it, Gabriele.Buriola@UGent.be.

Dept. of Computer Science, University of Verona, Italy.

E-mail: Peter.Schuster@UniVr.it.

Dept. of Computer Science, University of Ghent, Belgium.

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

Higman’s lemma and Kruskal’s theorem are two of the most celebrated results in the theory of well quasi-orders. In his seminal paper [1], Higman obtained what is known as Higman’s lemma as a corollary of a more general theorem, dubbed here Higman’s theorem. Kruskal was well aware of this more general set up; in the very end of his famous article [2], he explicitly stated how Higman’s theorem is a special version, the restriction to trees of finite branching degree, of Kruskal’s own tree theorem. This correspondence has been formalized subsequently by Pouzet [3]. We now transfer Pouzet’s proof to the context of Reverse Mathematics, proving its validity over RCA $_0$ and establishing various related proof-theoretic implications; moreover, extending the investigations by Rathjen and Weiermann [4], we calculate the proof-theoretic ordinals of the versions of Kruskal’s theorem occurring in this context.

[1] G. Higman, Ordering by divisibility in abstract algebras, Proceedings of the London Mathematical Society , vol. 3 (1952), no. 2, pp. 326–336.

[2] J.B. Kruskal, Well-quasi-ordering, the tree theorem, and Vazsonyi’s conjecture., Transactions of the American Mathematical Society , vol. 95 (1960), pp. 210–225.

[3] M. Pouzet, Applications of well quasi-ordering and better quasi-ordering, Graphs and order Publisher Springer, Year 1985, pp. 503–519.

[4] M. Rathjen and A. Weiermann, Proof-theoretic investigations on Kruskal’s theorem, Annals of Pure and Applied Logic , vol. 60 (1993), pp. 49–88.

▸ARTEM BURNISTOV, ALEXEY STUKACHEV AND MARINA STUKACHEVA, Computable functionals in Montague semantics.

Novosibirsk State University, Pirogova str. 1, Novosibirsk, 630090, Russia; CRI, Mines Paris, PSL University 35, rue Saint-Honore, Fontainebleau Cedex, 77305, France.

E-mail: artem.burnistov@etu.minesparis.psl.eu.

Novosibirsk State University, Pirogova str. 1, Novosibirsk, 630090, Russia; Sobolev Institute of Mathematics, Acad. Koptyug avenue 4, Novosibirsk, 630090, Russia.

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

Novosibirsk State University, Pirogova str. 1, Novosibirsk, 630090, Russia.

E-mail: stukacheva@yahoo.com.

We consider algorithmic properties of mathematical models used in computational linguistics to formalize and represent the semantics of natural language sentences. In particular, finite-order functionals play a crucial role in Montague intensional logic and formal semantics for natural languages [2]. We compare several computable (in sense of [1]) models for the spaces of finite-order functionals based on Ershov-Scott theory of domains and approximation spaces. Namely, we describe how complexity and representability of functional spaces depend from the choice of three basic domains: for entities, for truth values, and for states. This work continues the research started in [3,4,5] and is supported by the IM SB RAS state assignment, project number FWNF-2022-0012.

[1] Yu.L. Ershov, Definability and computability , Plenum, New York, 1996.

[2] D.R. Dowty, R.E. Wall and S. Peters, Introduction to Montague semantics , D. Reidel Publishing Company, 1989.

[3] A.I. Stukachev, Approximation spaces of temporal processes and effectiveness of interval semantics, Advances In Intelligent Systems and Computing , vol. 1242 (2021), pp. 53–61.

[4] , Interval extensions of orders and temporal approximation spaces, Siberian Mathematical Journal , vol. 62 (2021), no. 4, pp. 730–741.

[5] A.S. Burnistov and A.I. Stukachev, Generalized computable models and Montague semantics, Studies in Computational Intelligence , vol. 1081 (2023), pp. 107–124.

▸WESLEY CALVERT, DOUGLAS CENZER AND VALENTINA HARIZANOV, Generically computable structures.

School of Mathematical and Statistical Sciences, Southern Illinois University, Carbondale, IL 62901, USA.

E-mail: wcalvert@siu.edu.

Department of Mathematics, University of Florida, Gainesville, FL 32611, USA.

E-mail: cenzer@ufl.edu.

Department of Mathematics, George Washington University, Washington, DC 20052, USA.

E-mail: harizanv@gwu.edu.

Inspired by the study of generic computability of sets, based on the notion of asymptotic density and introduced in computability theory by C. Jockusch and P. Schupp, we extended such investigation to the context of computable structure theory. We introduced and studied the notion of a generically computable structure and its variants. We say that a countable structure is generically computable if it has a substructure the domain of which is a computably enumerable and asymptotically dense set and where the functions and characteristic functions of relations extend to partial computable functions. There are two directions in which this notion of generically computable structures could potentially trivialize: either all structures from a certain algebraic class have generically computable isomorphic copies, or only those having computable (or computably enumerable) copies. While we previously investigated generic and dense computability in general for equivalence structures and for directed graphs induced by one-to-one functions, our more recent focus is on generically computable Abelian groups. For example, any (countable) Abelian p-group has a generically computable isomorphic copy. We further characterize arbitrary Abelian groups that have generically computable isomorphic copies, or other variants of densely computable copies.

▸MATTEO CRISTANI, SREEHARI KALOORMANA AND LUCA PASETTO, Reasoning about ensemble learning algorithms with Justification Logic.

Dipartimento di Informatica, Università degli studi di Verona, Strada Le Grazie 15, Verona, Italy.

E-mail: matteo.cristani@univr.it.

Department of Computer Science, CUNY Graduate Center, 365 Fifth Avenue, New York, USA.

E-mail: skalloormana@gradcenter.cuny.edu.

Dipartimento di Informatica, Università degli studi di Verona, Strada Le Grazie 15, Verona, Italy.

E-mail: luca.pasetto@univr.it.

An ensemble learning algorithm is a predictive method that uses multiple learning algorithms to obtain better results than it could obtain by using only one of those algorithms [4]. An algorithm, or an ensemble of them, is said to be opaque when its internal workings are not transparent, making it challenging to understand how it makes decisions or to identify the factors that influence those decisions [3].

Justification Logic (specifically LP, the Logic of Proofs) was introduced by Artemov [1]. It allows one to introduce the notion of proofs or justifications in the object language. Instead of writing $\Box X$ to mean that “X is knowable” or that “X is provable”, one writes $t:X$ to mean that “t is a justification of X” or that “t is a proof of X” [2].

In this work, we present a first appraisal at reasoning on the opacity of ensemble learning algorithms through Justification Logic, so that a logical explanation of such algorithms can be given.

[1] S. Artemov, Operational modal logic, Technical Report MSI 95–29 , Cornell University, 1995.

[2] S. Artemov and M. Fitting, Justification Logic: Reasoning with Reasons , Cambridge Tracts in Mathematics, Cambridge University Press, 2019.

[3] J. Burrell, How the machine ‘thinks’: Understanding opacity in machine learning algorithms, Big Data & Society , vol. 3 (2016), no. 1.

[4] O. Sagi and L. Rokach, Ensemble learning: A survey, WIREs Data Mining and Knowledge Discovery , vol. 8 (2018), no. 8:e1249.

▸RAFAEL DA SILVA DA SILVEIRA, Precursors of the mathematization of thought applied to logic.

Instituto Federal de Ciência e Tecnologia do Amapá – IFAP campus Santana.

E-mail: rafael.silveira.ifap.edu.br.

By mathematization of thought, understand the slow process that leads to effective formalization in logic, with the aim of employing mathematical linguistic and notational structures, e.g. the use of variables, the analysis of combinations and the use of axioms to express an inference; operations with terms that, later, would be linked to logic would become his main means of expression.

Thus, with the objective of understanding how this process developed, the construction of such reflections was carried out, which will be presented in a linear way in relation to the history of philosophy, however, such formalization of logic and thought in the mathematical aspect occurred discontinuously and disperse. For this linearization, aspects related to logic research, formalization and the relationship between mathematics and thought were considered.

Among the thinkers who worked on this project of mathematization of thought and logic, Raimundo Lúlio (1232–1316) and his seven figures of reasoning in Ars Magna, Sebastián Izquierdo (1601–1681) and his combinatorial analysis stood out covered in Pharus Scientiarum, Thomas Hobbes (1588–1679) and his concept of addition and subtraction in De Corpore and Gottfried Wilhelm Leibniz (1646–1716) with his other approach to combinatorial analysis in Ars Combinatoria.

[1] L. Couturat, La logique de Leibniz , Felix Alcan, Paris, 1901.

[2] S. Izquierdo, Pharus Scientiarum, Volume 1 , Bourgeat and Liétard, Lyon, 1659.

[3] G.W. Leibniz, Dissertatio de arte combinatoria , Leipzig, 1666.

[4] R. Lúlio, Ars generalis ultima , Minerva, Frankfurt. 1970.

[5] R. Lúlio, The Art of Contemplation , Ignatius Press, San Francisco, 2002.

▸MATTEO DE CEGLIE, The V-logic multiverse and Benacerraf’s challenge.

Philosophy Department of the Cultural and Social Science, University of Salzburg.

E-mail: decegliematteo@gmail.com.

Clarke-Doane (2020) argues that the pluralist stance in the philosophy of mathematics, i.e. the position that any consistent mathematical theory produces a legitimate mathematical universe, can provide an answer to Benacerraf (1973) problem iff we interpret it in terms of safety: our set-theoretic beliefs are reliable iff, for any one of them P, we couldn’t have easily had a false belief as to whether P. In other words, if and only if we can be safe that by entertaining that belief we are not easily making a mistake. For example, the belief that “ $V = L \land \exists 0^{\#}$ ” cannot be held safely, since we have a proof that it is inconsistent, and we cannot have both the conjunctions. However, he also argues that it’s not clear how the pluralist can show that her set-theoretic beliefs are safe. In this paper, I argue there is actually a way for the pluralist to show whether her set-theoretic beliefs are safe. To do so, I propose the following, more precise, safety principle:

If we were to entertain a belief that $\varphi $ , but $\varphi $ cannot be added consistently to any axiomatisation of set theory, then it would be probable that the belief is false, thus not satisfying the Safety principle. At the same time, even if $\varphi $ could be added consistently to an axiomatisation of set theory, if we still cannot find an extension of V that witnesses this addition we would have doubts on the safety of our belief.

[1] Clarke-Doane, Justin, Set-theoretic pluralism and the Benacerraf problem, Philosophical Studies , vol. 177 (2020), no. 7, pp. 2013–2030.

[2] Benacerraf, Paul, Mathematical truth, The Journal of Philosophy , vol. 70 (1973), no. 19, pp. 661–679.

▸PABLO DOPICO, A rose by any other name: more supervalution-style truth without supervaluations.

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

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

One of the main shortcomings of Saul Kripke’s fixed-point semantics based on the Strong Kleene logic, presented for the first time in [1], is that it leaves many logical truths out of the extension of the truth predicate. Thus, as an alternative, Kripke suggests to construct the fixed-point models on the basis of the supervaluationist semantics advanced by van Fraassen [2]. What obtains is a supervaluatonist fixed-point semantics that has arguably constituted one of the most popular solutions to the paradoxes of self-reference.

However, the supervaluationist fixed-point theory of truth is not free from objections. The final picture yields a non-compositional theory of truth whose evaluation scheme is highly intransparent and that cannot be $\mathbb {N}$ -categorically axiomatized [3] like the Kripke-Strong Kleene can. For this reason, Johannes Stern [4] has recently advanced a theory (labelled SSK) that also meets the goal of the Kripkean supervaluationist theory (i.e., to include all first-order logical truths) while allegedly accounting for the failure of compositionality, and allowing for a $\mathbb {N}$ -categorical axiomatization.

Our main contribution in this paper is to show that SSK is strikingly similar to a rather understudied theory: Vann McGee’s theory of definite truth as presented in [5]. Thus, the first part of the paper is devoted to showing that McGee’s theory coincides with the minimal fixed point of Stern’s theory, modulo a suitable restriction of the language of the former. After that, we provide a generalization of McGee’s method that allows us to generate theories matching every inductive fixed point of Stern’s theory, always modulo the same restriction of the language. In sum, we could say that McGee’s theory is an alternative way of obtaining supervaluation-style truth without supervaluations.

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

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

[3] Martin Fischer, Volker Halbach, Jönne Kriener, and Johannes Stern, Axiomatizing semantic theories of truth?, The Review of Symbolic Logic , vol. 8 (2015), no. 2, pp. 257–278.

[4] Johannes Stern, Supervaluation-style truth without supervaluations, Journal of Philosophical Logic , vol. 47 (2018), no. 5, pp. 817–850.

[5] Vann McGee, Truth, Vagueness, and Paradox , Hackett Publishing Company, 1991.

▸FREDRIK ENGSTRÖM AND ORVAR LORIMER OLSSON, The propositional logic of teams.

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

E-mail: fredrik.engstrom@gu.se, orvar.lorimer.olsson@gu.se.

Starting from a logic given by traditional semantics formulated in terms of semantic objects (i.e., assignments, valuations or worlds) team semantics lifts the denotations of formulas to sets, or teams, of semantic objects instead enabling the formulation of properties, such as variable dependency, not available in the traditional setting. Since the introduction by Hodges, and refinement by Väänänen, team semantic constructions have been used to generate expressively enriched logics still conserving nice properties, such as compactness or decidability [1]. In contrast these logics fail to be substitutional, limiting any algebraic treatment, and rendering schematic proof systems impossible. This shortcoming can be attributed to the flatness principle, commonly adhered to when generating team semantics [2].

Investigating the formation of team logics from algebraic semantics, and disregarding the flatness-principle, we present the logic of teams (LT), a substitutional logic for which important propositional team logics are axiomatisable as fragments. Starting from classical propositional logic and Boolean algebras, we give semantics for LT by considering the algebras of the form $\mathcal P B$ for a Boolean algebra B, treated with an internal (derived from B) and an external (set-theoretic) set of connectives. Furthermore, we present a well-motivated labelled natural deduction system for LT, for which a further analysis motivates a generalisation to constructions of logics by combinations of an internal and an external logic, where for LT both are classical propositional logic.

[1] Fan Yang and Jouko Väänänen, Propositional team logics, Annals of Pure and Applied Logic , vol. 168 (2017), no. 7, pp. 1406–1441.

[2] Orvar Lorimer Olsson, Monadic semantics, team logics and substitution , Master’s thesis, University of Gothenburg, 2022, hdl.handle.net/2077/72005.

▸FRANCESCO GALLINARO AND JONATHAN KIRBY, Quasiminimality of complex powers.

Mathematisches Institut, Albert-Ludwigs-Universität Freiburg, Ernst-Zermelo-Str. 1, Freiburg im Breisgau, Germany.

E-mail: francesco.gallinaro@mathematik.uni-freiburg.de.

School of Mathematics, University of East Anglia, NR4 7TJ, Norwich, United Kingdom.

E-mail: jonathan.kirby@uea.ac.uk.

A conjecture due to Zilber predicts that the complex exponential field is quasiminimal: that is, that all subsets of the complex numbers that are definable in the language of rings expanded by a symbol for the complex exponential function are countable or cocountable. Zilber showed that this conjecture would follow from Schanuel’s Conjecture and an existential closedness-type property asserting that certain systems of exponential-polynomial equations can be solved in the complex numbers; later on, Bays and Kirby were able to remove the dependence on Schanuel’s Conjecture, shifting all the focus to the existence of solutions. This talk will discuss recent work about the quasiminimality of a reduct of the complex exponential field, that is, the complex numbers expanded by multivalued power functions.

▸GUIDO GHERARDI AND EUGENIO ORLANDELLI, Logics of super-strict implications.

Department of the Arts, University of Bologna, via Azzo Gardino 23, 40122, Bologna, Italy.

E-mail: guido.gherardi@unibo.it.

E-mail: eugenio.orlandelli@unibo.it.

C.I. Lewis’ [3] strict implication () is a stregthening of material implication ( $\supset $ ) that avoids its paradoxes— $\neg B\supset (B\supset A)$ and $A\supset (B\supset A)$ . It is meant to provide a formal explication of entailment-related uses of implication. Connexivists [4] and relevantists [1] have argued that the paradoxes of strict implication— and —are a reason to discard and they have proposed alternative implications that are paradox-free. One limitation of their proposals is that they involve a major departure from classical logic.

Super-strict implication ( $\vartriangleright $ ) strengthens in order to avoids its paradoxes: $A \vartriangleright B$ is true whenever $A\supset B$ is necessary and A is possible, see [2]. In this way we obtain a paradox-free implication that is compatible with classical logic. This talk provides some motivations for $\vartriangleright $ and studies proof-systems for some important logics of $\vartriangleright $ .

[1] A.R. Anderson and N.D. Belnap, Entailment. The Logic of Relevance and Necessity. Vol. 1 , Princeton University Press, 1975.

[2] G. Gherardi and E. Orlandelli, Super-strict implications, Bulletin of the Section of Logic , vol. 50 (2021), no. 1, pp. 1–34.

[3] C.I. Lewis and C.H. Langford, Symbolic Logic , Century, 1932.

[4] E.J. Nelson, Intensional relations, Mind , vol. (1930), no. 156, pp. 440–453.

▸DAVID GONZALEZ, The $\omega $ -Vaught’s conjecture.

Department of Mathematics, University of California, Berkeley, Evans Hall, University Dr, Berkeley, CA 94720.

E-mail: david_gonzalez@berkeley.edu.

Robert Vaught conjectured that the number of countable models of any given list of axioms must be either countable or continuum, but never in between. Despite all the work that has gone into this conjecture over the past sixty years, it remains open. It is one of the most well-known, long-standing open questions in mathematical logic. We introduce the $\omega $ -Vaught’s conjecture, a strengthening of Vaught’s conjecture for infinitary logic. We believe that a structural proof of Vaught’s conjecture for infinitary logic would actually be a proof of the $\omega $ -Vaught’s conjecture. Furthermore, a counterexample to the $\omega $ -Vaught’s conjecture would likely contain ideas helpful in constructing a counterexample to Vaught’s conjecture.

We prove the $\omega $ -Vaught’s conjecture for linear orderings, a strengthening of Vaught’s conjecture for linear orderings originally proved by Steel [1]. The proof notably differs from Steel’s proof (and any other previously known proof of Vaught’s conjecture for linear orderings) in that it makes no appeal to lemmas from higher computability theory or descriptive set theory.

This talk is based on joint work with Antonio Montalbán.

[1] John R. Steel, On Vaught’s conjecture, Cabal Seminar 76–77 (Proceedings, Caltech-UCLA Logic Seminar 1976–77) , Lecture Notes in Mathematics, vol. 689, (Alexander S. Kechris and Yiannis N. Moschovakis, editors), Springer, 1978, pp. 193–208

▸VALENTIN GORANKO, On modal logics with weakly transitive accessibility relations.

Department of Philosophy, Stockholm University.

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

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

We say that binary relation R on a set W has the weak transitivity property if for every $u,v \in W$ , if v is reachable from u in 3 R-steps, then v is reachable from u in 2 R-steps. Formally, weak transitivity is expressed by the first order sentence

Clearly, every transitive relation is weakly transitive, but not vice versa. Non-transitive but weakly transitive relations do not naturally occur often, but there are several interesting and diverse cases where they do, including:

• • The right (or left) neighbourhood relation between two intervals on a linear order, where an interval j is a right neighbour of the interval i iff the end of i and the beginning of j coincide.

• • The comparability relation between nodes in trees, regarded as models of branching time, where that relation R can be naturally defined as “being on the same history (timeline)”.

• • The edge relation in the countable random graph (aka, Rado graph); more generally, in any graph of diameter 2.

Weak transitivity is frame-definable by the modal formula $\Diamond \Diamond \Diamond p \to \Diamond \Diamond p$ or, equivalently, by $\Box \Box p \to \Box \Box \Box p$ . Added as an axiom to the modal logic $\textbf {K}$ it defines the simplest normal modal logic, $\textbf {K}^2_3$ , for which, to my knowledge, there are no published proofs or disproofs of decidability, nor finite model property.

This work presents and discusses some modal logics – including those associated with the cases above – containing $\textbf {K}^2_3$ but not $\textbf {K}_4$ (that is, with weakly transitive but generally non-transitive relations), including some known and some new results about representation theorems, finite model property, and decidability for them. It also outlines a general approach for proving completeness for axiomatizations of modal logics of $\Pi ^0_2$ -definable classes of frames.

▸ASSYLBEK ISSAKHOV AND ULDANA OSTEMIROVA, Notes on hyperimmunity and computably enumerable equivalence relations.

School of Applied Mathematics, Kazakh-British Technical University, Tole bi st. 59, Almaty 050000, Kazakhstan.

E-mail: asylissakhov@gmail.com.

E-mail: uuldanaustemir@gmail.com.

If $R, S$ are equivalence relations on the set $\omega $ of the natural numbers, we say that R is computably reducible to S (notation: $R\le S$ ) if there exists a computable total function f such that, $(\forall x,y\in \omega ) (xRy\Leftrightarrow f(x) S f(y))$ , [1].

For every set A, let $xR_{A} y\Leftrightarrow (x=y \text { or } {x;y}\subseteq A)$ , and let $x Id y \Leftrightarrow x=y$ . An infinite set A is hyperimmune if and only if no computable function f majorizes A. A function f majorizes an infinite set A if f majorizes its principal function $p_{A}$ (i.e. $f(x) \ge p_{A}(x)$ for all $x\in \omega $ ), where $p_{A}(n) = a_{n}$ for $A=\{a_0 < a_1 < a_2 < \cdots \}$ . It is known that $deg(Id)$ consists of all decidable computably enumerable equivalence relations (further - ceers) with infinitely many equivalence classes, and if $Id\le R\le R_{A}$ then there exists a c.e. set B such that $R=R_{B}$ , [2]. Some interesting recent properties of hyperimmunity and numberings one can find in [3].

For a given partial computable function $\varphi $ , let $P_{\varphi }$ be the ceer defined in the following way: $x P_{\varphi } y \Leftrightarrow (x=y \text { or } \varphi (x) \downarrow = \varphi (y) \downarrow )$ .

Let’s denote by $PC$ the class of all ceers of the form $P_{\varphi }$ . Let

A ceer R is universal if $S\le R$ for any ceer S. It is known that universal ceers do exist, [4].

[1] Yu.L. Ershov, Positive equivalences, Algebra and Logic , vol. 10 (1973), no. 6, pp. 378–394.

[2] U. Andrews and A. Sorbi, Joins and meets in the structure of ceers, Computability , vol. 8 (2019), no. 3-4, pp. 193–241.

[3] F. Rakymzhankyzy, N.A. Bazhenov, A.A. Issakhov and B.S. Kalmurzayev, Minimal generalized computable numberings and families of positive preorders, Algebra and Logic , vol. 61 (2022), no. 3, pp. 188–206.

[4] U. Andrews, S. Lempp, J.S. Miller, K.M. Ng, L. San Mauro and A. Sorbi, Universal computably enumerable equivalence relations, The Journal of Symbolic Logic , vol. 79 (2014), no. 1, pp. 60–88.

▸DEBORAH KANT, The hidden use of new axioms (Work title: Predicting axioms).

Department of Mathematics, University of Hamburg, Bundesstrasse 55, 20146 Hamburg, Germany.

E-mail: deborah.kant@uni-hamburg.de.

Nowadays, philosophers do not consider mathematical axioms necessarily as self-evident statements. If not self-evident, what are the roles of mathematical axioms in mathematical practice? General ideas by Easwaran [1], Maddy ([3] and [4]), and Schlimm [2] require complementation by analyses of specific uses of axioms in mathematical practice that go beyond the question of axiom adoption. In this talk, I elaborate on the hidden use of large cardinal axioms in set-theoretic practice. The hidden use of an axiom A consists in first proving some statement S in $\text {ZFC}+A$ and, second, eliminating A in the proof to demonstrate that S is actually ZFC-provable. In this sense, the use of A in the first proof is hidden in the final proof.

This case study is partially based on information gathered in an interview study with set-theoretic practitioners and augmented by two examples from set-theoretic research: Borel determinacy and Cichoń’s maximum. The philosophical appeal of the hidden use consists in its twofold significance. For one, it is a heuristic use of axioms in the discovery process of mathematical proofs, useful for all set-theoretic practitioners. Secondly, referring to Gödel’s ideas on extrinsic justification [5], I argue that each instance of a successful hidden use provides a verifiable consequence of some axiom, and in this sense, an extrinsic reason in favour of this axiom.

[1] Kenny Easwaran, The Role of Axioms in Mathematics, Erkenntnis , vol. 68 (2008), no. 3, pp. 381–391.

[2] Dirk Schlimm, Axioms in Mathematical Practice, Philosophia Mathematica , vol. 21 (2013), no. 1, pp. 37–92.

[3] Penelope Maddy, Believing the Axioms. I, The Journal of Symbolic Logic , vol. 53 (1988), no. 2, pp. 481–511.

[4] , Believing the Axioms. II, The Journal of Symbolic Logic , vol. 53 (1988), no. 3, pp. 736–764.

[5] Kurt Gödel, What is Cantor’s Continuum Problem, The American Mathematical Monthly , vol. 54 (1947), no. 9, pp. 515–525.

▸EITETSU KEN, On $\Sigma ^{B}_{0}$ -generalizations of counting principles over $V^{0}$ .

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.

URL: https://sites.google.com/g.ecc.u-tokyo.ac.jp/eitetsu-kens-homepage.

Ajtai’s discovery ([1]) of $V^{0}\not \vdash ontoPHP^{n+1}_{n}$ , where $ontoPHP^{n+1}_{n}$ is a $\Sigma ^{B}_{0}$ formalization of the statement “there does not exist a bijection between $(n+1)$ pigeons and n holes,” was a significant breakthrough in proof complexity, and there have been many interesting generalizations and variations of this result.

In this talk, we first focus on the following well-known result ([2]): for any $p\geq 2$ ,

where $Count^{p}_{k}$ denotes a $\Sigma ^{B}_{0}$ formalization of the modular counting principle mod p and $injPHP^{n+1}_{n}$ denotes that of the pigeonhole principle for injections.

We try to make this result uniform for p. We give three types of (first-order and propositional) formulae which at first glance seem to be generalized versions of counting principles, and compare their strengths over $V^0$ . In particular, we see two of them, $UCP^{l,d}_{n}$ and $GCP$ , actually serve as uniform versions of $Count^{p}_{n}$ ( $p \geq 2$ ).

Then we conjecture that $V^{0}+UCP^{l,d}_{k} \not \vdash injPHP^{n+1}_{n}$ and give a sufficient condition to prove it.

[1] Ajtai, M., The complexity of the Pigeonhole Principle, Combinatorica , vol. 14 (1994), pp. 417–433.

[2] Beame, P. and Riis, S., More on the relative strength of counting principles, Proof Complexity and Feasible Arithmetics (P. Beame, & S. Buss), American Mathematical Society, Providence, RI, 1998, pp. 13–35.

▸BEIBUT KULPESHOV, On algebras of binary formulas for weakly circularly minimal theories with a trivial definable closure.

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

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

Algebras of binary formulas are a tool for describing relationships between elements of the sets of realizations of 1-types at binary level with respect to superpositions of binary definable sets. We consider algebras of binary isolating formulas originally studied in [1, 2], where under a binary isolating formula we understand a formula of the form $\varphi (x,y)$ , without parameters, such that for some parameter a the formula $\varphi (a,y)$ isolates some complete type from $S_1(\{a\})$ .

The notion of weak circular minimality was originally studied in [3]. A weakly circularly minimal structure is a circularly ordered structure $M=\langle M, K_3,\ldots \rangle $ such that any definable (with parameters) subset of M is a union of finitely many convex sets in M. In [4] $\aleph _0$ -categorical 1-transitive non-primitive weakly circularly minimal structures of convexity rank 1 with a trivial definable closure have been described up to binarity.

Here we discuss algebras of binary isolating formulas for these structures and give the following criterion for commutability of such algebras:

This research has been funded by Science Committee of Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. BR20281002).

[1] S.V. Sudoplatov, Classification of countable models of complete theories , Novosibirsk, Edition of NSTU, 2018.

[2] I.V. Shulepov and S.V. Sudoplatov, Algebras of distributions for isolating formulas of a complete theory, Siberian Electronic Mathematical Reports , Vol. 11 (2014), pp. 362–389.

[3] B.Sh. Kulpeshov and H.D. Macpherson, Minimality conditions on circularly ordered structures, Mathematical Logic Quarterly , Vol. 51, No. 4 (2005), pp. 377–399.

[4] B.Sh. Kulpeshov, On $\aleph _0$ -categorical weakly circularly minimal structures, Mathematical Logic Quarterly , Vol. 52, No. 6 (2006), pp. 555–574.

▸BEIBUT KULPESHOV AND SERGEY SUDOPLATOV, Almost quite orthogonality of 1-types in weakly 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 State 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.

Here we study a new variant of orthogonality of non-algebraic 1-types in weakly o-minimal theories: almost quite orthogonality.

We need the notion of a $(p,q)$ -splitting formula introduced in [2]. Let $A\subseteq M$ , $p, q \in S_1(A)$ be non-algebraic, $p\not \perp ^w q$ . We say that an $L_A$ -formula $\phi (x,y)$ is a $(p, q)$ -splitting formula if there exists $a\in p(M)$ such that $\phi (a,M)\cap q(M)\ne \emptyset $ , $\neg \phi (a,M)\cap q(M)\ne \emptyset $ , $\phi (a,M)\cap q(M)$ is convex and $\inf [\phi (a,M)\cap q(M)]=\inf q(M)$ .

Let T be a weakly o-minimal theory, $M\models T$ , $A\subseteq M$ , $p,q\in S_1(A)$ be non-algebraic. We say that p is not almost quite orthogonal to q if there exist a $(p,q)$ -splitting formula $\phi (x,y)$ and an A-definable equivalence relation $E_q(x,y)$ partitioning $q(M)$ into infinitely many convex classes so that for any $a\in p(M)$ there is $b\in q(M)$ such that $\sup \phi (a,M)=\sup E_q(b,M)$ . We say that T is almost quite o-minimal if the notions of weak and almost quite orthogonality of 1-types coincide.

This research has been funded by Science Committee of Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP19674850), and by Russian Scientific Foundation (Project No. 22-21-00044).

[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, No. 12 (2000), pp. 5435–5483.

[2] B.Sh. Kulpeshov, Criterion for binarity of $\aleph _0$ -categorical weakly o-minimal theories, Annals of Pure and Applied Logic , Vol. 45 (2007), pp. 354–367.

▸DOROTA LESZCZYŃSKA-JASION, A sequent system for a Boolean non-Fregean logic WB.

Department of Logic and Cognitive Science, Adam Mickiewicz University, Poznań, ul. Szamarzewskiego 89 A, Poland.

E-mail: Dorota.Leszczynska@amu.edu.pl.

Logic WB is a Boolean non-Fregean logic introduced to the literature by Roman Suszko [2]. The idea of non-Fregean logics (NFL) stems from Wittgenstein’s Tractatus, more specifically—the semantics and ontology as suggested by this work [1,3]. Formally, an NFL is built upon classical propositional logic CPL by adding the identity connective $\equiv $ to the language. Intuitively, ‘ $\alpha \equiv \beta $ ’ is used to express the fact that $\alpha $ and $\beta $ describe the same situation. The basic NFL proposed by Suszko, sentential calculus with identity (SCI), has a drawback (at least, one may view it as such): hardly anything can be stated about identity of situations in this logic—all SCI-valid equations are of the form ‘ $\alpha \equiv \alpha $ ’.

WB is one of NFLs strengthening SCI by allowing $\equiv $ to have some Boolean properties; for example, ‘ $(\alpha \land \beta ) \equiv (\beta \land \alpha )$ ’ is a validity in WB. Still, $\equiv $ in WB is not truth-functional equivalence.

A little is known about proof-theoretical properties of this logic—the original account is axiomatic. In the talk I present a sequent system for WB (based on idea by Agata Tomczyk) together with a proof procedure by means of which positive decidability of WB is shown. I also introduce a new semantics of truth valuations for WB (as far, only algebraic semantics was available).

[1] Roman Suszko, Ontologia w Traktacie L. Wittgensteina (Ontology in the Tractatus of L. Wittgenstein), Studia Filozoficzne , vol. 1 (1968), pp. 97–121.

[2] , Identity connective and modality, Studia Logica , vol. 27 (1971), pp. 7–39.

[3] , Abolition of the Fregean axiom, Logic Colloquium (Boston 1972–1973), (R. Parikh, editor), vol. 453 of Lecture Notes in Mathematics, Springer Verlag, 1975, pp. 169–239.

▸LAURENŢIU LEUŞTEAN AND PEDRO PINTO, Proof mining and asymptotic regularity.

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.

Department of Mathematics, Technische Universität Darmstadt.

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

This talk presents a recent application of proof mining to the asymptotic behavior of the alternating Hapern-Mann iteration for nonexpansive mappings [2]. Proof mining is a subfield of applied proof theory concerned with the extraction of new quantitative and qualitative information from mathematical proofs, with the help of proof-theoretic tools. This paradigm of research, developed by Ulrich Kohlenbach and collaborators, is inspired by Kreisel’s program on unwinding of proofs from the 1950s. We present extensions to UCW-hyperbolic spaces of the quantitative asymptotic regularity results for the alternating Halpern-Mann iteration obtained by Dinis and Pinto for CAT(0) spaces [1]. These results are new even for uniformly convex normed spaces. Furthermore, for a particular choice of the parameter sequences, we compute linear rates of asymptotic regularity in W-hyperbolic spaces and quadratic rates of T- and U-asymptotic regularity in CAT(0) spaces.

[1] B. Dinis and P. Pinto, Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces, SIAM Journal on Optimization , vol. 33 (2023), no. 2, pp. 785–815.

[2] L. Leuştean and P. Pinto, Rates of asymptotic regularity for the alternating Halpern-Mann iteration, Optimization Letters , (2023).

▸STEPHEN MACKERETH AND JEREMY AVIGAD, Two-sorted Frege Arithmetic is not conservative.

Department of Philosophy, University of Pittsburgh, 4200 Fifth Ave, Pittsburgh, PA 15221, USA.

E-mail: sgmackereth@gmail.com.

Department of Philosophy, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA 15213, USA.

E-mail: avigad@cmu.edu.

URL: https://www.andrew.cmu.edu/user/avigad/.

Neo-Fregean logicists Hale and Wright [1] have claimed that Hume’s Principle (HP) may be taken as an implicit, stipulative definition of cardinal number, true simply by fiat. A longstanding problem for neo-Fregean logicism is that HP is not deductively conservative over the theory to which it is added, namely, pure axiomatic second-order logic. This seems to preclude HP from being true by fiat. In this talk, we study Richard Kimberly Heck’s [2] theory of Two-sorted Frege Arithmetic (2FA), a variation on HP which has been thought to be deductively conservative over second-order logic. We show that it isn’t [3]. In fact, 2FA is not conservative over n-th order logic, for all $n \geq 2$ . It follows that in the usual one-sorted setting, HP is not deductively Field-conservative (in the sense of Weir [4]) over second- or higher-order logic.

[1] Bob Hale and Crispin Wright, The Reason’s Proper Study: Essays towards a Neo-Fregean Philosophy of Mathematics , Clarendon Press, Oxford, 2001.

[2] Richard Kimberly Heck, The Julius Caesar objection, Language, Thought, and Logic: Essays in Honour of Michael Dummett (Richard Kimberly Heck, editor), Oxford University Press, Oxford, 1997, pp. 273–308.

[3] Stephen Mackereth and Jeremy Avigad, Two-sorted Frege Arithmetic is not conservative, The Review of Symbolic Logic , published online, 18 April 2022.

[4] Alan Weir, Neo-Fregeanism: An embarrassment of riches, Notre Dame Journal of Formal Logic , vol. 44 (2003), no. 1, pp. 13–48.

▸ALBERTO MARCONE, Jumping in the Weihrauch degrees.

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

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

URL: http://www.dimi.uniud.it/marcone.

The jump is a fundamental operation in the Turing degrees and jump operators have been defined also in other degree structures, such as the enumeration degrees.

Given a quasi-order $(Q, {\leq })$ , an operator $J: Q \to Q$ can be considered a jump if it satisfies $p < J(p)$ and $J(p) \leq J(q)$ whenever $p \leq q$ (the latter condition ensures that J is degree-theoretic, i.e. can be lifted to the quotient partial order).

In the Weihrauch degrees a natural operator called “jump” was introduced a few years ago ([1]) and then widely used. However this operator fails to satisfy both abstract properties mentioned above (although it satisfies the second one with respect to strong Weihrauch reducibility). We propose a natural definition of a jump operator which satisfies both properties and we compute explicitly the jumps of many well-known Weihrauch degrees. This jump is connected with the (non degree-theoretic) operation of total continuation.

If time allows, we will also mention results about the existence of jumps in arbitrary quasi-orders.

This is joint work with Uri Andrews, Steffen Lempp, Joe Miller and Manlio Valenti.

[1] Vasco Brattka, Guido Gherardi and Alberto Marcone, The Bolzano-Weierstrass theorem is the jump of weak Kőnig’s lemma, Annals of Pure and Applied Logic , vol. 163 (2012), no. 6, pp. 623–655.

▸GUILLAUME MASSAS, Duality for Fundamental Logic.

Department of Mathematics, University of California Berkeley.

E-mail: gmassas@berkeley.edu.

Holliday [2] recently introduced a non-classical logic called Fundamental Logic, which is meant to capture only those properties of the connectives $\wedge $ , $\vee $ and $\neg $ that hold in virtue of their introduction and elimination rules in Fitch’s natural deduction system for propositional logic. Holliday provides a semantics for fundamental logic in terms of compatibility frames (sets endowed with a relation of compatibility between its points) which generalizes both Goldblatt’s semantics for orthologic and Kripke’s semantics for intuitionistic logic. In particular, any relation R on a set X determines a closure operator on $\mathcal {P}(X)$ , and Holliday shows that any lattice can be represented as a sublattice of the fixpoints of such a closure operator for some compatibility frame $(X,R)$ .

In this talk, I will show how standard tools from duality theory allow one to lift Holliday’s representation theorem to a full duality between the category of lattices and a category of topologized compatibility frames. The key idea is to embed any lattice into the fixpoints of a Galois connection on a distributive lattice in order to then use a version of the duality between modal distributive lattices and coalgebras of the Vietoris functor on the category of Priestley spaces [1, 3]. Time permitting, I will also show how this duality yields natural semantics for any extension of fundamental logic with connectives that are monotone (i.e., order-preserving or order-reversing) in each coordinate.

[1] S. Celani and R. Jansana, Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic, Logic Journal of the IGPL , vol. 7 (1999), no. 6, pp. 683–715.

[2] W.H. Holliday, A fundament non-classical logic, arXiv:2207.06993, 2022.

[3] A. Palmigiano, A coalgebra view on positive modal logic, Theoretical Computer Science , vol. 327 (2004), pp. 175–195.

▸BRETT MCLEAN, Complete representation by partial functions for signatures containing antidomain restriction.

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

E-mail: brett.mclean@ugent.be.

In [2], Jackson and Stokes investigate the axiomatisability of classes of algebras that are representable as (i.e. isomorphic to) an algebra of partial functions. Using a uniform method of representation, they give, for around 30 different signatures containing the domain restriction operation, either a finite equational or finite quasi-equational axiomatisation of the class of representable algebras. Only a handful of these classes had previously been axiomatised.

We show that a similar uniform method of representation can be used to characterise many of the corresponding subclasses of completely representable algebras. A complete representation is one that turns any existing infima/suprema into intersections/unions. Specifically, we do this for signatures containing the operation called minus in [2] and which we call antidomain restriction; thus for about half of the signatures treated in [2]. Together with the results of [2], this gives us finite first-order axiomatisations of 14 of these classes of completely representable algebras. Only a couple of complete representation classes had previously been axiomatised (for representation as partial functions) [1,3].

[1] Célia Borlido and Brett McLean, Difference–restriction algebras of partial functions: axiomatisations and representations, Algebra Universalis , vol. 83 (2022), no. 3, 27 pp.

[2] Marcel Jackson and Tim Stokes, Restriction in Program Algebra, Logic Journal of the IGPL , (2022), 35 pp.

[3] Brett McLean, Complete representation by partial functions for composition, intersection and antidomain, Journal of Logic and Computation , vol. 27 (2017), no. 4, pp. 1143–1156.

▸RUSSELL MILLER, Skolem functions and definable subsets of the absolute Galois group of  $\mathbb Q$ .

Mathematics Dept., Queens College – CUNY, 65-30 Kissena Blvd., Queens, NY 11355, USA.

E-mail: russell.miller@qc.cuny.edu.

Fix a computable presentation $\overline {\mathbb Q}$ of the algebraic closure of the field $\mathbb Q$ of rational numbers. With such a presentation, the automorphisms of $\overline {\mathbb Q}$ are naturally given as paths through a strongly computable finite-branching tree. The operations of composition and inversion on these automorphisms (i.e., on these paths) are both type-2 computable. Thus we have an effective way of considering $\text {Aut}(\overline {\mathbb Q})$ , the absolute Galois group of $\mathbb Q$ .

In this context, one can discuss the computability of Skolem functions for $\text {Aut}(\overline {\mathbb Q})$ . We show that for positive formulas (not using the negation connective) with parameters, Skolem functions are close to computable: one can compute an approximation to the jump of a witness to an existential formula. (That is, these Skolem functions are low, in the sense of Brattka, de Brecht, and Pauly.) The same holds for Skolem functions for any $\Pi _2$ formula, positive or not, and for certain larger classes of formulas as well. We also present related results describing the subsets of $(\text {Aut}(\overline {\mathbb Q}))^n$ definable by such formulas.

▸OWEN MILNER, Formalizing the Whitehead tower in cubical agda.

Department of Philosophy, Carnegie Mellon University, 5000 Forbes Avenue, Pittsburgh, PA, USA.

E-mail: omilner@andrew.cmu.edu.

This talk will present details of a formalization, in cubical agda, of the key properties of the Whitehead tower. This construction has been an important tool for computing the algebraic invariants of spaces since the work of Cartan and Serre [1] and Whitehead [2] in the early 1950s. The recent development of homotopy type theory (as in [3], and [4]) has made it possible for significant parts of classical algebraic topology to be developed synthetically and constructively, and in a manner suitable for computer formalization. Work such as that being presented here connects a canonical part of pure mathematics with the burgeoning interest in formalization and verification of mathematics by computers. The formalization includes not only the definition of the Whitehead tower, but also a proof that its objects satisfy a universal property, the computation of their homotopy groups, and the identification of the fibers of the structure maps of the tower as particular Eilenberg-MacLane spaces. Parts of the formalization are available online at https://github.com/CMU-HoTT/serre-finiteness.

[1] Henri Cartan and Jean-Pierre Serre, Espaces Fibrés et Groupes d’Homotopie, I, Comptes Redus Hebdomadaires de Séances de l’Académie des Sciences , vol. 234 (1952), pp. 288–290.

[2] George W. Whitehead, Fiber Spaces and the Eilenberg Homology Groups, Proceedings of the National Academy of Sciences of the United States of America 38(5) , vol. 38 (1952), no. 5, pp. 426-430.

[3] The Univalent Foundations Program, Homotopy Type Theory: The Univalent Foundations of Mathematics , https://homotopytypetheory.org/book/, The Institute for Advanced Study, 2013.

[4] Cyril Cohen, Thierry Coquand, Simon Huber and Anders Mörtberg, Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom, Post-Proceedings of the 21st International Conference on Types for Proofs and Programs (TYPES 2015) (Tallinn, Estonia), (Tarmo Uustalu, editor), Dagstuhl Publishing, 2018, pp. 129–162.

▸JOACHIM MUELLER-THEYS, A Mathematical Model of the Atom.

Independent scholar; 69 226 Heidelberg, Germany.

E-mail: mueller-theys@gmx.de.

According to the idea of Wilfried Buchholz, we model the fundamental concept of atomic physics and chemistry naturally by triples

whereby $ P \neq \emptyset $ , $ N $ , $ E $ be finite sets of protons, neutrons, electrons respectively. Correspondingly, 2-tuples $ ( P , N ) $ model nuclei.

In the next step, functions assign the numbers of protons, neutrons, electrons:

The definitions for (atomic) ions now arise immediately—not requiring higher conceptuality. For example, $ A $ is an anion if $ \varepsilon ( A )> \pi ( A ) $ .

The proton number function induces the equi-valence

(cf. “Equivalence”, The Bulletin of Symbolic Logic 28 (2022), pp. 564–5).

Now the equi-valence classes

constituting a partition, model the (chemical) elements. Each element $ A / \pi $ is characterized by the natural number $ \pi ( A ) \geq 1 $ , corresponding to the order number. Afterwards, element names and symbols may be assigned, like $ 1 \ \mapsto $ hydrogen, H.

Additionally, the equi-valence $ \simeq _{\nu } $ with respect to the neutron number function partitions each element into its isotopes, and underlying systems of atoms $ \mathcal A $ may be further specified.

Acknowledgment. Ongoing thanks to ‘Peana Pesen’ and H. & A. Haltenhoff. The author wants to mention following chemists: O. Mueller, M. R. Bloch, John T. Wasson, Walter Littke, Wolfgang Maier-Borst, Stefan Reimann-Andersen, Bernhard Höferth, Claudia Friesen, Jerry LR Chandler.

▸LEONARDO PACHECO, The $\mu $ -calculus’ collapse on variations of $\mathsf {S5}$ .

Mathematical Institute, Tohoku University, Sendai, Japan.

E-mail: leonardovpacheco@gmail.com.

URL: leonardopacheco.xyz.

The $\mu $ -calculus is obtained by adding to modal logic the least and greatest fixed-point operators $\mu $ and $\nu $ . The alternation depth of a formula measures the entanglement of its least and greatest fixed-point operators. Bradfield [2] showed that, for all $n\in \mathbb {N}$ , there is a formula $W_n$ such that $W_n$ has alternation depth n and, over all Kripke frames, $W_n$ is not equivalent to any formula with alternation depth smaller than n.

The same may not happen over restricted classes of frames: Alberucci and Facchini [1] showed that, over frames of $\mathsf {S5}$ , every $\mu $ -formula is equivalent to a formula without fixed point operators. In this case, we say the $\mu $ -calculus collapses to modal logic over frames of  $\mathsf {S5}$ .

We show how Alberucci and Facchini’s proof generalize to the $\mu $ -calculus’s collapse over frames of intuitionistic $\mathsf {S5}$ . This generalization can also be done for some non-normal logics and for graded modal logics. We also show that, on the other hand, the $\mu $ -calculus does not collapse over the bimodal logic $\mathsf {S5}_2$ .

[1] Luca Alberucci Alessandro Facchini, The modal $\mu $ -calculus hierarchy over restricted classes of transition systems, The Journal of Symbolic Logic , vol. 74 (2009), no. 4, pp. 1367–1400.

[2] Julian C. Bradfield, The modal mu-calculus alternation hierarchy is strict, Theoretical Computer Science , vol. 195 (1998), no. 2, pp. 133–153.

▸LUIZ CARLOS PEREIRA, ELAINE PIMENTEL AND VALERIA DE PAIVA, Translations and Prawitz ecumenical system.

Universidade do Estado do Rio de Janeiro, Rio de Janeiro, Brazil.

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

Department of Computer Science, University College London, London, UK.

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

Topos Institute, Berkeley, USA.

E-mail: valeria@topos.institute.

Ecumenical systems are formal codifications where two or more logics can co-exist in peace, which means that these logics accept and reject the same formulae, the same rules and the same basic principles. Dag Prawitz proposed a natural deduction ecumenical system [2], where classical logic and intuitionistic logic are codified in the same system (see also [1]). In this system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz main idea is that these different meanings are given by a semantic framework that can be accepted by both parties. The rules for the intuitionistic operators ( $\to _{i}, \vee _{i}, \exists _{i}$ ) and for the shared operators ( $\wedge , \neg , \bot , \forall $ ) are the usual Gentzen-Prawitz natural deduction introduction and elimination rules. The rules for the classical propositional operators are as follows:

This short note has two main objectives. The first is to show, in the propositional case, that there are interesting relations between the Gödel-Gentzen translation and the ecumenical perspective, but that the later cannot be reduced to the former. The second main objective is to investigate the possibility of ecumenical systems with two independent negations, one classical and one intuitionistic.

[1] Pimentel, E., Pereira, Luiz C. and de Paiva, Valeria, An ecumenical notion of entailment (2020), Synthese , vol. 198, (2019), pp. 5391–5413.

[2] Prawitz, D., Classical versus intuitionistic logic, Why is this a Proof?, Festschrift for Luiz Carlos Pereira (Hermann Haeusler, Wagner Sanz, and Bruno Lopes editors), College Books, 2015, pp. 15–32.

▸PEDRO PINTO, Proof mining and the convex feasibility problem.

Department of Mathematics, Technische Universität Darmstadt, Schlossgartenstr. 7, 64289 Darmstadt, Germany.

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

URL: https://www2.mathematik.tu-darmstadt.de/~pinto/.

In this talk, we will discuss a recent proof mining study [5,6] regarding the strong convergence of Dykstra’s algorithm. Proof mining [4] employs proof-theoretical techniques to analyse prima facie noneffective mathematical proofs with the goal of extracting additional information. Such new information is usually in the form of effective and highly uniform rates or bounds. In the last twenty-five years, this area of Proof Theory has been greatly developed by Ulrich Kohlenbach and his collaborators, and proof mining techniques have been particularly successful in applications to nonlinear analysis and adjacent areas. In convex optimization, many practical problems can be framed in the setting of the convex feasibility problem [1], i.e. finding the projection onto the intersection of finitely many convex sets under the assumption that the projection onto the individual sets is easy to compute. We will discuss new results regarding the asymptotic behavior of the well-known Dykstra’s algorithm [2,3], obtained via proof mining techniques.

[1] Heinz H. Bauschke and Jonathan M. Borwein, On projection algorithms for solving convex feasibility problems, SIAM Review , vol. 38 (1996), no. 3, pp. 367–426.

[2] James P. Boyle and Richard L. Dykstra, A Method for Finding Projections onto the Intersection of Convex Sets in Hilbert Spaces, Advances in Order Restricted Statistical Inference , Lecture Notes in Statistics, vol. 37, (Richard L. Dykstra, Tim Robertson and Farroll T. Wright, editors), Springer, New York, 1986, pp. 28–47.

[3] Richard L. Dykstra, An algorithm for restricted least squares regression, Journal of the American Statistical Association , vol. 78 (1983), no. 384, pp. 837–842.

[4] Ulrich Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics , Springer Monographs in Mathematics, Springer, 2008.

[5] Pedro Pinto, On the finitary content of Dykstra’s algorithm, Submitted , arXiv:2306.09791 (2023).

[6] , Proof mining and the convex feasibility problem: The curious case of Dykstra’s algorithm in preparation.

▸JONI PULJUJÄRVI AND DAVIDE EMILIO QUADRELLARO, Some model-theoretic results in team semantics.

Department of Mathematics and Statistics, University of Helsinki, Finland.

E-mail: joni.puljujarvi@helsinki.fi.

E-mail: davide.quadrellaro@helsinki.fi.

In this talk, we continue the work started in [2] and we try to develop a suitable model-theoretic framework for logics over team semantics. In fact, since logics in team semantics admit a compactness theorem [2], it is natural to consider how far the standard tools and results from classical model theory can be pushed in this context.

We introduce a suitable notion of maps between models that preserve formulas of independent logic and we describe the resulting category of models and morphisms. In particular, we show that a suitable version of the amalgamation property holds in this context and we introduce a notion of Galois types for logics in team semantics. Finally, we also describe in better detail to what extent this category fits the framework of Abstract Elementary Categories of Kamsma and Kirby [1].

[1] Mark Kamsma, The Kim-Pillay Theorem for Abstract Elementary Categories, The Journal of Symbolic Logic , vol. 85 (2020), no. 4, pp. 1717–1741.

[2] Joni Puljujärvi and Davide Emilio Quadrellaro, Compactness in Team Semantics, arXiv:2212.03677.

▸MARCOS M. RECIO, JOSÉ MIGUEL BLANCO AND SANDRA M. LÓPEZ, Exploring the building blocks of 2 set-up Routley-Meyer semantics.

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

E-mail: marcosmanuelrecioperez@usal.es.

Universidad Politécnica de Madrid, Av. Complutense 30, 28040, Madrid, Spain.

E-mail: josemiguel.blanco@upm.es.

URL: https://sites.google.com/view/jmblancos.

Universidad de Valladolid, Pl. Campus Universitario, 47011, Valladolid, Spain.

E-mail: sandralv@uva.es.

While 2 set-up Routley-Meyer semantics has been historically considered as less interesting than regular Routley-Meyer semantics, this trend seems to break in recent years [1]. In particular, its accessibility relation has been studied with respect to the semantic postulates of its regular counterpart in certain many-valued logics [2]. Nevertheless, there is another relationship to be explored within 2 set-up Routley-Meyer semantics: the one of the accessibility relation with respect to Hilbert-style theorems. For each of the eight possible accessibility relations supported by 2 set-up Routley-Meyer semantics, there is an intrinsic relationship with, at least, one theorem that needs to be part of the logical system endowed with this kind of semantics. Thus, the main aim of this talk is to present an approach to how the accessibility relations relate to Hilbert-style theorems and how each other supports themselves during the process of soundness and completeness proofs.

Acknowledgements. This work is supported by the Spanish Ministry of Science and Innovation (MCIN/AEI/ 10.13039/501100011033) under Grant PID2020-116502GB-I00. This work has been supported by the Madrid Government (Comunidad de Madrid-Spain) under the Multiannual Agreement with Universidad Politécnica de Madrid in the line Support for R&D projects for Beatriz Galindo researchers, in the context of the V PRICIT (Regional Programme of Research and Technological Innovation).

[1] G. Robles, S.M. López, J.M. Blanco, M.M. Recio and J.R. Paradela, A 2-set-up Routley-Meyer semantics for the 4-valued relevant logic E4, Bulletin of the Section of Logic , vol. 45 (2016), no. 2, pp. 93–109.

[2] J.M. Blanco, S.M. López and M.M. Recio, On how the 2 Set-up Routley-Meyer semantics are a case of the Reduced General Routley-Meyer semantics in the context of some 4-valued logics, Journal of Applied Logics , vol. 10 (2023), no. 1, pp. 1–18.

▸JUAN M. SANTIAGO SUÁREZ AND MATTEO VIALE, Boolean valued semantics for infinitary logics.

Université Paris Cité, Place Aurélie Nemours 75013 Paris, France.

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

Department of Mathematics Giuseppe Peano, University of Turin, Palazzo Campana Via Carlo Alberto 10 10123 Turin, Italy.

E-mail: matteo.viale@unito.it.

It is well known that the completeness theorem for $\mathrm {L}_{\omega _1\omega }$ fails with respect to Tarski semantics. Mansfield [1] showed that it holds for $\mathrm {L}_{\infty \infty }$ if one replaces Tarski semantics with boolean valued semantics. We use forcing to improve his result in order to obtain a stronger form of boolean completeness (but only for $\mathrm {L}_{\infty \omega }$ ). Leveraging on our completeness result, we establish the Craig interpolation property and a strong version of the omitting types theorem for $\mathrm {L}_{\infty \omega }$ with respect to boolean valued semantics. We also show that a weak version of these results holds for $\mathrm {L}_{\infty \infty }$ (if one leverages instead on Mansfield’s completeness theorem). Furthermore we bring to light (or in some cases just revive) several connections between the infinitary logic $\mathrm {L}_{\infty \omega }$ and the forcing method in set theory.

[1] Richard Mansfield, The Completeness Theorem for Infinitary Logic, The Journal of Symbolic Logic , vol. 37 (1972), no. 1, pp. 31-34.

▸GIORGIO SBARDOLINI AND SEBASTIAN G.W. SPEITEL, Logic and evolution.

Munich Center for Mathematical Philosophy, Ludwig Maximilian University of Munich.

E-mail: giorgio.sbardolini@lrz.uni-muenchen.de.

Institute of Philosophy, University of Bonn.

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

Can logic change over time? On the one hand, the logical concepts, as expressed by function words (every, some, and, if), are subject to the evolutionary forces shaping natural language vocabulary. Since natural language undergoes constant and continuous change, so do the logical concepts expressed through it. On the other hand, the logical operators are unchanging: as part of the abstract mathematical realm there can be no more change in logic than there can be in mathematics.

Our goal is to make some headway on a possible reply to this dilemma. We begin by characterizing two senses of the word ‘logic’, distinguishing, following Harman [2], between a theory of deduction and a theory of reasoning. This distinction is used to defuse Quine’s [6] famous objection to the possibility of change in logic: according to Quine, there can only be wholesale replacement of logical theory but no incremental development (‘change of logic, change of subject’). We then present two arguments in favor of the possibility of change in logic, one from a naturalistic perspective on scientific explanation [3] and the other from considerations of open texture [7, 4].

Having argued for change in logic, we owe an account of logical meaning that, on the one hand, shows how logical concepts can change while, on the other, explains their relative robustness when it comes to conceptual change: the logical vocabulary can change, but not as fast as nouns and predicates do. To this end we first discuss a proposal based on Došen’s [1] idea that the logical constants mark structural features of deductive reasoning. We then reject the problematic underlying assumption of a stable core meaning, to sketch an account that makes room for a more flexible treatment of the identity and individuation of logical concepts, elaborating on an old theme from Putnam [5].

[1] K. Došen, Logical Constants as Punctuation Marks, Notre Dame Journal of Formal Logic , vol. 30 (1989), pp. 362–381.

[2] G. Harman, Logic and Reasoning, Synthese , vol. 60 (1984), pp. 107–127.

[3] P. Maddy, Second Philosophy: A Naturalistic Method , Oxford University Press, 2007.

[4] D. Makovec and S. Shapiro, editors. Friedrich Waismann , Springer International Publishing, 2019.

[5] H. Putnam, Three-Valued Logic, Philosophical Studies , vol. 8 (1957), pp. 73–80.

[6] W.V.O. Quine, Philosophy of Logic , Harvard University Press, 1970.

[7] F. Waismann, Verifiability, Aristotelian Society Supplementary Volume , vol. XIX (1947), pp. 119–150.

▸IOANNIS SOULDATOS, The Hanf Number for the Joint Embedding Property.

Department of Mathematics, Aristotle University of Thessaloniki, Thessaloniki 54124, Greece.

E-mail: souldatos@math.auth.gr.

Define the Hanf number for the joint embedding property (JEP), or the amalgamation property (AP), for Abstract Elementary Classes (AEC) to be the least cardinal $\mu $ so that if K is an AEC with $LS($ K $)<\mu $ , and K satisfies JEP (AP) cofinally below $\mu $ , then K satisfies JEP (AP) in all cardinals $\ge \mu $ .

In [1], Baldwin and Boney proved that the first strongly compact cardinal is an upper bound for the Hanf number for JEP and AP. They raised the question if the strongly compact upper bound is optimal.

In this talk we will survey some recent developments in the area.

[1] John Baldwin and Will Boney, Hanf numbers and presentation theorems in aecs, Beyond First Order Model Theory , (Jose Iovino, editor), Chapman Hall, 2017, pp. 81–106.

[2] Will Boney and Ioannis Souldatos, A lower bound for the Hanf number for joint embedding, Fundamenta Mathematicae , vol. 258 (2022), no. 2, pp. 115–135.

▸BERNHARD STOINSKI, Extension of category theory using a PL0 calculus functor to form propositional morphisms in multi-agent systems.

Private Institute for General Dynamic Logic, Herforder Strasse 15, Cologne, Germany.

E-mail: bernhard.stoinski@pifdl.eu.

Abstract: The subject of this talk are morphisms between categories that are able to map truth values by means of a PL0-calculus functor $ Calc_{0} $ . This functor is used in the generation of AI multi-agent systems (MAS) [3]. In this case, the agents are equivalent to the categories [1]. A highly simplified example of an AI-MAS using PL0 calculus functors represents the practical aspect of this talk [2]. The special feature of the functor $ Calc_{0} : A \rightarrow B $ is that the morphism from agent $ A $ to agent $ B $ yields a truth value $ t_{A}:X \rightarrow [0,1] $ , taking A to be a fuzzy set. The function value $ m_{A} (a) $ for $ a \in X $ is itself again the membership value formed by the result of a calculus function of A. Hereby A itself becomes a fuzzy set. By this fact, a fuzzy space is formed by means of $ Calc_{0} $ , which, however, must not be confused with a type 2 fuzzy set. Through this construct and the self-similarity of the MAS, it is possible to represent complex natural processes with a high entropy [4] content.

[1] Mac Lane, S., Categories for the working Mathematician , Second Edition, Springer, New York, 1978.

[2] Rust, S.; Stoinski, B., Using Artificial Intelligence to assist Tree Risk Assessment, Arboriculture and Urban Forestry , vol. 48 (2022), no. 2, pp. 138–146.

[3] Stoinski, B., Dynamische Multi-Agent-Systeme Komplexe KI-Systeme: Wann ein kognitiver Ansatz wichtig ist, Industry-Of-Things , 2022.

[4] Szilard, L., Über die Entropieverminderung in einem thermodynamischen System bei Eingriffen intelligenter Wesen, Zeitschrift für Physik , vol. 53 (1929), pp.840–856.

▸DAVIDE SUTTO, Potentialist set theory: New paths and open questions.

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

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

In the last ten years potentialist set theory has emerged as one of the most lively trends in the philosophy of set theory. Remarkably, a modal account of sets has been developed in two different ways, the first inspired by the work of Charles Parsons and the second dating back to Hilary Putnam and Geoffrey Hellman. The aim of the paper is to present these two approaches through two groups of questions, with the aim of outlining the state of the art while, at the same time, sketching the new paths and challenges soon-to-be-faced by a potentialist account of sets.

[1] N. Barton, Iterative Conception of Sets , Cambridge Elements: The Philosophy of Mathematics, Cambridge University Press, forthcoming.

[2] P. Benacerraf and H. Putnam, editors. Philosophy of Mathematics: Selected Readings , Second Edition, Cambridge University Press, 1983.

[3] S. Berry, A Logical Foundation for Potentialist Set Theory , Cambridge University Press, 2022.

[4] T. Button, Level Theory, Part 2: Axiomatizing the Bare Idea of a Potential Hierarchy, The Bulletin of Symbolic Logic , vol. 27 (2022), no. 4, pp. 461–484.

[5] Ø. Linnebo, Pluralities and Sets, Journal of Philosophy , vol. 107 (2010), no. 3, pp. 144–164.

[6] , The Potential Hierarchy of Sets, The Review of Symbolic Logic , vol. 6 (2013), no. 2, pp. 205–228.

[7] , Thin Objects: An Abstractionist Account , Oxford University Press, 2018.

[8] C. Parsons, Sets and Modality, Mathematics in Philosophy: Selected Essays (C. Parsons, editor), Cornell University Press, 1983, pp. 298–341.

[9] H. Putnam, Mathematics Without Foundations, Journal of Philosophy , vol. 64 (1967), no. 1, pp. 5–22.

[10] J. P. Studd, The Iterative Conception of Set: A (Bi-)Modal Axiomatisation, Journal of Philosophical Logic , vol. 42 (2013), no. 5, pp. 697–725.

[11] , Everything, More or Less: A Defence of Generality Relativism , Oxford University Press, 2019.

▸GIORGIO VENTURI AND PEDRO YAGO, How to be (semantically) insensitive.

Dipartimento di Civilità e Forme di Sapere, Università di Pisa, Via Palestro 15, Italy.

E-mail: gio.venturi@gmail.com.

Classe di Lettere e Filosofia, Scuola Normale Superiore, Piazza dei Cavalieri 6, Italy.

E-mail: pedro.tyago@outlook.com.

In this paper we study the semantic insensitivity of nonnormal modal languages, in the sense of insensitivity presented in [5] – that such a language is semantically insensitive to a frame property when the language cannot define it. Starting with relational frames, we present an heuristic inspired by modalities that are insensitive to reflexivity [3], seriality [2], and narcissism [4], which we then use to offer nonnormal modal languages which are insensitive to functionality, transitivity, symmetry, and second-reflexivity. In the last part of this paper, we cover neighborhood models, presenting the insensitivity of particular nonnormal modal operators in that semantics [1]. We then offer a general result regarding the insensitivity of a wide class of languages in neighborhood semantics, which explains the previously presented particular insensitivities.

[1] David Gilbert and Giorgio Venturi, Neighborhood semantics for logics of unknown truths and false beliefs, Australasian Journal of Logic , vol. 14 (2017), no. 1, pp. 246–267.

[2] Lloyd Humberstone, The logic of non-contingency, Notre Dame Journal of Formal Logic , vol. 36 (1995), no. 2, pp. 214–229.

[3] João Marcos, Logics of essence and accident, Bulletin of the Section of Logic , vol. 34 (2005), no. 1, pp. 43–56.

[4] Cristopher Steinsvold, Being wrong: logics for false belief, Notre Dame Journal of Formal Logic , vol. 52 (2011), no. 3, pp. 245–253.

[5] Giorgio Venturi and Pedro Yago, Tableaux for essence and contingency, Logic Journal of the IGPL , vol. 29 (2020), no. 5, pp. 719–738.

▸ANDREAS WEIERMANN, The phase transition for Harvey Friedman’s Bolzano Weierstrass principle.

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

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

Let f be a strictly positive function. Harvey Friedman’s Bolzano Weierstrass principle with respect to f is the following assertion ( $BW_f$ ). $(\forall K\geq 3)( \exists M) (\forall x_1,\ldots , x_M\in [0,1] )( \exists {k_1},\ldots , k_K) (k_1<\ldots <k_K\leq M \wedge (\forall l\leq K-2) (\lvert x_{k_{l+1}}-x_{k_{l+2}}\rvert <{f(k_{l})}))$ . Friedman has shown that $BW_f$ is true (by an application of the compactness of the Hilbert cube). Morever Friedman has shown that for $f(x)=1/x^{1+\varepsilon }$ where $\varepsilon>0$ the principle $BW_f$ is not provable in $I\Sigma _1$ . He also has shown that for $f(x)=\log (x)/x$ the assertion $BW_f$ is provable from $I\Sigma _1$ and asked for the strength of $BW_f$ for $f(x)=1/x$ and $f(x)=1/(x\log (x))$ .

In our talk we answer these two questions and we give rather sharp bounds on the phase transition window for those functions f for which $BW_f$ is provable or unprovable from $I\Sigma _1$ . We also discuss the Friedman principle for monotone increasing sequences.

Finally as a real analysis spin off we obtain explicit formulas for the derivative of the smooth version of the inverse function of the d-th branch of the Ackermann function for any natural number d.

▸A.R. YESHKEYEV, I.O. TUNGUSHBAYEVA AND G.YE. ZHUMABEKOVA, The central type of a semantic pair.

Department of Algebra, Mathematical Logic and Geometry named after T.G. Mustafin, Karaganda Buketov University, Universitetskaya street 28, Kazakhstan.

E-mail: aibat.kz@gmail.com.

Department of Algebra, Mathematical Logic and Geometry, named after T.G. Mustafin, Karaganda Buketov University, Universitetskaya street 28, Kazakhstan.

E-mail: intng@mail.ru.

Karaganda Industrial University, Respublika Avenue 30, Temirtau, Kazakhstan.

E-mail: galkatai@mail.ru.

We consider a hereditary [1] Jonsson theory T that is J- $\lambda $ -stable [2]. Let $C_T$ be a semantic model of T, and $N, M$ be existentially closed submodels of $C_T$ . A pair $(N,M)$ is called existentially closed pair, if M is an existentially closed submodel of N. An existentially closed pair $(C_T, M)$ is a semantic pair, if the following conditions hold: 1) M is $|T|^+_\exists $ -saturated (it means that it is $|T|^+$ -saturated restricted up to existential types); 2) for any tuple $\overline {a} \in C$ each its $\exists $ -type in sense of T over $M \cup \{\overline {a}\}$ is satisfiable in C. We define the theory $T'$ as follows: $T' = T \cup \{P, \subseteq \}$ , where $\{P, \subseteq \}$ is an infinite set of existential sentences with constants from the existentially closed submodel in the considered existentially closed pair. Let T be a Jonsson L-theory and $f(\overline {x}, \overline {y})$ be an $\exists $ -formula of L. If for any arbitrary large n there exists $\overline {a}_1, \ldots ,\overline {a_n}$ in some existentially closed model of T, and $\overline {a}_1, \ldots ,\overline {a_n}$ satisfies $\neg (\exists \overline {x}) \wedge \!\!\!\!\wedge _{k \leq n} f(\overline {x},\overline {a_k})$ , and for any $l \leq n\ \neg (\exists \overline {x}) \wedge \!\!\!\!\wedge _{k \leq n, k \neq l} f(\overline {x},\overline {a_k})$ , then $f(\overline {x}, \overline {y})$ is said to have e.f.c.p. (existentially finite covered property). In the framework of the study of Jonsson theories, which are generally incomplete, and in some expanded language with new unary predicate and constant symbols, we refine in such generalization the earlier result obtained on beautiful pairs for complete theories from [3] (Theorem 6).

[1] Aibat Yeshkeyev, Maira Kassymetova, Olga Ulbrikht, Independence and simplicity in Jonsson theories in abstract geometry, Siberian Electronic Mathematical Reports , vol. 18 (2021), no. 1, pp. 433–455.

[2] Aibat Yeshkeyev, On Jonsson stability and some of its generalizations, Journal of Mathematical Sciences , vol. 166 (2010), no. 5, pp. 646–654.

[3] Bruno Poizat, Paires de structures stables, The Journal of Symbolic Logic , vol. 48 (1983), no. 2, pp. 239–249.

▸AIBAT YESHKEYEV, OLGA ULBRIKHT AND AIGUL ISSAYEVA, Algebraically primeness and JSP-cosemanticness.

Faculty of Mathematics and Information Technologies, Karaganda Buketov University, Universitetskaya str., 28, Building 2, Kazakhstan.

E-mail: aibat.kz@gmail.com.

E-mail: ulbrikht@mail.ru.

E-mail: isaaiga13@gmail.com.

In [3] a criterion for the existence of a prime model for an arbitrary abelian group was found. The concept of an algebraically prime model generalizes the concept of a prime model.

As shown in [1], no general criterion of algebraic primeness is known for an arbitrary theory. As is known from work [5], the theory of Abelian groups is a perfect Jonsson theory. The main result of this thesis is a criterion for the existence of an algebraically prime model for the theory of Abelian groups. In the work [2] gives criteria for the existence of different types of prime models and also for algebraically prime models for a particular case of Abelian groups, namely, for torsion-free Abelian groups. The results of works [3] and [2] are realized in the framework of the complete theories of the corresponding Abelian groups. Jonsson theory is, generally speaking, not complete.

The following theorem generalizes the main results from [3] and [2] on the language of cosemanticness ( $\bowtie $ ), which generalized the notion of elementary equivalence.

All information about Jonsson theory and its details linked with a cosemanticness one can extract from [5].

This research is funded by the Science Committee of the Ministry of Science and Higher Education of the Republic of Kazakhstan (Grant No. AP09260237).

[1] Baldwin, J.T. and Kueker, D.W., Algebraically prime models, Annals of Mathematical Logic , vol. 20 (1981), no. 3, pp. 289–330.

[2] Deissler, R., Minimal and prime models of complete theories for torsionfree abelian groups, Algebra Universalis , (1979), no. 2, pp. 250–265.

[3] Molokov, A.V., Prime models of the theories of Abelian groups, Some problems and tasks of algebra and analysis , Novosibirsk, 1985, pp. 113–119.

[4] Robinson, A., Introduction to Model Theory and to the Metamathematics of Algebra , North-Holland, 1963.

[5] Yeshkeyev A.R. and Ulbrikht O.I., $JSp$ -cosemanticness and JSB property of Abelian groups, Siberian Electronic Mathematical Reports , vol. 13 (2016), pp. 861–874.

Abstract of talk presented by title

▸ALEXEJ PYNKO, Structural completeness versus completions of finitely-valued logics.

V.M. Glushkov Institute of Cybernetics, Glushkov prosp. 40, Kiev, 03680, Ukraine.

E-mail: pynko@i.ua.

Given any sentential language L with $\langle $ out $\rangle $ constants {and any $n\in (\omega \setminus ((1|0)\langle \cup 1\rangle ))$ } (with treating integers $\geqslant 0$ as sets $\wr $ ordinals of lesser ones and denoting their set $\wr $ ordinal by $\omega $ ) $\|$ “and any class $\mathsf {K}$ of L-algebras”, $\operatorname {\mathrm {Fm}}_{L\|\mathsf {K}}^{\{|n\}}$ is the carrier of $\|$ “the quotient $\mathfrak {Fm}_{\mathsf {K}}^{\{|n\}}$ of” the absolutely-free L-algebra $\mathfrak {Fm}_L^{\{|n\}}$ with free generators in $\{x_i\}_{i\in (\omega \{|\cap n\})}\ \|$ “by $\theta ^{\{|n\}}_{\mathsf {K}}\triangleq ((\operatorname {\mathrm {Fm}}^{\{|n\}}_L)^2\cap (\bigcap \{\ker h\mid h\in \hom (\mathfrak {Fm}^{\{|n\}}_L,\mathfrak {A}),\mathfrak {A}\in \mathsf {K}\}))$ ”; an L-logic C (viz., a closure operator over $\operatorname {\mathrm {Fm}}_L$ such that $\forall \Gamma \in (\operatorname {\mathrm {img}} C), \forall \sigma \in \hom (\mathfrak {Fm}_L,\mathfrak {Fm}_L): {\sigma }^{-1}[\Gamma ]\in (\operatorname {\mathrm {img}} C)$ , elements of $C(\varnothing )$ being called its theorems) is called $\lceil $ maximally/ $\rceil $ [inferentially] $\lceil $ /in $\rceil $ consistent, if $x_1\not \in (\lfloor /\operatorname {\mathrm {Fm}}_L\setminus \rceil C(\varnothing [\cup \{x_0\}]))\ \lceil $ “and C has no proper (viz., $\neq C$ ) [inferentially] consistent extension (viz., an L-logic with image $\subseteq (\operatorname {\mathrm {img}} C))$ ”/ $\rceil $ (“maximal” standing for “maximally consistent”), and [“uniform and” $|||$ ] $\lfloor \,$ [ $|||$ uniformly] finitely-valued and $\rfloor $ [{“n-valued and” $|$ }] of/“defined by” a $\lfloor $ finite $\rfloor $ [1-element] class $\mathsf {M}$ [identified with its element] of $\lfloor $ finitely-valued $\rfloor $ {n-valued $|(\omega \|n)$ -generated} L-matrices (viz., pairs $\mathcal {A\wr B}$ of L-algebras $\mathfrak {A\wr B}$ { $|$ “with $\lceil \leqslant \rceil (\omega \|n)\ \lceil $ distinct $\rceil $ generators”} and subsets $D^{\mathcal {A\wr B}}$ of their $\lfloor $ finite $\rfloor $ {n-element $|$ } carriers $A\wr B$ , “ $\mathcal {B}$ is a $\lceil $ strict $\rceil $ homomorphic image of $\mathcal {A}$ ”//“a submatrix of $\mathcal {A}$ “//” $\mathcal {A}^I$ with a set I” meaning “existence of any $h\in \hom (\mathfrak {A},\mathfrak {B})$ with $D^{\mathcal {A}}\subseteq {h}^{-1}[D^{\mathcal {B}}]\lceil \subseteq D^{\mathcal {A}}\rceil $ and $h[A]=B$ ”//“any $\langle {\mathfrak {B}},{B\cap D^{\mathcal {A}}}\rangle $ with a subalgebra $\mathfrak {B}$ of $\mathfrak {A}$ ”//“ $\langle {\mathfrak {A}^I},{(D^{\mathcal {A}})^I}\rangle $ ”), if $\{{h}^{-1}[D^{\mathcal {B}}]\mid h\in \hom (\mathfrak {Fm}_L,\mathfrak {B}),\mathcal {B}\in \mathsf {M}\}$ is a basis of $\operatorname {\mathrm {img}} C$ ; L-matrices defining extensions of C are called its models; the L-logic $C^{\mathrm {SC}}$ with image being the intersection of those of all extensions of C with same theorems is the greatest (under the extension partial ordering) one, called the structural completion of C; C is called structurally complete, if $C=C^{\mathrm {SC}}$ ; and a ( $2$ -valued) L-matrix $\mathcal {A}$ is called reduced, if $\operatorname {\mathrm {Co}}(\mathcal {A})\triangleq \{\theta \in \operatorname {\mathrm {Co}}(\mathfrak {A})\mid \theta [D^{\mathcal {A}}]\subseteq D^{\mathcal {A}}\})=\{\{\langle {a},{a}\rangle \mid a\in A\}\}$ (and $\neg $ -classical with unary $\neg \in L$ , if $(\neg ^{\mathfrak {A}}[D^{\mathcal {A}}/(A\setminus D^{\mathcal {A}})])=((A\setminus D^{\mathcal {A}})/D^{\mathcal {A}})$ ).

Thus, the structural completion/completeness of any [finitely-valued] logic is “uniform[ly finitely-valued, its finitely-valued defining matrix being constructed effectively”/ decidable, though the computational complexity of the construction/decision procedure to be extracted from this theorem is too big to count it practically applicable (even, to two-valued logics) that makes less generic results like the corollary above rather acute].

[1] A. P. Pynko, Four-valued expansions of Dunn-Belnap’s logic (I): Basic characterizations, The Bulletin of the Section of Logic , vol. 49 (2020), no. 4, pp. 401–437.

▸ALEXEJ PYNKO AND IVAN SELUK, Self-extensionality of finitely-valued sentential logics.

V.M. Glushkov Institute of Cybernetics, Glushkov prosp. 40, Kiev, 03680, Ukraine.

E-mail: pynko@i.ua.

Given any sentential language L with $\langle $ out $\rangle $ constants {and any $n\in (\omega \setminus ((1|0)\langle \cup 1\rangle ))$ } (with treating integers $\geqslant 0$ as sets of lesser ones and denoting their set by $\omega $ ) $\|$ “and any class $\mathsf {K}$ of L-algebras”, $\operatorname {\mathrm {Fm}}_{L\|\mathsf {K}}^{\{|n\}}$ is the carrier of $\|$ “the quotient $\mathfrak {Fm}_{\mathsf {K}}^{\{|n\}}$ of” the absolutely-free L-algebra $\mathfrak {Fm}_L^{\{|n\}}$ with free generators in $\{x_i\}_{i\in (\omega \{|\cap n\})}\ \|$ “by $(\operatorname {\mathrm {Fm}}^{\{|n\}}_L)^2\cap \bigcap \{\ker h\mid h\in \hom (\mathfrak {Fm}^{\{|n\}}_L,\mathfrak {A}),\mathfrak {A}\in \mathsf {K}\}$ ”; an L-logic C (viz., a closure operator over $\operatorname {\mathrm {Fm}}_L$ with $\forall \Gamma \subseteq \operatorname {\mathrm {Fm}}_L, \forall \sigma \in \hom (\mathfrak {Fm}_L,\mathfrak {Fm}_L): \sigma [C(\Gamma )]\subseteq C(\sigma [\Gamma ])$ ) is said to be self-extensional, if $\{\langle {\phi },{\psi }\rangle \in (\operatorname {\mathrm {Fm}}_L)^2\mid C(\{\phi \})=C(\{\psi \})\}\in \operatorname {\mathrm {Co}}(\mathfrak {Fm}_L)$ , and $\lfloor $ finitely-valued and $\rfloor $ [{“n-valued and” $|$ }] of/“defined by” a $\lfloor $ finite $\rfloor $ [1-element] class $\mathsf {M}$ [identified with its element] of $\lfloor $ finitely-valued $\rfloor $ {n-valued $|$ -generated} L-matrices (viz., pairs $\mathcal {A\wr B}$ of L-algebras $\mathfrak {A\wr B}$ { $|$ “with $\lceil \leqslant \rceil n\ \lceil $ distinct $\rceil $ generators”} and subsets $D^{\mathcal {A\wr B}}$ of their $\lfloor $ finite $\rfloor $ {n-element $|$ } carriers $A\wr B$ , “ $\mathbf {S}\mathfrak {A}$ ”//“a submatrix of $\mathcal {A}$ ” meaning “the set of $\lceil $ the carriers of $\rceil $ subalgebras of $\mathfrak {A}$ ”//“any $(\mathcal {A}{\upharpoonright } B)\triangleq \langle {\mathfrak {B}},{B\cap D^{\mathcal {A}}}\rangle $ with $\mathfrak {B}\in \mathbf {S}\mathfrak {A}$ ”), if $\{{h}^{-1}[D^{\mathcal {B}}]\mid h\in \hom (\mathfrak {Fm}_L,\mathfrak {B}),\mathcal {B}\in \mathsf {M}\}$ is a basis of $\operatorname {\mathrm {img}} C$ ; C/“an L-matrix defining it” is called $\neg $ -paraconsistent $\|\varphi $ -conjunctive with $1$ -ary $\|$ $(\neg \|\varphi )\in (L\|\operatorname {\mathrm {Fm}}^2_L)$ , if $(x_1\not \in C(\{x_0,\neg x_0\}))\| (C(\{x_i\}_{i\in 2})=C(\{\varphi \}))$ ; C/“an L-matrix $\mathcal {A}$ ” is called [strongly]/ $\|\ \varphi $ -implicative $\|$ -disjunctive, if $(\forall \phi ,\psi \in \operatorname {\mathrm {Fm}}_L,\forall \Gamma \subseteq \operatorname {\mathrm {Fm}}_L: (([(\varphi (\varphi (\varphi ,x_0),x_0)\in C(\varnothing ))\&]((\psi \in C(\Gamma \cup \{\phi \}))\Leftrightarrow (\varphi (\phi ,\psi )\in C(\Gamma ))))\|(C(\Gamma {\kern1pt}\cup{\kern1pt} \{\varphi (\phi ,\psi )\})=(C(\Gamma {\kern1pt}\cup{\kern1pt} \{\phi \}){\kern1pt}\cap{\kern1pt} C(\Gamma \cup \{\psi \})))))/(\forall a, b{\kern-1pt}\in{\kern-1pt} A: (((a{\kern-1pt}\in{\kern-1pt} \|\not \in D^{\mathcal {A}})\Rightarrow (b{\kern-1pt}\in{\kern-1pt} D^{\mathcal {A}}))\Leftrightarrow (\varphi ^{\mathfrak {A}}(a,b)\in D^{\mathcal {A}})))$ [so it is $\varphi (\varphi ,x_1)$ -disjunctive] $\|$ ; $\mathcal {A}$ is called reduced, if $\Delta _A^0=\Omega ^{\mathcal {A}}\triangleq (\bigcup \operatorname {\mathrm {Co}}(\mathcal {A})) \,(\in \operatorname {\mathrm {Co}}(\mathcal {A})\triangleq \{\theta \in \operatorname {\mathrm {Co}}(\mathfrak {A})\mid \theta [D^{\mathcal {A}}]\subseteq D^{\mathcal {A}}\})$ with $\Delta _B^{0[+1]}\triangleq ([B^2\setminus ]\{\langle {b},{b}\rangle \mid b\in B\})$ ; and $\mathcal {A}$ /“its logic” is called $\neg $ -[super-/infra-]classical, if $(A\|(2\setminus D^{\mathcal {A}})\|(\neg ^{\mathfrak {A}}[{\upharpoonright }2]))=((2[\cup \{{\frac {1}{2}} \}])\|1\|\Delta ^1_2)$ .

This yields a ([very] effective) algebraic criterion of self-extensionality of any ([“strongly implicative”/“conjunctive and disjunctive”] finitely-valued) L-logic (if L is finite).

This yields both a language-minimal instance of a self-extensional implicative $\|$ “both conjunctive and disjunctive” paraconsistent infra-classical logic, “an effective criterion of”[/non- $\|$ ]self-extensionality of “[strongly] implicative” $\|$ conjunctive [non-]paraconsistent infra-classical [/non-classical $\|$ ] logics and the (non-)self-extensionality of some infra-classical non-classical disjunctive conjunctive logics like (Kleene’s one, $LP$ , $HZ$ and $P^1$ , but) Gödel’s implicative one, so showing the necessity of the strength stipulation.

▸ALEXEJ PYNKO AND OLEG KOT, Extensions of constructive lattice three-valued logics.

V.M. Glushkov Institute of Cybernetics, Glushkov prosp. 40, Kiev, 03680, Ukraine.

E-mail: pynko@i.ua.

Given any [propositional] language L (viz., a set of finitary [propositional] connectives to be viewed as operation symbols, when dealing with L-algebras) with binary infix $\land $ and $\lor $ as well as unary prefix $\neg $ , let $\operatorname {\mathrm {Fm}}^{\{n\}}_L$ {with $n\in (\omega \setminus 1)\ \langle $ integers $\geqslant 0$ are treated as sets of lesser ones, the set of all them being denoted by $\omega \rangle $ } be the carrier of the absolutely-free L-algebra $\mathfrak {Fm}^{\{n\}}_L$ freely-generated by $\{x_i\}_{i\in (\omega \{\cap n\})}$ . Then, a [propositional] L-logic C (viz., a closure operator over $\operatorname {\mathrm {Fm}}_L$ with $\forall \Gamma \subseteq \operatorname {\mathrm {Fm}}_L, \forall \sigma \in \hom (\mathfrak {Fm}_L,\mathfrak {Fm}_L): \sigma [C(\Gamma )]\subseteq C(\sigma [\Gamma ])$ ) is called consistent $|$ “constructive/intuitionistic/ paracomplete”, unless $x_0|(x_0\lor \neg x_0)$ is a theorem of C (viz., an element of $C(\varnothing )$ ), and $\lceil $ strongly/classically $\rceil \ \iota $ -implicative, where $\iota \in \operatorname {\mathrm {Fm}}^2_L$ , if $\lceil (\iota (\iota (\iota ,x_0),x_0)\in C(\varnothing ))\&\rceil \forall \phi ,\psi \in \operatorname {\mathrm {Fm}}_L,\forall \Gamma \subseteq \operatorname {\mathrm {Fm}}_L: ((\psi \in C(\Gamma \cup \{\phi \}))\Leftrightarrow (\iota (\phi ,\psi )\in C(\Gamma )))$ , as well as structurally complete, unless it has a proper (viz., distinct from C) extension (viz., an L-logic with image $\subseteq (\operatorname {\mathrm {img}} C)$ ) with same theorems, i.e., any L-rule $\mathscr {R}$ (viz., a pair $\Gamma \vdash \varphi $ with $\Gamma \subseteq \operatorname {\mathrm {Fm}}_L\ni \varphi $ to be identified with $\varphi $ , if $\Gamma =\varnothing $ ) is satisfied in C (i.e., $\varphi \in C(\Gamma )$ ), if it is admissible in C, i.e., the extension of C relatively axiomatized by $\mathscr {R}$ (viz., the least one – under the extension partial ordering $\preceq $ – satisfying $\mathscr {R}$ ) has same theorems as C. Likewise, a [logical] L-matrix (viz., a pair $\mathcal {A}=\langle {\mathfrak {A}},{D}\rangle $ constituted by an L-algebra $\mathfrak {A}$ with carrier A and a $D\subseteq A$ , $(\mathbf {S}\mathfrak {A})|$ “ $\mathcal {A}{\upharpoonright } B$ with $B\in \mathbf {S}\mathfrak {A}$ ” denoting “the set of all subalgebras of $\mathfrak {A}$ identified with their carriers” $|\langle {\mathfrak {A}{\upharpoonright } B},{B\cap D}\rangle $ ) is called $\iota $ -implicative $|\neg $ -classical, if $(\forall a,b\in A: ((a\in D)\Rightarrow (b\in D))\Leftrightarrow (\iota ^{\mathfrak {A}}(a,b)\in D))|( (|A/D|=(2/1))\&(\neg ^{\mathfrak {A}}[D/(A\setminus D)]=((A\setminus D)/D)))$ . Then, any [one-element] class $\mathsf {M}$ [identified with its element] of L-matrices defines its (L-)logic $\operatorname {\mathrm {Cn}}_{\mathsf {M}}$ with closure basis $\{{h}^{-1}[D]\mid \langle {\mathfrak {A}},{D}\rangle \in \mathsf {M},h\in \hom (\mathfrak {Fm}_L,\mathfrak {A})\}$ of $\operatorname {\mathrm {img}}\operatorname {\mathrm {Cn}}_{\mathsf {M}}$ , L-logics {with extensions} defined by $\neg $ -classical L-matrices being called $\neg $ -{sub-}classical.

This covers all three-valued expansions of “the implication-less fragment $GL_3^*$ of Gödel’s” $|$ Kleene’s three-valued logic $GL_3|\text {"}KL_3$ including those of Łukasiewicz’ one”, in this way, providing an effective purely-algebraic criterion of “structural completeness of”/“admissibility of rules in”/“strong implicativity of $\neg $ -subclassical” ones, and so a new insight into (both the strong non-implicativity and) $|$ the structural completeness of $GL_3^{/\!/*}|$ “the bounded three-valued expansion of $KL_3$ by nullary connectives taking values in $2$ ” (thus showing the necessity of the $\lceil \rceil $ -optional strength stipulation) $/\!/|$ .