Logic Colloquium ’21, the annual European Summer Meeting of the Association of Symbolic Logic, was organized by the Faculty of Psychology and Cognitive Science and the Faculty of Mathematics and Computer Science at Adam Mickiewicz University Poznań. This conference was initially scheduled as Logic Colloquium ‘20, but it was postponed due to the covid pandemic. Logic Colloquium ’21 took place virtually from July 19 to July 24, 2021.

Funding and support for the conference was provided by the Association for Symbolic Logic (ASL), the Faculties of Psychology and Cognitive Science and of Mathematics and Computer Science at Adam Mickiewicz University Poznań, the Office of the Mayor of Poznań, and the US National Science Foundation, as well as the partner organizations the Polish Association for Logic and Philosophy of Science, the Polish Cognitive Science Society, and the Poznań Science and Technology Park.

The success of the meeting was largely due to the flexibility and excellent work of the Local Organizing Committee chaired by Mariusz Urbański and the Organizing Committee co-chaired by Mariusz Urbański and Roman Murawski. The remaining members of the Local Organizing Committee were Szymon Chlebowski, Andrzej Gajda, Marta Gawek, Patrycja Kupś, Paweł Łupkowski, Dawid Ratajczyk, Agata Tomczyk, Aleksandra Wasielewska, and Natalia Żyluk. The remaining members of the Organizing Committee were Wojciech Buszkowski, Joanna Golińska-Pilarek, Leszek Kołodziejczyk, Paweł Łupkowski, Marek Nasieniewski, Jerzy Pogonowski, Tomasz Skura, Kazimierz Swirydowicz, and Andrzej Wiśniewski.

The Program Committee consisted of Boris Zilber (University of Oxford, chair), Wojciech Buszkowski (Adam Mickiewicz University Poznań), Anuj Dawar (University of Cambridge), Giuseppe Primiero (University of Milan), Mariya Soskova (University of Wisconsin–Madison), Henry Towsner (University of Pennsylvania), and Matteo Viale (University of Torino)

The main topics of the conference were: Computability Theory, Logic in Cognitive Science and Linguistics, Modal and Epistemic Logic, Model Theory, Proofs and Programs, and Set Theory. The program included 2 tutorial courses, 11 invited lectures, among which was the Gödel Lecture by Elisabeth Bouscaren, 23 invited lectures in 6 special sessions, and 45 contributed talks. The following tutorial courses were given:

Krzysztof Krupiński (University of Wroclaw), Topological dynamics in model theory.

Andrew Marks (University of California Los Angeles), Characterizing Borel complexity and an application to decomposability.

The following invited plenary lectures were presented:

Elisabeth Bouscaren (CNRS—Université Paris-Saclay) gave the 31st Annual Gödel Lecture, The ubiquity of configurations in model theory.

Artem Chernikov (University of California Los Angeles), Measures in model theory.

Vera Fischer (University of Vienna), Combinatorial sets of reals.

Noam Greenberg (Victoria University of Wellington), The information common to relatively random sequences.

Benoît Monin (Creteil University), The computational content of Miliken’s tree theorem.

Luca Motto Ros (University of Turin), Generalized descriptive set theory for all cofinalities, and some applications.

Frank Pfenning (Carnegie Mellon University), Adjoint logic.

Elaine Pimentel (Federal University of Rio Grande do Norte), A pure view of ecumenical modalities.

Johan van Benthem (University of Amsterdam), Interleaving logic and counting, a view from below.

Linda Westrick (Pennsylvania State University), Reverse mathematics of Borel sets.

Ryan Williams (Massachusetts Institute of Technology), Complexity lower bounds from algorithm design.

More information about the meeting can be found at the conference website https://lc2021.cpl.

Abstracts of invited and contributed talks given in person or by title by members of the Association follow.

For the Program Committee

Boris Zilber

Abstract of the invited 31st Annual Gödel Lecture

▸ ELISABETH BOUSCAREN, The ubiquity of configurations in model theory.

CNRS—Université Paris -Saclay, Gif-sur-Yvette, France.

E-mail: elisabeth.bouscaren@universite-paris-saclay.fr.

Originally in Classification Theory, then in Geometric Stability, and now, beyond Stability, in Tame Model Theory, one common essential feature is the identification and study of some geometric configurations, of combinatorial and dimensional theoretic nature. They can witness the combinatorial and the model theoretic complexity of a theory or indicate the existence of specific definable algebraic structures. This enables model theory to tackle questions from very diverse subjects. We will attempt to illustrate the importance of these configurations through some examples.

Abstract of invited tutorials

▸ KRZYSZTOF KRUPIŃSKI, Topological dynamics in model theory.

University of Wrocław, Wrocław, Poland.

E-mail: kkrup@math.uni.wroc.pl.

Some fundamental notions and methods of topological dynamics were introduced to model theory by Newelski in the mid-2000s.

In the first part of my tutorial, I will recall some basic notions of topological dynamics, discuss the flows which appear naturally in model theory (as various spaces of types), and give applications of basic topological dynamics to some group covering results of Newelski such as: if an ${\aleph}_0$ -saturated group is covered by countably many 0-type-definable sets ${X}_n$ , $n\in \omega$ , then for some finite $A\subseteq G$ and $n\in \omega$ , $G = {AX}_n{X}_n^{-1}$ .

In the second part, I will define the Ellis semigroup and Ellis group of a flow, and focus on connections between the Ellis groups of natural flows in model theory and certain invariants of definable groups (quotients by model-theoretic connected components) or first order theories (Galois groups of first order theories as well as spaces of strong types). In particular, I will discuss the results of Pillay, Rzepecki, and myself which present certain invariants of this kind as quotients of compact (Hausdorff) groups (which are canonical Hausdorff quotients of Ellis groups). This has various consequences obtained by Pillay, Rzepecki, and myself, e.g., it leads to a general result that model-theoretic type-definability of a bounded invariant equivalence relation defined on a single complete type over $\varnothing$ is equivalent to descriptive set theoretic smoothness of this relation.

In the last part, I will discuss a definable variant of Kechris–Pestov–Todorčević (KPT) theory, developed by Lee, Moconja, and myself. KPT theory studies relationships between dynamical properties of the groups of automorphisms of Fraïssé structures and Ramsey-theoretic (so combinatorial) properties of the underlying Fraïssé classes. In our research, the idea is to find interactions between dynamical properties of first order theories (i.e., properties related to the actions of the automorphism group of a sufficiently saturated model on various types spaces over this model) and definable versions of Ramsey-theoretic properties of the theory. This leads to analogs of various results of KPT theory (i.e., a combinatorial characterization of the definable extreme amenability of a theory), but also to some rather novel theorems, e.g., yielding criteria for profiniteness of the Ellis group of a first order theory.

The author is supported by National Science Center, Poland, grants 2015/19/B/ST1/01151, 2016/22/E/ST1/00450, and 2018/31/B/ST1/00357.

▸ ANDREW MARKS, Characterizing Borel complexity and an application to decomposability.

University of California Los Angeles, Los Angeles, CA, USA.

E-mail: marks@math.ucla.edu.

We give a new characterization of when sets in the Borel hierarchy are ${\Sigma}_n^0$ hard. This characterization is proved using Antonio Montalban’s true stages method for conducting priority arguments in computability theory. We use this to prove the decomposability conjecture, assuming projective determinacy. The decomposability conjecture describes what Borel functions are decomposable into a countable union of partial continuous functions with ${\Pi}_n^0$ domains. This is joint work with Adam Day.

Abstracts of invited keynote lectures

▸ ARTEM CHERNIKOV, Measures in model theory.

Department of Mathematics, University of California Los Angeles, Los Angeles, CA 90095-1555, USA.

E-mail: chernikov@math.ucla.edu.

URL Address: http://www.math.ucla.edu/~chernikov/.

In model theory, a type is an ultrafilter on the Boolean algebra of definable sets in a structure, which is the same thing as a finitely additive $\left\{0,1\right\}$ -valued measure. This is a special kind of a Keisler measure, which is just a finitely additive real-valued probability measure on the Boolean algebra of definable sets. Introduced by Keisler in the late 80s, Keisler measures became a central object of study in the last decade. This is motivated by several intertwined lines of research. One of them (and perhaps the oldest one) is the development of probabilistic and continuous logics. Another is the study of definable groups in o-minimal, and more generally in NIP theories, leading to interesting connections with topological dynamics. Further motivation comes from applications in additive and in extremal combinatorics, uniting the aforementioned directions. I will survey some of the recent developments in the subject.

[1] A. Chernikov, Model theory, Keisler measures and groups, this Journal, vol. 24 (2018), no. 3, pp. 336–339.

[2] A. Chernikov and K. Gannon, Definable convolution and idempotent Keisler measures. Israel Journal of Mathematics , to appear, 2021, arXiv:2004.10378.

[3] A. Chernikov, E. Hrushovski, A. Kruckman, K. Krupinski, S. Moconja, A. Pillay, and N. Ramsey, Invariant measures in simple and in small theories, preprint, 2021, arXiv:2105.07281.

[4] A. Chernikov and P. Simon, Definably amenable NIP groups. Journal of the American Mathematical Society , vol. 31 (2018), no. 3, pp. 609–641.

[5] A. Chernikov and S. Starchenko, Regularity lemma for distal structures. Journal of the European Mathematical Society , vol. 20 (2018), no. 10, pp. 2437–2466.

[6] A. Chernikov and H. Towsner, Hypergraph regularity and higher arity VC-dimension, preprint, 2020, arXiv:2010.00726.

▸ VERA FISCHER, Combinatorial sets of reals.

University of Vienna, Vienna, Austria.

E-mail: vera.fischer@univie.ac.at.

Infinitary combinatorial sets of reals, such as almost disjoint families, cofinitary groups, independent families, and towers, occupy a central place in the study of the set-theoretic properties of the real line. Of particular interest are such extremal sets of reals, i.e., combinatorial sets which are maximal under inclusion with respect to a desired property, their possible cardinalities, definability properties, as well as the existence or non-existence of ZFC dependences. The study of such combinatorial sets of reals is closely connected with the development of a broad spectrum of forcing techniques.

In this talk we will see some recent advances in the subject and point towards interesting remaining open questions.

▸ NOAM GREENBERG, The information common to relatively random sequences.

Victoria University of Wellington, Wellington, New Zealand.

E-mail: noam.greenberg@vuw.ac.nz.

If $X$ and $Y$ are relatively random, what common information can $X$ and $Y$ have? We use algorithmic randomness and computability theory to make sense of this question. The answer involves some unexpected ingredients, such as the Lebesgue density theorem, and linear programming, and reveals a rich hierarchy of Turing degrees within the $K$ -trivial degrees.

▸ BENOÎT MONIN, The computational content of Miliken’s tree theorem.

Créteil University, Créteil, France.

E-mail: benoit.monin@computability.fr.

The Milliken’s tree theorem is an extension of Ramsey’s theorem to trees. It implies for instance that if we assign to all the sets of two strings of the same length, one among k colors, there is an infinite binary tree within which every pair of strings of the same height has the same color. We are going to present some results on Milliken’s tree theorem from the viewpoint of computability theory and reverse mathematics.

▸ LUCA MOTTO ROS, Generalized descriptive set theory for all cofinalities, and some applications.

University of Turin, Turin, Italy.

E-mail: luca.mottoros@unito.it.

Generalized descriptive set theory is nowadays a very active field of research. The idea is to develop a higher analogue of classical descriptive set theory in which $\omega$ is systematically replaced with an uncountable cardinal $\kappa$ . With a few exceptions, papers in this area tend to concentrate on the case of regular cardinals. This is because under such an assumption one can easily generalize a number of basic facts and techniques from the classical setup, but from the theoretical viewpoint the choice is indeed not fully justified.

In this talk I will survey some recent work in which the theory is instead developed in a uniform and cofinality-independent way, thus naturally including the case of singular cardinals. I will also consider some interesting applications connecting generalized descriptive set theory to Shelah’s stability theory (in the case of regular cardinals), and to the study of nonseparable complete metric spaces under Woodin’s axiom IO (in the case of singular cardinals of countable cofinality).

▸ FRANK PFENNING, Adjoint logic.

Carnegie Mellon University, Pittsburgh, PA, USA.

E-mail: fp@cs.cmu.edu.

We introduce adjoint logic as a general framework for integrating logics with different structural properties, that is, admitting or denying exchange, weakening, or contraction among the hypotheses. We investigate its proof-theoretic properties from two angles: proof construction and proof reduction. The former is the basis for applications in logical frameworks and logic programming, while the latter provides computational interpretations in functional and concurrent programming. We briefly sketch some of these applications.

The talk presents joint work with William Chargin, Klaas Pruiksma, and Jason Reed.

▸ ELAINE PIMENTEL, A pure view of ecumenical modalities.

University College London, London, UK.

E-mail: elaine.pimentel@gmail.com.

Recent works about ecumenical systems, where connectives from classical and intuitionistic logics can co-exist in peace, warmed the discussion of proof systems for combining logics [2, 3]. This discussion has been extended to alethic K-modalities in [1]: using Simpson’s meta-logical characterization, necessity is independent of the viewer, while possibility can be either intuitionistic or classical. In this work, we propose an internal pure calculus for ecumenical modalities, $\mathsf{nEK}$ , where every basic object of the calculus can be read as a formula in the language of the ecumenical modal logic $\mathsf{EK}$ . We prove that $\mathsf{nEK}$ is sound and complete w.r.t. the ecumenical birrelational semantics, and study fragments and modal extensions. This is joint work with Sonia Marin, Luiz Carlos Pereira, and Emerson Sales.

[1] S. Marin, L. C. Pereira, E. Pimentel, and E. Sales, Ecumenical modal logic, Dynamic Logic. New Trends and Applications—Third International Workshop, DaLí 2020 (M. A. Martins and I. Sedlár, editors), Springer Lecture Notes in Computer Science, vol. 12569, Springer, Cham, 2020, pp. 187–204.

[2] E. Pimentel, L. C. Pereira, and V. de Paiva, An ecumenical notion of entailment. Synthese , vol. 198 (2021), no. 22-S, pp. 5391–5413.

[3] D. Prawitz, Classical versus intuitionistic logic, Why Is This a Proof? Festschrift for Luiz Carlos Pereira (E. H. Haeusler, W. de Campos Sanz, and B. Lopes, editors), Tributes, vol. 27, College Publications, London, 2015, pp. 15–32.

▸ JOHAN VAN BENTHEM, Interleaving logic and counting, a view from below.

University of Amsterdam, Amsterdam, The Netherlands.

E-mail: johan@stanford.edu.

Reasoning with quantifier expressions in natural language combines logical and arithmetical features, transcending strict divides between qualitative and quantitative. Our topic is this cooperation of styles as it occurs in common linguistic usage and its extension into the broader practice of natural language plus “grassroots mathematics.”

A view from the top is afforded by $\mathsf{FO}\left(\#\right)$ , first-order logic with counting operators and cardinality comparisons. This system is known to be of very high complexity, and drowns out finer aspects of the combination of logic and counting. Therefore, we start from below, and first study a small fragment that can represent numerical syllogisms and basic reasoning about comparative size: monadic first-order logic with counting, $\mathsf{MFO}\left(\#\right)$ . We provide normal forms that allow for axiomatization, determine which arithmetical notions can be defined on finite and (using a separation theorem) on infinite models, and conversely, we discuss which logical notions can be defined out of purely arithmetical ones, and what sort of (non-)classical logics can be induced.

Next, moving upward, we investigate a series of strengthenings of $\mathsf{MFO}\left(\#\right)$ , again using normal form methods. The monadic second-order version is close, in a precise sense, to additive Presburger Arithmetic, while versions with the natural device of tuple counting take us to Diophantine equations, making the logic undecidable. We also define a system $\mathsf{ML}\left(\#\right)$ that combines basic modal logic over binary accessibility relations with counting, needed to formulate ubiquitous reasoning patterns such as the Pigeon Hole Principle. We prove decidability of $\mathsf{ML}\left(\#\right)$ , and provide a new kind of bisimulation matching the expressive power of the language.

As a complement to the fragment approach pursued here, we also discuss two other ways of lowering the complexity of $\mathsf{FO}\left(\#\right)$ by changing the semantics of counting in natural ways. A first approach replaces cardinalities by abstract but well-motivated values of “mass” or more generally, mereological aggregating notions. A second approach keeps the cardinalities but generalizes the meaning of counting to work in models that allow dependencies between variables.

Finally, we return to our starting point in natural language, confronting the architecture of the formal systems studied here with linguistic quantifier vocabulary and syntax, as well as with natural reasoning modules such as the monotonicity calculus. In addition to these encounters with formal semantics, we discuss the role of counting in semantic evaluation procedures for quantifier expressions and determine, for instance, which binary quantifiers are computable by finite “semantic automata.” We conclude with some general thoughts on yet further entanglements of logic and counting in formal systems, on rethinking the qualitative/quantitative divide, and on connecting our analysis to empirical findings in cognitive science.

Caveat. Combining logic and counting is a topic that has emerged in many places, with a vast and scattered literature. The full paper for this lecture contains a broad set of references to relevant papers in mathematical logic, computational logic, formal semantics, and cognitive science.

ILLC Amsterdam, Stanford, and Tsinghua University. Joint work with Thomas Icard, Stanford University.

▸ LINDA WESTRICK, Reverse mathematics of Borel sets.

Pennsylvania State University, State College, PA, USA.

E-mail: westrick@psu.edu.

Theorems about Borel sets are often proved using arguments which appeal to some regularity property of Borel sets, rather than recursing on the Borel structure of the set directly. For example, the statement “there is no Borel well-ordering of the reals” can be proved using either a measure or category argument. More generally, suppose we are given a theorem about Borel sets and a proof based on their measurability. Could the same theorem also be proved with a category argument? In principle, when the answer is “no,” reverse mathematics provides a framework for proving this negative answer. However, if ATR is taken as a base theory, measure and category arguments cannot be distinguished. That is because both “Every Borel set is measurable” and “Every Borel set has the property of Baire” follow already from ATR.

The notion of a completely determined Borel set, which is now a few years old, allows theorems involving Borel sets to be analyzed over a weaker base theory. The principles “Every c.d. Borel set is measurable” and “Every c.d. Borel set has the property of Baire” are both strictly weaker than ATR and incomparable with each other. With reference to these landmarks, we present what is known about the reverse mathematical strength of weak theorems involving Borel sets, including the Borel Dual Ramsey Theorem and some theorems from descriptive combinatorics. We also characterize the sets which HYP believes are c.d. Borel. This work was partially supported by NSF grant DMS-1854107, and parts are joint with various collaborators: Astor, Dzhafarov, Flood, Montalbán, Solomon, Towsner, and Weisshaar.

▸ RYAN WILLIAMS, Complexity lower bounds from algorithm design.

Massachusetts Institute of Technology, Cambridge, MA, USA.

E-mail: rrw@mit.edu.

Since the beginning of the theory of computation, researchers have been fascinated by the prospect of proving impossibility results on computing. When and how can we argue that a task cannot be efficiently solved, no matter what algorithm we use? I will briefly introduce some of the ideas behind a research program in computational complexity that I and others have studied, for the last decade. The program begins with the observations that:

1. (a) Computer scientists know a great deal about how to design efficient algorithms.

2. (b) However, we do not know how to prove many weak-looking complexity lower bounds.

It turns out that certain knowledge we have from (a) can be leveraged to prove complexity lower bounds in a systematic way, making progress on (b). For example, progress on faster circuit satisfiability algorithms (even those that barely improve upon exhaustive search) automatically imply circuit complexity lower bounds for interesting functions.

Abstracts of invited talks in the Special Session on Computability

▸ NIKOLAY BAZHENOV, Primitive recursive algebraic structures, and the theory of numberings.

Sobolev Institute of Mathematics, Novosibirsk, Russia.

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

The paper of Kalimullin, Melnikov, and Ng (2017) was a starting point for the recent significant progress in the studies of sub-recursive algebra. The key notion in these developments is that of a punctual structure. A countably infinite structure $S$ is punctual if the domain of $S$ is the set of natural numbers, and the signature predicates and functions of $S$ are uniformly primitive recursive. In the talk, we discuss recent results on punctual algebraic structures, and related results on upper semilattices of numberings.

▸ ARMAN DARBINYAN, Computable groups and computable group orderings.

Texas A&M University, College Station, TX, USA.

E-mail: adarbina@math.tamu.edu.

An important class of abstract groups is the one that consists of linearly ordered groups whose orders are invariant under left (and right) group multiplications. From computability point of view it is interesting to investigate when orderable groups admit computable orders. In particular, a question of Downey and Kurtz asks about existence of computable orderable groups that do not admit computable orders with respect to any group presentation. In my talk I will discuss recent advancements on this topic.

▸ JUN LE GOH, Redundancy of information: lowering effective dimension.

University of Wisconsin–Madison, Madison, WI, USA.

E-mail: junle.goh@wisc.edu.

The effective Hausdorff dimension of an infinite binary sequence can be characterized using the (normalized) Kolmogorov complexity of its initial segments (Mayordomo). It is invariant under changes on a set of positions of upper density $0$ . Greenberg, Miller, Shen, and Westrick initiated the study of how effective Hausdorff dimension can be changed if one is allowed to change a sequence on a set of positive upper density. Specifically, given some $X$ of dimension $t$ , what is the minimum density of changes needed to obtain some $Y$ of dimension $s$ ? The situation differs depending on $X$ , as well as the value of the target dimension $s$ relative to the value of the starting dimension $t$ . We present joint work with Miller, Soskova, and Westrick on these questions.

▸ LESZEK KOLODZIEJCZYK, Weak König’s Lemma in the absence of ${\Sigma}_1^0$ induction.

University of Warsaw, Warsaw, Poland.

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

Reverse mathematics studies the logical strength of mathematical theorems by proving implications between the theorems and some well-established set existence principles expressed in the language of second-order arithmetic. The implications are proved over a fixed base theory embodying “computable mathematics.” The usual base theory, ${\mathrm{RCA}}_0$ , is axiomatized by comprehension for computable (i.e., ${\Delta}_1^0$ -definable) properties of natural numbers and by induction for c.e. (i.e., ${\Sigma}_1^0$ -definable) properties. In the 1980s, Simpson and Smith introduced an alternative weaker base theory ${\mathrm{RCA}}_0^{\ast }$ , in which ${\Sigma}_1^0$ -induction is replaced by ${\Delta}_1^0$ -induction.

One of the most important set existence principles considered in reverse mathematics is Weak König’s Lemma, $\mathrm{WKL}$ . This states that every infinite binary tree has an infinite branch. Since there are computable binary trees without computable branches, $\mathrm{WKL}$ is not provable in ${\mathrm{RCA}}_0$ , but it is well-known that adding $\mathrm{WKL}$ to ${\mathrm{RCA}}_0$ results in a theory that does not prove any new ${\Pi}_1^1$ statements.

Already Simpson and Smith showed that an analogous ${\Pi}_1^1$ -conservation result for $\mathrm{WKL}$ also holds over ${\mathrm{RCA}}_0^{\ast }$ . We prove that $\mathrm{WKL}$ nevertheless behaves very differently over ${\mathrm{RCA}}_0^{\ast }+\neg {\mathrm{RCA}}_0$ than in the traditional setting. Namely, any two countable models of ${\mathrm{RCA}}_0^{\ast }+\mathrm{WKL}$ that have a common first-order part and share a common witness to the failure of ${\Sigma}_1^0$ -induction are isomorphic. It follows, for instance, that $\mathrm{WKL}$ is the strongest ${\Pi}_2^1$ statement that is ${\Pi}_1^1$ -conservative over ${\mathrm{RCA}}_0^{\ast }+\neg {\mathrm{RCA}}_0$ . Moreover, the isomorphism theorem provides new information about the structure of models of ${\mathrm{RCA}}_0$ that satisfy ${\Delta}_2^0$ - but not ${\Sigma}_2^0$ -induction, which has some implications for traditional reverse mathematics.

Joint work with Marta Fiori Carones, Tin Lok Wong, and Keita Yokoyama.

Abstracts of invited talks in the Special Session on Logic in Cognitive Science and Linguistics

▸ JONATHAN GINZBURG, Quantifiers as (quasi)-referential pluralities.

Laboratoire de Linguistique Formelle, CNRS, Université de Paris, Paris, France.

E-mail: yonatan.ginzburg@u-paris.fr.

(Joint work with Andy Lücking (Université de Paris and Goethe-Universität Frankfurt))

A great insight of Richard Montague’s [6] was to use Mostowski’s notion of Generalized Quantification [7] to offer a uniform syntax and semantics for both referential and quantification terms. Via subsequent work of Barwise, Cooper, Keenan, Stavi, van Benthem, Westerstahl [1, 2, 5, 10], and many others this ushered in a golden age of work on natural language quantification.

Nonetheless, there are grounds to question whether a semantics based on Generalized Quantification is optimal as an analysis of the meaning of natural language nominal terms, once we consider certain cognitive desiderata. Classical formal semantics, going back to [4], characterizes meanings in terms of (communicative) success conditions. A semantics intended for conversation is also required to explicate the resulting context in cases involving communicative problems since these result in the highly systematic process of clarification interaction [9]. The data from clarification questions and their answers accord with standard approaches that associate individuals as the content of proper names and deictic pronoun utterances, and properties with verb utterances. What, then, for the clarificational potential of quantified Noun Phrases? [8] show, based on data from the British National Corpus (a collection of spontaneous conversations), that answers to clarification questions about quantified noun phrases communicate individuals and sets of individuals and even function denoting noun phrases. However, there is no evidence of talk about Generalized Quantifiers (sets of sets/properties of properties, the contents associated with noun phrases according to Generalized Quantifier Theory).

Natural language understanding is incremental, occurring at a latency that is at least as fast as word by word. Therein lies another problem for a Generalized Quantifier approach to quantification in that such terms can be understood incrementally as talking directly of sets, before any available predicator occurs.

Given these and several other problems for a Generalized Quantifier strategy, I will present an alternative approach, based on viewing nominals as structured pluralities. More specifically, we postulate that nouns denote ordered set partitions. From these denotations, using Type Theory with Records [3], we construct meanings for noun phrases that allow access both to the (witness) reference set and the (anti-witness) complement set that noun phrase uses give rise to. On the basis of this a variety of natural language phenomena can be explicated relating to anaphora, clarification, and gesture. The framework also directly derives fundamental properties of quantified noun phrases such as conservativity, while considerably simplifying the computational complexity of the denotations.

[1] J. Barwise and R. Cooper, Generalized quantifiers and natural language. Linguistics and Philosophy , vol. 4 (1981), no. 2, pp. 159–219.

[2] J. van Benthem, Determiners and logic. Linguistics and Philosophy , vol. 6 (1983), no. 4, pp. 447–478.

[3] R. Cooper and J. Ginzburg, Type theory with records for natural language semantics, The Handbook of Contemporary Semantic Theory , second ed. (S. Lappin and C. Fox, editors), Wiley-Blackwell, Oxford, 2015, pp. 375–407.

[4] G. Frege, “Uber Sinn und Bedeutung”. Zeitschrift für Philosophie und philosophische Kritik , vol. 100 (1892), no. 1, pp. 25–50. Reprinted in Funktion—Begriff—Bedeutung (M. Textor, editor), “Sammlung Philosophie, vol. 4,” Vandenhoeck & Ruprecht, Göttingen, 2002, pp. 2–22.

[5] E. L. Keenan and J. Stavi, A semantic characterization of natural language determiners. Linguistics and Philosophy , vol. 9 (1986), no. 3, pp. 253–326.

[6] R. Montague, The proper treatment of quantification in ordinary English, Formal Philosophy (R. Thomason, editor), Yale University Press, New Haven, 1974.

[7] A. Mostowski, On a generalization of quantifiers. Fundamenta mathematicae , vol. 44 (1957), no. 2, pp. 12–36.

[8] M. Purver and J. Ginzburg, Clarifying noun phrase semantics. Journal of Semantics , vol. 21 (2004), no. 3, pp. 283–339.

[9] M. Purver, J. Ginzburg, and P. Healey, On the means for clarification in dialogue, Current and New Directions in Discourse & Dialogue (R. Smith and J. van Kuppevelt, editors), Kluwer Academic, Amsterdam, 2003, pp. 235–255.

[10] D. Westerståhl, Determiners and context sets, Generalized Quantifiers in Natural Language (A. ter Meulen and J. van Benthem, editors), De Gruyter Mouton, Berlin, 1985, pp. 45–72.

▸ MICHAEL KAMINSKI, Extending the Lambek calculus with classical negation.

Technion—Israel Institute of Technology, Haifa, Israel.

E-mail: kaminski@cs.technion.ac.il.

The Lambek calculus is tightly related to categorial grammars—a family of formalisms for natural language syntax. The categorial grammars can bear only positive information, whereas, as it has been pointed out (independently) by Wojciech Biszkowski and Heinrich Wansing about 25 years ago, negative information is also of importance. In our talk, we present an axiomatization of the non-associative Lambek calculus extended with classical negation and show that the frame semantics with the classical interpretation of negation is sound and complete for this extension.

▸ PIOTR ŁUKOWSKI. A proposal for formalization of Kahneman and Tversky’s thinking fast and slow.

Department of Logic, Institute of Philosophy, Jagiellonian University, Kraków, Poland.

E-mail: piotr.lukowski@uj.edu.pl.

Fregean versus non-Fregean paradigm.

Frege’s Axiom by Suszko: There are only two references for all sentences: truth and falsehood. All true sentences have one and the same reference, the truth; all false sentences have one and the same reference, the falsehood. An acceptance of Frege’s axiom means to semantically reduce all sentences to two or more objects, the logical values. Thus, there are sentences with completely different meanings but with the same semantic correlate (i.e., their logical value). This approach leads to many paradoxes, including paradoxes of material implication or paradoxes of self-reference.

Example 1. How to interpret the connective of implication appearing in the classical tautology ( $\alpha \to \beta$ ) $\vee$ ( $\beta \to \alpha$ )? For any two sentences, at least one implies the other? What does it mean?

Example 2. How to formalize the liar sentence L? Is L $\leftrightarrow \neg$ L a correct expressing of the sense L says “L is false?” After all, the liar sentence says nothing about equivalence of sentences.

Example 3. The Linda problem.

After getting acquainted with the characteristics of a previously unknown Linda, the subjects assessed the conjunctions of two sentences as more likely than that of one of these sentences. Now, that is as conjunction fallacy. Of course, the list of problems is long, and well known. So, let us follow Suszko and reject Frege’s axiom, and let us see what comes out of it. Thus, let every sentence has its own semantic correlate, understood as situation or content.

Two non-Fregean logics plus one not standard inference. One of these logics is well known Suszko’s SCI, and the second is the logic with content implication CCL. However, the logic closest to our thinking seems to be a specific contentual inference. It is seemingly non-monotonic, with empty set of tautologies inference satisfying the rule of implosion: from contradiction, nothing, like in our everyday thinking.

Thinking fast and slow. Using the same class of mappings and the same class of models it is possible to define two kinds of inferences. One is like fast and the second like slow thinking, both described by Kahneman and Tversky.

▸ MARIUSZ URBAŃSKI, Descriptions are not enough and norms are not forever. Formal modelling of human reasoning processes: triggers, methods, and results.

Adam Mickiewicz University, Poznań, Poland.

E-mail: Mariusz.Urbanski@amu.edu.pl.

Since the end of the twentieth century, certain areas of logic become more and more oriented towards modelling actual cognitive activities of more or less idealized agents. Drawing on enormous achievements brought about by the mathematical turn that started more than 100 years ago, logic now has come back to its Aristotelian roots as an instrument by which we come to know anything. The re-forged alliance between logic—now well equipped with sophisticated formal tools—and psychology results in more and more substantial developments in studies on human reasoning and problem-solving. To reap the fruits of this alliance we need to be aware that it leads to a shift in focal points of interest of such studies as well as to the expansion of their methodological repertoire. In this talk, I argue that such a practical, or cognitive, turn in logic results in (1) the concept of error becoming crucial for formal modelling of human reasoning processes; (2) prescriptive perspective, which takes into account human limitations in information processing, becoming the most interesting vantage point for such research; and (3) triangulation of formal methods, quantitative approach, and qualitative analyses becoming the most effective methodology in formal modelling studies.

Abstracts of invited talks in the Special Session on Modal and Epistemic Logic

▸ ALEXANDRU BALTAG, The logic of Cantor’s derivative and the perfect core: a topological exploration of unknowable worlds, surprise exams, and other epistemic paradoxes.

University of Amsterdam, Amsterdam, The Netherlands.

E-mail: thealexandrubaltag@gmail.com.

What is the epistemic meaning of Cantor–Bendixson’s derivative? A common epistemic (mis)interpretation is that Cantor’s derivative is a good topological model for belief. In several joint papers, I criticized this interpretation as ad-hoc and highly problematic. In this talk, I give what I think is the correct answer to the above question, generalizing to arbitrary topologies an idea that goes back (in a restricted, S5 setting) to an old paper by Rohit Parikh.

I start by briefly reviewing the view of topology as a model for evidential epistemology, in particular recalling the two epistemic interpretations of topological interior: as knowledge, or as knowability (by the corresponding agent), depending on whether the topology is taken to represent “evidence in hand” (=the actual evidence currently available to the agent) or “evidence out there” (=the potential evidence, that might be observed or learnt by the agent). I then move to the derivative modality $D(P)$ , extracting its epistemic meaning from that of the interior modality. It turns out that $D(P)$ captures the “lack of knowledge,” or “unknowability,” of the actual world even in the presence of additional information $P$ .

Once derivative is thus understood, you’ll be wondering how did you ever manage to do any epistemic logic without it. I show that derivative and its multi-agent generalizations play a key role in a wide range of well-known epistemic puzzles: from the Wise Men (or Muddy Children) puzzle, to the Two Numbers’ Puzzle, to the Surprise Exam Paradox. I explain how the Cantor–Bendixson process of iterating derivatives $D(P)$ , $D\left(D(P)\right)$ , etc. models the informational dynamics underlying all these puzzles, and how the (non-)paradoxicality of different scenarios is related to the (non-)emptiness of the greatest fixed point of this process: the “perfect core” ${D}^{\infty }(P)$ of the set $P$ .

I then present a complete axiomatization of the logic of Cantor’s derivative and the perfect core, and prove its decidability. This last part is based on joint work with Nick Bezhanishvili and David Fernandez-Duque.

▸ THOMAS BOLANDER, From dynamic epistemic logic to socially intelligent robots.

Technical University of Denmark, Kongens Lyngby, Denmark.

E-mail: tobo@dtu.dk.

Dynamic Epistemic Logic (DEL) can be used as a formalism for agents to represent the mental states of other agents: their beliefs and knowledge, and potentially even their plans and goals. Hence, the logic can be used as a formalism to give agents a Theory of Mind allowing them to take the perspective of other agents. In my research, I have combined DEL with techniques from automated planning in order to describe a theory of what I call Epistemic Planning: planning where agents explicitly reason about the mental states of others. Recently, Lasse Dissing, Nicolai Hermann, and I have implemented the framework of epistemic planning on physical robots and applied the implementation to human–robot collaboration scenarios. One of the recurring themes is implicit coordination: how to successfully achieve joint goals in decentralised multi-agent systems without prior negotiation or coordination. The talk will first give an introduction to epistemic planning based on DEL and will then demonstrate its use in human–robot collaboration.

▸ HELLE HVID HANSEN, Automata minimisation in logical form.

University of Groningen, Groningen, The Netherlands.

E-mail: h.h.hansen@rug.nl.

Recently, two apparently quite different duality-based approaches to automata minimisation have appeared. One [3] is based on ideas that originated from the controllability–observability duality from systems theory, and the other [2] is based on ideas derived from Stone-type dualities specifically linking coalgebras with algebraic structures derived from modal logics.

In this talk, I will present an abstract framework, based on coalgebraic modal logic, that unifies the two approaches [1]. As in the Stone-duality approach, the algebras are essentially logics for reasoning about automata viewed as coalgebras. By exploiting the ability to pass between coalgebras and algebras via a dual adjunction, and extending this dual adjunction to one between automata, we obtain an abstract minimisation algorithm that has several instances, including the Brzozowski minimisation algorithm of DFAs. Further examples include deterministic Kripke frames based on a Stone-type duality, weighted automata based on the self-duality of semimodules, topological automata based on Gelfand duality, and alternating automata based on the discrete duality between sets and complete atomic Boolean algebras.

[1] N. Bezhanishvili, M. Bonsangue, H. H. Hansen, D. Kozen, C. Kupke, P. Panangaden, and A. Silva, Minimisation in logical form, Outstanding Contributions to Logic , Springer–Palgrave, to appear, 2020, arXiv:2005.11551.

[2] N. Bezhanishvili, C. Kupke, and P. Panangaden, Minimization via duality, Proceedings of WoLLIC 2012 (Buenos Aires, Argentina), Springer Lecture Notes in Computer Science, vol. 7456, Springer, 2012.

[3] F. Bonchi, M. Bonsangue, H. H. Hansen, P. Panangaden, J. Rutten, and A. Silva, Algebra-coalgebra duality in Brzozowski’s minimization algorithm. ACM Transactions on Computational Logic , vol. 15 (2014), no. 1, pp. 1–29.

▸ SOPHIA KNIGHT, Reasoning about agents’ knowledge about one another’s strategies in strategy logic.

University of Minnesota Duluth, Duluth, MN, USA.

E-mail: sophia.knight@gmail.com.

In this talk I will discuss some new developments in Strategy Logic with imperfect information. Strategy Logic is concerned with agents’ strategic abilities in multi-agent systems, and unlike ATL, treats strategies as first-class objects in the logic, independent from the agents. Thus, in imperfect information settings, Strategy Logic raises delicate issues, such as what agents know about one another’s strategies. I will describe a new version of Strategy Logic that ensures that agents’ strategies are uniform, and allows a formal description of their knowledge about each other’s strategies. This talk is on joint work with Bastien Maubert, Aniello Murano, Sasha Rubin, Francesco Belardinelli, and Alessio Lomuscio.

Abstracts of invited talks in the Special Session on Model Theory

▸ PABLO CUBIDES KOVACSICS, Beautiful pairs and spaces of definable types.

Heinrich Heine Universität Düsseldorf, Düsseldorf, Germany.

E-mail: cubidesk@hhu.de.

We introduce a general notion of beautiful pairs which encompasses classical results of Poizat in the stable case and of van den Dries–Lewemberg/Pillay in the o-minimal case. We obtain an Ax–Kochen–Ershov-type result, showing that beautiful pairs of certain classes of henselian valued fields are essentially controlled by the corresponding beautiful pairs of the value group and residue field. As an application, we infer strict pro-definability of various spaces of definable types. For simplicity, the talk will mainly focus on the case of algebraically closed non-trivially valued fields, where the associated spaces of definable types have a concrete geometric interpretation, e.g., the stable completion introduced by Hrushovski–Loeser, and a model theoretic analogue of the Huber analytification of an algebraic variety.

This is work in progress, joint with Martin Hils and Jinhe Ye.

▸ YATIR HALEVI, Definable fields in various dp-minimal fields.

Ben-Gurion University of the Negev, Beersheba, Isreal.

E-mail: yatirh@gmail.com.

The study of definable (or interpretable) fields in various fields has a long history, though with relatively few results, in model theory. For interpretable fields the proof usually relies on elimination of imaginaries in some well-understood language.

In this talk we outline a proof that every definable field in a dp-minimal valued field $K$ , of characteristic $0$ , with generic differentiability of definable functions is definably isomorphic to a finite extension of $K.$ This latter condition holds, e.g., in p-adically closed fields, t-convex power-bounded fields, and algebraically closed valued fields (really in any 1-h-minimal dp-minimal valued field).

If time permits, we will briefly outline a general method for the study of fields interpretable in dp-minimal valued fields (of characteristic 0) satisfying generic differentiability of definable functions, which bypasses elimination of imaginaries. More specifically, we show that in some situations the “interpretable” case reduces (locally) to the “definable” case.

(Joint work with Assaf Hasson and Kobi Peterzil)

▸ DANIEL MAX HOFFMANN, Kim-independence and ranks.

Instytut Matematyki, Uniwersytet Warszawski, Warsaw, Poland.

E-mail: d.hoffmann@uw.edu.pl.

There are two main, quite independent, goals of this talk:

• • to describe how the Kim-independence can be induced by its counterpart from the absolute Galois group;

• • to present some ranks developed for NSOP ${}_1$ .

Before coming to the aforementioned points of the talk, I will start with a mild introduction to the class of NSOP ${}_1$ theories and provide a summary of the recent results in the NSOP ${}_1$ . Of course, the list of results will be incomplete and just my personal insight into the subject.

The content of the first goal of this talk is based on the results from [3]. Basically, we generalize there theorems of Zoé Chatzidakis and Nick Ramsey on PAC fields [1, 4] to the level of arbitrary PAC substructures of a stable model. We show how the Kim-independence descents from the many sorted structure of the absolute Galois group of a PAC structure to the PAC structure itself.

Second goal of the talk is related to searching for a proper rank for any NSOP ${}_1$ theory. There is already a notion of rank intended for NSOP ${}_1$ which might be found in [2]. However, there are some questions related to this rank and we would like to propose a slightly different approach to the rank for NSOP ${}_1$ .

[1] Z. Chatzidakis, Amalgamation of types in pseudo-algebraically closed fields and applications. Journal of Mathematical Logic , vol. 19 (2019), no. 2, p. 1950006.

[2] A. Chernikov, B. Kim, and N. Ramsey, Transitivity, lowness, and ranks in NSOP ${}_1$ theories, preprint, 2020, arXiv:2006.10486.

[3] D. M. Hoffmann and J. Lee, Co-theory of sorted profinite groups for PAC structures, preprint, 2021, arXiv:1905.09748.

[4] S. N. Ramsey, Independence, amalgamation, and trees . Ph.D. thesis, University of California, Berkeley, 2018.

Abstracts of invited talks in the Special Session on Proofs and Programs

▸ DOMINIQUE LARCHEY-WENDLING, Extraction of recursive algorithms in Coq using the Braga method.

The French National Centre for Scientific Research, Paris, France.

E-mail: dominique.larchey-wendling@loria.fr.

This is joint work with J. F. Monin.

We present the Braga method which we use to get verified OCaml programs by extraction from fully specified Coq terms. Unlike structural recursion which is accepted as is by Coq, the Braga method works systematically with more involved recursive schemes, including the nonterminating schemes of partial algorithms, nested or mutually recursive schemes, etc. The method is based on two main concepts linked together: an inductive description of the computational graph of an algorithm and an inductive characterization of its domain. The computational graph mimics the structure of recursive calls of the algorithm and serves both (a) as a guideline for the definition of a domain predicate of which the inductive structure is compatible with recursive calls; and (b) as a conformity predicate to ensure that the Coq algorithm logically reflects the original algorithm at a low-level.

▸ THOMAS POWELL, Some recent work in proof mining.

Bath University, Bath, UK.

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

I present some recent results on the application of proof-theoretic methods in functional analysis, where we produce rates of convergence for algorithms that compute fixpoints for a general class of contractive mappings [2]. The talk does not assume any background in either proof theory or functional analysis but will instead aim to provide a high-level illustration of some of the core ideas that are relevant to applied proof theory in general.

The first part of the talk focuses on a simple example from [1], in which it is shown that if $T$ is a $\psi$ -weakly contractive mapping then the Picard scheme ${x}_{n+1} = {Tx}_n$ converges to a fixpoint of $T$ . The proof of this fact involves reducing the problem to the following recursive inequality on sequences of nonnegative reals:

It can be shown that under suitable conditions on $\psi$ , any such sequence converges to zero, and moreover an explicit rate of convergence can be given.

We discuss logical aspects of this proof, and in the second part of the talk proceed to show how one can produce very general convergence results by following the same basic proof scheme adapted to more complex recursive inequalities. In all cases, explicit rates of convergence are formulated in terms of the relevant “proof-theoretic” moduli.

[1] Y. Alber and S. Guerre-Delabriere, Principle of weakly contractive maps in Hilbert spaces, New Results in Operator Theory and Its Applications (I. Gohberg and Y. Lyubich, editors), Operator Theory: Advances and Applications, vol. 98, Birkhauser, Basel, 1997, pp. 7–22.

[2] T. Powell and F. Wiesnet, Rates of convergence for asymptotically weakly contractive mappings in normed spaces, preprint, 2021, arXiv:2104.14495.

▸ VINCENT RAHLI, Brouwerian intuitionistic realizability theories.

University of Birmingham, Birmingham, UK.

E-mail: v.rahli@bham.ac.uk.

In this talk, I will present two Brouwerian intuitionistic realizability theories, namely BITT and OpenTT, whose underlying notions of computability go beyond that of standard Church-Turing. These two time-relative theories capture, through Brouwer’s concept of choice sequences, the intuitionistic notion that new knowledge can be acquired as time progresses. We will describe how these two theories capture intuitionistic theories of choice sequences. In addition, we will discuss the status of the Law of Excluded Middle (LEM) w.r.t., these two theories. LEM, which essentially flattens the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired, can be shown to be false in BITT. It is however consistent with OpenTT, which relies on a more relaxed model of time, which is more classically inclined than BITT’s.

As BITT and OpenTT are both inspired by CTT (a Brouwerian intuitionistic realizability theory implemented by the Nuprl proof assistant), we will start with a description of CTT. We will in particular describe how we were able to extend CTT with Brouwer’s continuity principle for numbers as well as his bar induction principle (which allows deriving induction principles for W types), by validating these principles using our implementation of CTT in Coq.

This is joint work with Liron Cohen (Ben-Gurion University of the Negev, Beersheba, Israel), Mark Bickford, and Bob Constable (Cornell University, Ithaca, NY, USA).

▸ HELMUT SCHWICHTENBERG, Proofs and computation with infinite data.

University of Munich, Munich, Germany.

E-mail: schwicht@math.lmu.de.

It is natural to represent real numbers in $\left[{-}1,1\right]$ by streams of signed digits ${-}\mathrm{1,0,1}$ . Algorithms operating on such streams can be extracted from formal proofs involving a unary coinductive predicate CoI on (standard) real numbers $x$ : a realizer of CoI( $x$ ) is a stream representing $x$ . We address the question how to obtain bounds for the look-ahead of such algorithms: how far do we have to look into the input streams to compute the first $n$ digits of the output stream? We present a proof-theoretic method how this can be done. The idea is to replace the coinductive predicate CoI( $x$ ) by an inductive predicate $I\!\left(x,n\right)$ with the intended meaning that we know the first $n$ digits of a stream representing $x$ . Then from a formal proof of $Ix\!\left(n+1\right)\to Iy\!\left(n+1\right)\to I\!\left(\left(x+y\right)\!/2\right)n$ we can extract an algorithm for the average function whose look-ahead is $n+1$ for both arguments. This is joint work with Nils Köpp.

Abstracts of invited talks in the Special Session on Set Theory

▸ DOMINIK ADOLF AND OMER BEN-NERIA, Tree-like scales and free subsets of set theoretic algebras.

Hebrew University, Jerusalem, Israel.

E-mail: omer.bn@mail.huji.ac.il.

In his Ph.D. thesis, Luis Pereira isolated and developed several principles of singular cardinals that emerge from Shelah’s PCF theory; principles which involve properties of scales, such as the inexistence of continuous Tree-Like scales, and properties of internally approachable structures such as the Approachable Free Subset Property. In the talk, I will discuss these principles and their relations, and present new results from a joint work with Dominik Adolf concerning their consistency and consistency strength.

▸ SANDRA MÜLLER, The strength of determinacy when all sets are universally Baire.

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

Faculty of Mathematics, University of Vienna, Kolingasse 14-16, 1090 Vienna, Austria.

E-mail: sandra.mueller@tuwien.ac.at.

URL Address: http://www.logic.univie.ac.at/~smueller/.

The large cardinal strength of the Axiom of Determinacy when enhanced with the hypothesis that all sets of reals are universally Baire is known to be much stronger than the Axiom of Determinacy itself. In fact, Sargsyan conjectured it to be as strong as the existence of a cardinal that is both a limit of Woodin cardinals and a limit of strong cardinals. Larson, Sargsyan, and Wilson showed that this would be optimal via a generalization of Woodin’s derived model construction. We will discuss a new translation procedure for hybrid mice extending work of Steel, Zhu, and Sargsyan and use this to prove Sargsyan’s conjecture.

▸ GIORGIO VENTURI, On non-classical models of ZFC.

Department of Philosophy, State University of Campinas, Rua Cora Coralina, 100, Campinas, SP, Brazil.

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

In this talk we present some recent developments in the study of non-classical models of ZFC. We will show that there are algebras that are neither Boolean, nor Heyting, but that still give rise to models of ZFC. This result is obtained by using an algebra-valued construction similar to that of the Boolean-valued models. Specifically we will show the following theorem.

Theorem 1. There is an algebra $\mathbb{A}$ , whose underlying logic is neither classical, nor intuitionistic such that ${\mathbf{V}}^{\mathbb{A}}\models$ ZFC. Moreover, there are formulas in the pure language of set theory such that ${\mathbf{V}}^{\mathbb{A}}\models \varphi \wedge \neg \varphi$ .

The above result is obtained by a suitable modification of the interpretation of equality and belongingness, which are classical equivalent to the standard ones, used in Boolean-valued constructions.

Towards the end of the talk we will present an application of these constructions, showing the independence of CH from non-classical set theories, together with a general preservation theorem of independence from the classical to the non-classical case.

(This is a joint work with Sourav Tarafder and Santiago Jockwich)

▸ TREVOR M. WILSON, Characterizing strong cardinals, virtually strong cardinals, and other large cardinals by Löwenheim–Skolem properties

Department of Mathematics, Miami University, 123 Bachelor Hall, 301 S. Patterson Avenue, Oxford, OH 45056, USA.

E-mail: twilson@miamioh.edu.

Let us say that a logic $L$ has the Löwenheim–Skolem (LS) property at a cardinal $\kappa$ if every sentence of $L$ with a model $M$ also has a model ${M}_0$ of cardinality less than $\kappa$ , and has the Löwenheim–Skolem–Tarski (LST) property at $\kappa$ if in addition we may take ${M}_0$ to be a substructure of $M$ . Magidor [1] proved that the least cardinal at which second-order logic ${L}_{\omega \omega}^2$ has the LST property equals the least supercompact cardinal. By weakening the LST property to the LS property and strengthening ${L}_{\omega \omega}^2$ to various fragments of infinitary second-order logic ${L}_{\infty \infty}^2$ , we obtain similar characterizations of various other large cardinals.

Letting ${L}_{\omega \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ be the fragment of ${L}_{\infty \infty}^2$ obtained from atomic formulas and their negations by the operations of infinitary disjunction, finitary conjunction, infinitary universal quantification, and finitary existential quantification, we show that the least cardinal at which ${L}_{\omega \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ has the LS property equals the least strong cardinal. We also show that the least cardinal at which ${L}_{\omega \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ has the weak LS property, which is the special case of the LS property in which $M$ has cardinality exactly $\kappa$ , equals the least measurable cardinal.

Letting ${L}_{\kappa \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ be as above but also allowing $<\kappa$ -ary conjunctions, we show that any given cardinal $\kappa$ is strong if and only if ${L}_{\kappa \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ has the LS property at $\kappa$ , and is measurable if and only if ${L}_{\kappa \omega}^2\left({\vee}_{\infty }{\forall}_{\infty}\right)$ has the weak LS property at $\kappa$ . We also obtain analogous results for ${L}_{\kappa \omega}^2\left({\vee}_{\infty}\right)$ , which allows only finitary quantification. Namely, we show that any given cardinal $\kappa$ is virtually strong (a new large cardinal property weaker than remarkability) if and only if ${L}_{\kappa \omega}^2\left({\vee}_{\infty}\right)$ has the LS property at $\kappa$ , and is completely ineffable if and only if ${L}_{\kappa \omega}^2\left({\vee}_{\infty}\right)$ has the weak LS property at $\kappa$ .

[1] M. Magidor, On the role of supercompact and extendible cardinals in logic. Israel Journal of Mathematics , vol. 10 (1971), no. 2, pp. 147–157.

Abstracts of contributed talks

▸ CLAUDIO AGOSTINI AND EUGENIO COLLA, An algebraic characterization of Ramsey monoids.

Department of Mathematics “G. Peano”, Università degli Studi di Torino, Via Carlo Alberto 10, 10123 Torino, Italy.

E-mail: claudio.agostini@unito.it.

E-mail: eugenio.colla@unito.it.

Carlson’s Theorem on variable words and Gowers’ ${\mathrm{FIN}}_k$ Theorem are generalizations of Hindman’s Theorem that involve a monoid action on a semigroup. In short, they state that for any finite coloring of a semigroup there is an infinite monochromatic “span.” They differ in the choice of the monoid. Recently, Solecki in [1] isolated from these two theorems the notion of Ramsey monoid, providing a common generalization of them. Then, he proved that an entire class of finite monoids is Ramsey. In this talk, I will present some of the results from a joint work with Eugenio Colla, where we prove a generalization of Solecki’s theorem, enlarging the class of monoids that can be proved to be Ramsey and reaching a simple algebraic characterization of Ramsey monoids.

[1] S. Solecki, Monoid actions and ultrafilter methods in Ramsey theory. Forum of Mathematics, Sigma , vol. 7 (2016), p. E2.

▸ AIZHAN ALTAYEVA, BEIBUT KULPESHOV, AND SERGEY SUDOPLATOV, On algebras of binary formulas for almost $\omega$ -categorical weakly o-minimal theories.

Institute of Mathematics and Mathematical Modeling, Al-Farabi Kazakh National University, Pushkin Street 125, Almaty, Kazakhstan.

E-mail: vip.altayeva@mail.ru.

Kazakh-British Technical University, Tole bi Street 59, Almaty, Kazakhstan.

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

Sobolev Institute of Mathematics, Novosibirsk State Technical University, Karl Marx Avenue 20, Novosibirsk, Russia.

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

In [1, 2], algebras of distributions of binary isolating formulas for both countably categorical weakly o-minimal theories and quite o-minimal theories with few countable models were described. Here we describe algebras of distributions of binary isolating formulas for almost $\omega$ -categorical weakly o-minimal theories.

Definition 1 [3, 5]. Let $T$ be a complete theory, and ${p}_1\!\left({x}_1\right),\dots, {p}_n\!\left({x}_n\right)\in {S}_1\!\left(\varnothing \right)$ . A type $q\!\left({x}_1,\dots, {x}_n\right)\in {S}_n\!\left(\varnothing \right)$ is said to be a $\left({p}_1,\dots, {p}_n\right)$ -type if $q\!\left({x}_1,\dots, {x}_n\right)\supseteq \underset{i = 1}{\overset{n}{\cup }}{p}_i\left({x}_i\right)$ . The set of all $\left({p}_1,\dots, {p}_n\right)$ -types of the theory $T$ is denoted by ${S}_{p_1,\dots, {p}_n}(T)$ . A countable theory $T$ is said to be almost $\omega$ -categorical if for any types ${p}_1\!\left({x}_1\right)$ , $\dots$ , ${p}_n\!\left({x}_n\right)\in {S}_1\!\left(\varnothing \right)$ there are only finitely many types $q\!\left({x}_1,\dots, {x}_n\right)\in {S}_{p_1,\dots, {p}_n}(T)$ .

The convexity rank of a formula with one free variable was introduced in [4].

Theorem 2. Let $T$ be an almost $\omega$ -categorical weakly o-minimal theory, $p,q\in {S}_1\!\left(\varnothing \right)$ be non-algebraic, $p\not\perp^w q$ . Then the algebra ${\mathfrak{P}}_{\nu \left(\left\{p,q\right\}\right)}$ of binary isolating formulas is generalized commutative iff ${\mathrm{RC}}_{\mathrm{bin}}(p) = {\mathrm{RC}}_{\mathrm{bin}}(q)$ .

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

[1] D. Yu. Emeliyanov, B. Sh. Kulpeshov, and S. V. Sudoplatov, Algebras of distributions for binary formulas in countably categorical weakly o-minimal structures. Algebra and Logic , vol. 56 (2017), no. 1, pp. 13–36.

[2] _____, Algebras of distributions of binary isolating formulas for quite o-minimal theories. Algebra and Logic , vol. 57 (2019), no. 6, pp. 429–444.

[3] K. Ikeda, A. Pillay, and A. Tsuboi, On theories having three countable models. Mathematical Logic Quarterly , vol. 44 (1998), no. 2, pp. 161–166.

[4] B. Sh. Kulpeshov, Weakly o-minimal structures and some of their properties. Journal of Symbolic Logic , vol. 63 (1998), pp. 1511–1528.

[5] S. V. Sudoplatov, Classification of Countable Models of Complete Theories, Part 1 , Novosibirsk State Technical University Publishing House, Novosibirsk, 2018.

▸ JOHN T. BALDWIN, On strongly minimal Steiner systems: Zilber’s conjecture, universal algebra, and combinatorics.

Mathematics, Statistics and Computer Science, University of Illinois at Chicago, 850 S. Morgan Street, Chicago, IL 60607, USA.

E-mail: jbaldwin@uic.edu.

URL Address: http://homepages.math.uic.edu/jbaldwin/.

This is joint work with Viktor Verbovski. We refine Zilber’s trichotomy by studying several variants on definable closure and exploring strongly minimal sets with flat geometries. We find the following classes: 0) $\mathrm{acl}$ is trivial; $\mathrm{acl}$ is non-trivial but: 1) $\mathrm{sdcl}$ (see below) is trivial on independent sets (no commutative binary functions), 2) $\mathrm{dcl}$ is trivial on independent sets (no binary functions), and 4) definable binary functions exist, e.g., quasigroups and ternary rings. This includes the basic Hrushovski example with any admissible $\mu$ ( $\delta (B)\le \mu \left(A/B\right)$ ) [2]. In particular no structure in class 1) admits elimination of imaginaries. (Verbovskiy has an example with elimination of imaginaries in an infinite vocabulary.) This includes the basic ternary Hrushovski example with any admissible $\mu$ ( $\delta (B)\le \mu \left(A/B\right)$ ) [2].

To distinguish the classes 0)–4) we introduce several notions. We write ${G}_I$ ( ${G}_{\left\{I\right\}}$ ) for the group of automorphisms of a model $M$ that fix $I$ pointwise (setwise). For either choice of $G$ , $\mathcal{A}$ is $G$ -normal if it is finite $G$ -invariant and strong in $M$ . Then $a$ is in $\mathrm{dcl}(X)$ ( $\mathrm{sdcl}(X)$ ) if $a$ is fixed by ${G}_X$ , ( ${G}_{\left\{X\right\}}$ ). We introduce the notion of tree-decomposition of a $G$ -normal subset. Under appropriate conditions on $\mu$ , we prove for all $G$ normal sets $\mathcal{A}$ , by induction on the height of $\mathcal{A}$ , that ${\mathrm{dcl}}^{\ast }(I)$ ( ${\mathrm{sdcl}}^{\ast }(I)$ ) is empty when $G = {G}_I$ , ( ${G}_I$ ) and $I$ is independent with $\mid I\mid <\omega$ . (The $\ast$ means $a$ depends on all elements of $I$ .) In particular, we show that strongly minimal systems from [1, 2] can be found in each classes 1)–4).

[1] J. T. Baldwin and G. Paolini, Strongly minimal Steiner systems I: Existence. Journal of Symbolic Logic , vol. 86 (2021), no. 4, pp. 1486–1507.

[2] E. Hrushovski, A new strongly minimal set. Annals of Pure and Applied Logic , vol. 62 (1993), pp. 147–166.

▸ NIKOLAY BAZHENOV, DARIUSZ KALOCIŃSKI, AND MICHAŁ WROCŁAWSKI, Degree spectra of unary recursive functions on naturals with standard ordering.

Sobolev Institute of Mathematics, 4 Akademika Koptyuga Avenue, 630090 Novosibirsk, Russia.

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

Institute of Computer Science, Polish Academy of Sciences, ul. Jana Kazimierza 5, 01-248 Warsaw, Poland.

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

Faculty of Philosophy, University of Warsaw, ul. Krakowskie Przedmieście 3, 00-927 Warsaw, Poland.

E-mail: m.wroclawski@uw.edu.pl.

Existing results provide some insights into obtaining computable, c.e. or ${\Delta}_2$ degrees as a spectrum of a unary recursive function on naturals with standard ordering $\le$ [1, 3]. We extend these results by providing a more complete picture, covering natural subclasses of unary recursive functions. For example, we show that if a computable structure $\left(\omega, \le, f\right)$ has a finitely generated infinite substructure, then the degree spectrum of $f$ on $\left(\omega, \le \right)$ contains precisely c.e. degrees. This prompts to introduce the notion of an $f$ -block, understood as a substructure of $\left(\omega, \le, f\right)$ , with the domain equal to some interval in $\left(\omega, \le \right)$ and with no proper substructures. We will discuss the following result: if a computable structure $\left(\omega, \le, f\right)$ , with $f$ unary, has only finitely many isomorphism types of $f$ -blocks, and all its $f$ -blocks are finite, then either $f$ is intrinsically computable or its degree spectrum on $\left(\omega, \le \right)$ consists of all ${\Delta}_2$ degrees.

We also briefly discuss the philosophical side of the results which becomes more apparent when viewed through the lens of Shapiro’s notations for natural numbers [2]. For example, Shapiro’s notion of a function computable in every notation (with computable ordering) coincides with functions having the trivial degree spectrum. Our results provide a more fine-grained classification of the complexity of functions in various notations, as measured by the Turing degrees thereof.

[1] R. Downey, B. Khoussainov, J. S. Miller, and L. Yu, Degree spectra of unary relations on $\left(\omega, <\right)$ , Logic, Methodology and Philosophy of Science (C. Glymour, W. Wei, and D. Westerstahl, editors), College Publications, London, 2009, pp. 35–55.

[2] S. Shapiro, Acceptable notation. Notre Dame Journal of Formal Logic , vol. 23 (1982), no. 1, pp. 14–20.

[3] M. Wright, Degrees of relations on ordinals. Computability , vol. 7 (2018), no. 4, pp. 349–365.

▸ GAIA BELARDINELLI AND RASMUS K. RENDSVIG, Epistemic planning with attention as a bounded resource.

Center for Information and Bubble Studies, University of Copenhagen, Copenhagen, Denmark.

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

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

Where information grows abundant, attention becomes scarce. As a result, agents must plan wisely how to allocate their attention in order to achieve epistemic efficiency. Here, we present a framework for multi-agent epistemic planning with attention, based on Dynamic Epistemic Logic (DEL; powerful formalism for epistemic planning [1]). The static part of the framework is composed by an attention state: a Kripke model augmented with an attention function that assigns to each agent a quantitative attention budget. The budget is spent in the dynamic part to learn formulas from a language for attention and knowledge. The learning dynamics are partly captured by an attention action: an action model augmented with a cost function and a questioning function. The cost function specifies how much attention the agent must spend to learn any given formula; the questioning function specifies what formula each agent is attempting to learn the truth-value of, by paying attention to it. A product update then merges the attention state and action to represent the epistemic changes and the relative attention expenditures.

We identify this framework as a fragment of standard DEL, and consider its plan existence problem [1]: given an (initial) attention state, a finite set of attention actions, and a goal formula, is there a finite sequence of the attention actions applicable to the initial attention state that realizes the goal formula? While in the general case the plan existence problem is undecidable, we show that when attention is required for learning, all instances of the problem are decidable.

[1] T. Bolander, T. Charrier, S. Pinchinat, and F. Schwarzentruber, DEL-based epistemic planning: Decidability and complexity. Artificial Intelligence , vol. 287 (2020), p. 103304.

▸ DYLAN BELLIER, MASSIMO BENERECETTI, DARIO DELLA MONICA, AND FABIO MOGAVERO, Good-for-game QPTL: an alternating Hodges semantics.

IRISA, University of Rennes, Rennes, France.

E-mail: dylan.bellier@irisa.fr.

Università di Napoli “Federico II”, Naples, Italy.

E-mail: massimo.benerecetti@unina.it.

E-mail: fabiomogavero@gmail.com.

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

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

The well-established connection between logic and games is witnessed by the fact that satisfiability of a (first-order) logical formula can be reduced to deciding whether a player has a winning strategy in a zero-sum two-player game. Logic can also be used to reason about coalition-games, by encoding moves of the opposing coalitions by means of existentially and universally quantified variables and by describing the game with a formula over those variables. Deciding who wins the game reduces to deciding whether the resulting sentence is satisfiable. When infinite games are considered, one can make the quantified variables range over (infinite) sequences of moves. This leads to first-order extensions of temporal logics, which predicate over infinite sequences of temporal points, one for each round of the game. In this setting, however, the satisfiability and the game solution problems do not coincide anymore, since the choices of one player at each round may depend on the future choices of the adversary.

Inspired by the work on dependence logics [1, 3, 5], we propose a novel semantics, generalizing Hodges’ one [2], for a first-order extension of Linear Temporal Logic [4], where functional dependencies among the variables can be restricted so that their current values are independent of the future values of the other variables. This allows us to encode various forms of independence constraints and provide a powerful tool to fine-tune the semantics of the propositional quantifiers. In particular, we discuss a specific instantiation of the semantics that allows one to recover a compositional game-theoretic interpretation of the quantifiers and reconcile the satisfiability and the game solution problems. This semantics leads to 2ExpTime decision procedures for both satisfiability and model-checking, heavily reducing the complexity of the logic when interpreted with the standard semantics.

Work partially supported by the GNCS 2020 project “Ragionamento Strategico e Sintesi Automatica di Sistemi Multi-Agente.”

[1] S. Abramsky, J. Kontinen, J. Väänänen, and H. Vollmer, Dependence Logic: Theory and Applications , Birkhäuser, Cham, 2016.

[2] W. Hodges, Compositional semantics for a language of imperfect information. Logic Journal of the Interest Group in Pure and Applied Logic , vol. 5 (1997), no. 4, pp. 539–563.

[3] A. L. Mann, G. Sandu, and M. Sevenster, Independence-Friendly Logic—A Game-Theoretic Approach , Cambridge University Press, Cambridge, 2011.

[4] A. Pnueli, The Temporal Logic of Programs, 18th Annual Symposium on Foundations of Computer Science (Providence, RI, USA), IEEE, 1977, pp. 46–57.

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

▸ LAURENT BIENVENU, VALENTINO DELLE ROSE, AND TOMASZ STEIFER, Computable randomness relative to almost all oracles.

LaBRI, CNRS & Université de Bordeaux, 351 Cours de la Libration, 33405 Talence, France.

E-mail: laurent.bienvenu@u-bordeaux.fr.

Università degli Studi di Siena—Rettorato, via Banchi di Sotto 55, 53100 Siena, Italy.

E-mail: valentin.dellerose@student.unisi.it.

Institute of Fundamental Technological Research, Polish Academy of Sciences, ul. Pawinskiego 5B, 02-106 Warszawa, Poland.

E-mail: tsteifer@ippt.pan.pl.

It follows from van Lambalgen’s theorem for Martin-Löf randomness, that every Martin-Löf random set $X$ is also Martin-Löf random relative to almost all oracles. Is this also true for notions of randomness for which van Lambalgen’s theorem does not hold? We answer this question in the negative for computable randomness. A binary sequence $X$ is a.e. computably random if there is no probabilistic computable strategy which is total and succeeds on $X$ for positive measure of oracles. Using the fireworks technique we construct a sequence which is computably random but not a.e. computably random. We also prove separation between a.e. computable randomness and partial computable randomness. This happens exactly in the uniformly almost everywhere dominating Turing degrees.

[1] L. Bienvenu and L. Patey, Diagonally non-computable functions and fireworks. Information and Computation , vol. 253 (2017), pp. 64–77.

[2] L. Yu, When van Lambalgen’s theorem fails. Proceedings of the American Mathematical Society , vol. 135 (2007), no. 3, pp. 861–864.

▸ KATALIN BIMBÓ, Abaci running backward.

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

E-mail: bimbo@ualberta.ca.

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

Abacus machines were introduced by Lambek in [3]. (See [2] for a newer and easily accessible presentation.) Abacus machines are a full model of computation, which are equivalent to Turing machines, Markov algorithms, etc. They are ingenious in having only two kinds of instructions while also being deterministic (and computing functions on $\mathrm{\mathbb{N}}$ ). A way in which a logic may be connected to a model of computation is through proofs, for example, proofs in a sequent calculus. In [1], we raised a problem for certain undecidability proofs by pointing out that the sequent calculus proofs, on which the undecidability claims rely, model backward computation.

In this talk, I define the notion of reverse computation for an abacus—following similar notions for finite state automata and finite state transducers introduced earlier. To ensure that reverse computation is as flexible as it reasonably can be, reverse computation is defined as a non-deterministic notion. Then, I prove that reverse computation in abaci is not sufficiently powerful to compute primitive recursive functions.

[1] K. Bimbó and J. M. Dunn, Modalities in lattice-R, 2015, submitted.

[2] G. S. Boolos and R. C. Jeffrey, Computability and Logic , third ed., Cambridge University Press, Cambridge, 1992.

[3] J. Lambek, How to program an infinite abacus. Canadian Mathematical Bulletin , vol. 4 (1961), no. 3, pp. 295–302.

▸ PAUL BLAIN LEVY, Broad infinity and generation principles.

School of Computer Science, University of Birmingham, Birmingham B15 2TT, UK.

E-mail: p.b.levy@bham.ac.uk.

URL Address: www.cs.bham.ac.uk/~pbl.

This work, presented in detail in [2], has three main contributions:

• • To introduce an (arguably intuitive) set-theoretic axiom scheme, called Broad Infinity.

• • To show it provides powerful generation principles for families, and (assuming AC) for sets and ordinals.

• • To show it is equivalent (assuming AC) to the widely studied Ord-is-Mahlo scheme: every closed unbounded class of ordinals contains a regular ordinal [1, 3].

The new scheme is presented as follows. Let $\mathfrak{T}$ denote the universal class.

Firstly we want $\mathsf{Start}\in \mathfrak{T}$ and $\mathsf{Build}:{\mathfrak{T}}^3\to \mathfrak{T}$ such that $\mathsf{Build}$ is injective and never yields $\mathsf{Start}$ . The following achieves this:

A signature consists of a set $I$ and an $I$ -indexed family of sets ${\left({K}_i\right)}_{i\in I}$ . A broad signature is a class function from $\mathfrak{T}$ to the class of all signatures.

Given a broad signature $G$ , a set $X$ is said to be $G$ -inductive when the following conditions hold.

• • $\mathsf{Start}\in X$ .

• • For any $x\in X$ with $Gx = {\left({K}_i\right)}_{i\in I}$ , and any $i\in I$ and ${K}_i$ -tuple ${\left[{a}_k\right]}_{k\in {K}_i}$ of elements of $X$ , we have $\mathsf{Build}\left(x,i,{\left[{a}_k\right]}_{k\in {K}_i}\right)\in X$ .

A set of all $G$ -broad numbers is a minimal (and therefore least) $G$ -inductive set. The axiom scheme of Broad Infinity states that, for every broad signature $G$ , there is a set of all $G$ -broad numbers. Equivalently: the class of all $G$ -broad numbers (i.e., the least $G$ -inductive class, which can be constructed) is a set. We may visualize a $G$ -broad number as a well-founded three-dimensional tree.

Here is an attempt to articulate the intuitive justification for Broad Infinity. For any $G$ -broad number of the form $\mathsf{Build}\left(x,i,{\left[{a}_k\right]}_{k\in {K}_i}\right)$ , the signature $Gx = {\left({K}_i\right)}_{i\in I}$ is obtained from $x$ , which “has already been constructed.” This seems to provide a clearly specified construction process.

[1] A. Lévy, Axiom schemata of strong infinity in axiomatic set theory. Pacific Journal of Mathematics , vol. 10 (1960), no. 1, pp. 223–238.

[2] P. B. Levy, Broad infinity and generation principles, preprint, 2021, arXiv:2101.01698.

[3] H. Wang, Large sets, Logic, Foundations of Mathematics, and Computability Theory (R. E. Butts and J. Hintikka, editors), D. Reidel, Dordrecht, 1977, pp. 309–333.

▸ NICOLA BONATTI, Two questions concerning quantifiers rules.

Munich Center for Mathematical Philosophy, LMU Munich, Geschwister-Scholl-Platz 1, Munich, Germany.

E-mail: Nicola.Bonatti@campus.lmu.de.

NK systems are distinguished on whether they adopt subordinate proofs for the rules of the quantifiers $\forall$ and $\exists$ , thus distinguishing between indirect rules (Existential Elimination, Universal Introduction—see [2]) and direct rules (Existential Instantiation and Universal Generalisation—see [3]). Even if the rules are logically equivalent, the choice between direct and indirect rules has raised philosophical discussion on the role of eigenvariables in proofs. More precisely, as suggested by [1], the descriptive question concerning the role of eigenvariables in proofs should be distinguished from the normative question of what grounds the restrictions on both direct and indirect rules. In this talk, I will first argue that both direct and indirect quantifiers rules represent the same order relation—called term-dependence—among the eigenvariables introduced within a proof (either by direct or indirect rules). The order relation of term-dependence represents and constraints the choice process of instances for consecutive application of (in)direct rules—thus answering the normative question. Then, I will point out that term-dependence is instantiated in NK ${}_{\varepsilon }$ (namely, NK extended with Hilbert’s $\varepsilon$ -operator—see [4]) at the syntactic level of nested $\varepsilon$ -terms. I will conclude that term-dependence is best represented by NK ${}_{\varepsilon }$ , where the $\varepsilon$ -terms I are interpreted as eigenvariables—thus answering the descriptive question.

[1] K. Fine, Reasoning with Arbitrary Objects , Blackwell, Oxford–NewYork, 1985.

[2] F. B. Fitch, Symbolic Logic , Ronald Press, New York, 1952.

[3] W. V. O. Quine, Methods of Logic , Harvard University Press, New York, 1950.

[4] R. Zach, Semantics and proof theory of the epsilon calculus, 7th Indian Conference on Logic and Its Applications (S. Ghosh and S. Prasad, editors), Springer, Berlin–Heidelberg, 2017, pp. 27–47.

▸ HORATIU CHEVAL, General metatheorems in proof mining.

University of Bucharest, Bucharest, Romania.

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

Proof mining [2] is a research program within applied proof theory having as its goal the extraction of information hidden in non-constructive proofs. The extracted content may take the form of quantitative results such as uniform effective bounds, or of the weakening of certain premises. A crucial advance came in 2005, when Kohlenbach [1] proved the first general metatheorems guaranteeing a priori, under certain conditions, that such results can be obtained. These metatheorems are each applicable in the context of a certain class of mathematical structures, Kohlenbach initially providing versions for inner product spaces, normed spaces, bounded metric spaces, $W$ -hyperbolic spaces, or $\mathrm{CAT}(0)$ spaces. Since 2005, metatheorems for other classes of structures in optimization and nonlinear analysis have been developed, for example, for $\mathrm{\mathbb{R}}$ -trees and totally bounded metric spaces.

By identifying in the systems used in the results we enumerated the common properties involved in the proofs of the metatheorems, we introduce a generalization of them to a unified logical system of a more abstract class of structures satisfying these properties, containing the restrictions to systems without dependent choice of the aforementioned metatheorems as particular instances, with the goal of facilitating the introduction of metatheorems for structures not previously approached.

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

[2] U. Kohlenbach, Applied Proof Theory: Proof Interpretations and Their Use in Mathematics , Springer Monographs in Mathematics, Springer, Berlin–Heidelberg, 2008.

▸ SZYMON CHLEBOWSKI, MARCIN JUKIEWICZ, ALEKSANDER KIRYK, DOROTA LESZCZYŃSKA-JASION, MICHAŁ SOCHAŃSKI, AND AGATA TOMCZYK, Synthetic tableaux: minimal tableau search heuristics.

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

E-mail: Szymon.Chlebowski@amu.edu.pl.

E-mail: Marcin.Jukiewicz@amu.edu.pl.

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

E-mail: Michal.Sochanski@amu.edu.pl.

E-mail: Agata.Tomczyk@amu.edu.pl.

Faculty of Mathematics and Computer Science, Adam Mickiewicz University, ul. Uniwersytetu Poznańskiego 4, Poznań, Poland.

E-mail: kiryk@wmi.amu.edu.pl.

In [1] we report on research on heuristics for generating minimal synthetic tableaux (ST) for CPL. The research was conducted in a quasi-experimental setting. Based on theoretical considerations we described a number of functions indicating heuristics of an optimal ST construction, and we developed a methodological framework to examine the efficiency of these functions.

Functions were tested on over 30 million of ST for more than 240000 of formulas. The outcomes are satisfactory: we have settled the most efficient functions indicating heuristics to use them on larger data; also the methodological framework has been tested with a preliminary success.

In our talk we present the outcomes of further experiments conducted on data sets containing randomly generated formulas longer than those used in the first phase of research.

This work was supported financially by National Science Centre, Poland, Grant No. 2017/26/E/HS1/00127.

[1] M. Sochański, D. Leszczyńska-Jasion, Sz. Chlebowski, A. Tomczyk, and M. Jukiewicz, Synthetic tableaux: minimal tableau search heuristics, 2021, submitted.

▸ ANAHIT CHUBARYAN, HAYK GASPARYAN, AND SARGIS HOVHANNISYAN, Comparison of two propositional proof systems by lines and by sizes.

Department of Informatics and Applied Mathematics, Yerevan State University, 1 Alex Manoogian, Yerevan, Armenia.

E-mail: achubaryan@ysu.am.

E-mail: haykgasparyan012@gmail.com.

E-mail: saqohovhannisyan0199@gmail.com.

The two main proof complexity characteristics (lines and sizes) are compared for two classes of formulas in some “weak” propositional proof system, based on generalization of splitting method, and in one of “strong” systems—Frege systems.

For any proof system $\phi$ and tautology $\varphi$ we denote by ${t}_{\varphi}^{\phi }$ ( ${l}_{\varphi}^{\phi }$ ) the minimal possible value of lines (sizes) for all $\phi$ -proofs of tautology $\varphi$ .

We compare propositional proof system $\mathrm{GS}$ , based on generalization of splitting method, which is defined in [2], and system $\mathbf{\mathcal{F}}$ —one of well-known Frege systems.

Our formulas are:

and

Main results are the following:

and

Earlier it is proved in [2] that for sufficiently big $n$ and $\forall i$ ( $1\le i<\left[n{\log}_n2\right]$ ) for formulas ${\varphi}_n^i = {\mathrm{TTM}}_{n,{n}^i}$ we have ${\log}_2{t}_{\varphi_n^i}^{\mathrm{GS}} = \Omega \left({n}^i\right)$ and ${\log}_2{l}_{\varphi_n^i}^{\mathrm{GS}} = \Omega \left({n}^i\right)$ , and it is proved in [1] that ${t}_{{\mathbf{TTM}}_{n,{\mathbf{2}}^n-\mathbf{1}}}^{\mathrm{\mathcal{F}}}$ and ${l}_{{\mathbf{TTM}}_{n,{\mathbf{2}}^n-\mathbf{1}}}^{\mathrm{\mathcal{F}}}$ are polynomial bounded.

Comparative analysis of above results shows that the first system is better by both complexity characteristics for the first of considered formula classes, just as the second system is better for the other classes.

[1] S. R. Aleksanyan and An. A. Chubaryan, The polynomial bounds of proof complexity in Frege systems. Siberian Mathematical Journal , vol. 50 (2009), no. 2, pp. 243–249.

[2] An. Chubaryan and Arm. Chubaryan, Bounds of some proof complexity characteristics in the system of splitting generalization. Otechestv. Nauka w epokhu izmenenij , vol. 10 (2015), no. 2(7), pp. 11–14.

▸ ANAHIT CHUBARYAN AND ARSEN HAMBARDZUMYAN, On non-monotonous properties of some propositional proof systems.

Department of Informatics and Applied Mathematics, Yerevan State University, 1 Alex Manoogian, Yerevan, Armenia.

E-mail: achubaryan@ysu.am.

E-mail: arsen.hambardzumyan2@ysumail.am.

We investigate the relations between the proof lines of non-minimal tautologies and its minimal tautologies for some propositional systems of classical and nonclassical logics.

Definition 1. A tautology of some logic is called minimal if the replacement result of all occurrences for each of its non-elementary subformulas by some new variable is not a tautology of the same logic.

Definition 2. A minimal tautology $\varphi$ of some logic is minimal of some formula $\psi$ if $\varphi$ is $\psi$ , or $\varphi$ is the replacement result of all occurrences of some non-elementary subformulas of $\psi$ by some new variable. We denote by $M\left(\psi \right)$ the set of all minimal tautologies of the tautology $\psi$ .

We denote by ${\mathbf{t}}^{\boldsymbol{\phi}}\left(\varphi \right)$ the minimal possible value of the number of proof steps for all proofs of the tautology $\varphi$ in the system $\phi$ .

Definition 3. The proof system $\phi$ is called $t$ -monotonous if for every tautology $\psi$ there is a minimal tautology $\varphi$ , such that $\varphi \in M\left(\psi \right)$ and ${\boldsymbol{t}}^{\boldsymbol{\phi}}\left(\psi \right) = {\boldsymbol{t}}^{\boldsymbol{\phi}}\left(\varphi \right)$ .

Definition 4. The proof system $\phi$ is called $t$ -strongly monotonous if for every tautology $\psi$ there is no minimal tautology $\varphi$ , such that $\varphi \in M\left(\psi \right)$ and ${\boldsymbol{t}}^{\boldsymbol{\phi}}\left(\varphi \right)>{\boldsymbol{t}}^{\boldsymbol{\phi}}\left(\psi \right)$ .

Theorem. The Frege systems, the sequent systems with cut rule, and the systems of natural deductions of classical, intuitionistic, and Johansson’s logics are not $t$ -monotonous, and consequently, are not $t$ -strongly monotonous.

Proof is given by showing that for these systems there are sequences of tautologies ${\psi}_n$ , every one of which has unique minimal tautologies ${\varphi}_n$ such that for each n the minimal proof lines of ${\varphi}_n$ are an order more than the minimal proof lines of ${\psi}_n$ .

[1] S. A. Cook and R. A. Reckhow, The relative efficiency of propositional proof systems. Journal of Symbolic Logic , vol. 44 (1979), no. 1, pp. 36–50.

[2] A. A. Hambardzumyan, Investigation of monotonous properties for Frege systems. Mathematical Problems of Computer Science , vol. 53 (2020), pp. 14–20.

[3] G. Mints and A. Kozhevnikov, Intuitionistic Frege systems are polynomially equivalent. Zapiskinauchnykhseminarov POMI , vol. 316 (2004), pp. 129–146.

▸ GABRIEL CIOBANU, Various notions of infinity for finitely supported structures.

Romanian Academy, Institute of Computer Science, Iaşi, Romania.

E-mail: gabriel@info.uaic.ro.

URL Address: https://profs.info.uaic.ro/~gabriel.

Finitely supported structures are related to permutation models of Zermelo–Fraenkel set theory with atoms. For such structures we focus only on a finite subset (its “finite support”) which can characterize the entire structure. More exactly, they are sets equipped with actions of the group of all permutations of a fixed (infinite) set $A$ of atoms satisfying a certain finite support requirement; this requirement states that any element of such a set is left unchanged under the effect of each permutation of $A$ that fixes pointwise finitely many atoms.

There exist several notions of infinity for finitely supported structures: Tarski infinity, Dedekind infinity, Mostowski infinity, etc. These notions are defined and studied, and several relationships between them are given. There are emphasized the similarities and differences between these new definitions of infinity for finitely supported structures. By presenting examples of finitely supported sets that satisfy a certain forms of infinity, while they do not satisfy other forms of infinity, we show that these notions of infinity are pairwise non-equivalent.

Examples of some finitely supported sets satisfying various forms of infinity (Tarski I, Tarski III, Dedekind, Mostowski, Ascending, Tarski II, and Non-Amorphous infinity) are presented shortly in the table below, where $\mathrm{\mathbb{N}}$ is the set of natural numbers, ${\wp}_{\mathrm{fin}}(X)$ is the finite powerset of $X$ , ${\wp}_{\mathrm{fs}}(X)$ is the set of all finitely supported subsets of $X$ , ${T}_{\mathrm{fin}}(A)$ is the set of all finite and injective tuples of elements from $A$ , and ${Y}_{\mathrm{fs}}^X$ is the set of all finitely supported functions from $X$ to $Y$ .

More details are available in the recent book Foundations of Finitely Supported Structures: A Set Theoretical Viewpoint available at the URL Address: https://www.springer.com/gp/book/9783030529611.

▸ VITTORIO CIPRIANI, Cantor–Bendixson theorem in the Weihrauch lattice.

Dipartimento di informatica, scienze matematiche e fisiche, Università degli studi di Udine, Via delle Scienze 206, Udine (UD), Italy.

E-mail: cipriani.vittorio@spes.uniud.it.

In this talk, we continue the program initiated in [5] aiming to study theorems occurring at the high levels of reverse mathematics (see [8]). Recently there has been a growing interest in this topic by many authors (see, for example, [1–3, 6] and a recent survey with some open problems concerning also this specific area [7]). We first present some results at the level of ${\mathsf{ATR}}_0$ , showing that (a variant of) the perfect tree theorem (in [5] denoted with ${\mathsf{PTT}}_1$ ) is strictly stronger than its version for closed sets, showing a difference with respect to the reverse mathematics setting where the two principles are equivalent. On the other hand, if one considers arithmetical Weihrauch reducibility (see [1, 2]) the two principles are equivalent.

We then move our attention to natural counterparts of the highest subsystem in the big five in reverse mathematics, namely ${\Pi}_1^1\hbox{-} {\mathsf{CA}}_0$ . The natural function representing ${\Pi}_1^1\hbox{-} {\mathsf{CA}}_0$ is the one that maps a countable sequence of trees to the characteristic function of the set of indices corresponding to well-founded trees. Recently in [4], Hirst showed its Weihrauch equivalence with $\mathsf{PK}$ , the function that takes as input a tree and outputs its perfect kernel. We will show that $\mathsf{PK}$ , as defined in [4], is strictly stronger than the version for closed sets, even if, as for the perfect tree theorem, they are arithmetically equivalent. Our analysis then moves to multivalued functions representing variations of the Cantor–Bendixson theorem, that, given in input a closed set output its perfect kernel plus a listing of the points in the scattered part. We will show that (variations of) the Cantor–Bendixson theorem for trees are as strong as the perfect kernel theorem (for trees). The same holds for closed sets with the only exception regarding a version of the Cantor–Bendixson in Baire space.

This is joint work with Alberto Marcone and Manlio Valenti.

[1] P.-E. Angls d’Auriac and T. Kihara, A comparison of various analytic choice principles, preprint, 2019, arXiv:1907.02769.

[2] J. Le Goh, Some computability-theoretic reductions between principles around ${\mathsf{ATR}}_0$ , preprint, 2019, arXiv:1905.06868.

[3] J. Le Goh, A. Pauly, and M. Valenti, Finding descending sequences through ill-founded linear orders. Journal of Symbolic Logic , vol. 86 (2021), no. 2, pp. 817–854.

[4] J. L. Hirst, Leaf management. Computability , vol. 9 (2020), nos. 3–4, pp. 309–314.

[5] T. Kihara, A. Marcone, and A. Pauly, Searching for an analogue of ${\mathsf{ATR}}_0$ in the Weihrauch lattice. Journal of Symbolic Logic , vol. 85 (2020), no. 3, pp. 1006–1043.

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

[7] A. Pauly, An update on Weihrauch complexity, and some open questions, preprint, 2020, arXiv:2008.11168.

[8] S. G. Simpson, Subsystems of Second Order Arithmetic , Perspectives in Logic, second ed., Cambridge University Press, Cambridge, 2009.

▸ WILLEM CONRADIE AND VALENTIN GORANKO, Algorithmic correspondence for relevance logics.

School of Mathematics, University of the Witwatersrand, 1 Jan Smuts Avenue, Johannesburg, South Africa.

E-mail: willem.conradie@wits.ac.za.

Department of Philosophy, Stockholm University, Stockholm, Sweden.

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

This work brings together two important areas of active development in non-classical logics, viz. relevance logics and algorithmic correspondence theory.

The classical correspondence theory of modal logic was developed in the 1970s by van Benthem, Sahlqvist, and others, to establish first-order definability and completeness via canonicity for a wide syntactically defined class of modal axioms, commonly referred to as Sahlqvist—van Benthem formulae. These were later generalised to a range of logics with non-classical propositional base in the works of Gehrke, Venema, Nagahasi, Celani, Jansana, and others. Algorithmic correspondence theory, first developed in [2], transcends the syntactic approach of the classical correspondence theory by developing algorithmic procedures for computing first-order equivalents and proving canonicity of a considerably wider class of input formulae, including all inductive formulae [4]. The first such algorithmic procedure, developed for normal modal logics, was $\mathsf{SQEMA}$ [2], later generalised to $\mathsf{ALBA}$ [3] for logic algebraically captured by classes of normal lattice expansions.

In this work, reported in [1], we develop a variation of $\mathsf{ALBA}$ for formulae of relevance logics with semantics over Routley–Meyer frames.The resulting algorithmic procedure $\mathsf{PEARL}$ computes first-order correspondents with respect to validity in Routley–Meyer frames. It succeeds, inter alia, on a large class of inductive relevance formulas, including almost all axioms for important relevance logics known from the literature and it is currently under implementation.

[1] W. Conradie and V. Goranko, Algorithmic correspondence for relevance logics I. The algorithm PEARL, Alasdair Urquhart on Nonclassical and Algebraic Logic and Complexity of Proofs (I. Düntsch and E. Mares, editors), Springer, Cham, 2021, pp. 163–209.

[2] W. Conradie, V. Goranko, and D. Vakarelov, Algorithmic correspondence and completeness in modal logic. I. The core algorithm SQEMA. Logical Methods in Computer Science , vol. 2 (2006), no. 1, pp. 1–26.

[3] W. Conradie and A. Palmigiano, Algorithmic correspondence and canonicity for non-distributive logics. Annals of Pure and Applied Logic , vol. 170 (2019), no. 9, pp. 923–974.

[4] V. Goranko and D. Vakarelov, Elementary canonical formulae: Extending Sahlqvist’s theorem. Annals of Pure and Applied Logic , vol. 141 (2006), nos. 1–2, pp. 180–217.

▸ A. CORDÓN–FRANCO, F. F. LARA–MARTÍN, AND MANUEL J. S. LOUREIRO, On determinacy of Lipschitz and Wadge games in second order arithmetic.

Department of Computer Science and Artificial Intelligence, Universidad de Sevilla, Facultad de Matemáticas, C/ Tarfia s/n, Sevilla, Spain.

E-mail: acordon@us.es.

Universidad de Sevilla, Seville, Spain.

E-mail: fflara@us.es.

Faculty of Engineering, Lusofona University, Lisbon, Portugal.

E-mail: mloureiro@ulusofona.pt.

We present a detailed formalization of Lipschitz and Wadge games in the context of second order arithmetic (SOA) and we investigate the logical strength of Lipschitz and Wadge determinacy, and the tightly related Semi-Linear Ordering principle. We show that the topological analysis of the complete sets in Hausdorff difference hierarchy (with respect to Wadge reducibility) developed in [2] can be adapted to prove the determinacy of these games in SOA. As a result, we extend the work developed in [1] and characterize the basic systems from Reverse Mathematics ${\mathsf{WKL}}_0$ , ${\mathsf{ACA}}_0$ , and ${\mathsf{ATR}}_0$ in terms of these determinacy principles.

Given two formula classes ${\Gamma}_1$ and ${\Gamma}_2$ in the language of SOA, let $\left({\Gamma}_1,{\Gamma}_2\right)$ - ${\mathsf{Det}}_L$ denote the principle of determinacy for Lipschitz games in the Baire space where player I’s pay-off set is ${\Gamma}_1$ -definable and player II’s pay-off set is ${\Gamma}_2$ -definable. A similar principle for Wadge games is introduced and denoted by $\left({\Gamma}_1,{\Gamma}_2\right)$ - ${\mathsf{Det}}_W$ . Likewise, let $\left({\Gamma}_1,{\Gamma}_2\right)$ - ${\mathsf{SLO}}_{L/W}$ denote the corresponding semi-linear ordering principles. If ${\Gamma}_1 = {\Gamma}_2 = \Gamma$ then we simply write $\Gamma$ - ${\mathrm{Det}}_{L/W}$ or $\Gamma$ - ${\mathsf{SLO}}_{L/W}$ and, when restricting ourselves to games in the Cantor space the corresponding principles are denoted by ${\mathsf{Det}}^{\ast }$ and ${\mathsf{SLO}}^{\ast }$ . Regarding games in the Cantor space we prove that:

1. 1. Over ${\mathsf{RCA}}_0$ , ${\Delta}_1^0$ - ${\mathsf{Det}}_L^{\ast }$ and ${\mathsf{WKL}}_0$ are equivalent.

2. 2. Over ${\mathsf{RCA}}_0$ , ${\Sigma}_1^0$ - ${\mathsf{Det}}_L^{\ast }$ , $\left({\Sigma}_1^0,{\Sigma}_1^0\wedge {\Pi}_1^0\right)$ - ${\mathsf{SLO}}_{L/W}^{\ast }$ , and ${\mathsf{ACA}}_0$ are pairwise equivalent.

3. 3. Over ${\mathsf{WKL}}_0$ , ${\Sigma}_1^0$ - ${\mathsf{Det}}_W^{\ast }$ , ${\Sigma}_1^0$ - ${\mathsf{SLO}}_{L/W}^{\ast }$ , and ${\mathsf{ACA}}_0$ are pairwise equivalent.

4. 4. Over ${\mathsf{RCA}}_0$ , ${\Delta}_2^0$ - ${\mathsf{Det}}_L^{\ast }$ and ${\mathsf{ATR}}_0$ are equivalent.

As for games in the Baire space we prove that:

1. 1. Over ${\mathsf{RCA}}_0$ , $\left({\Delta}_1^0,{\Pi}_1^0\right)$ - ${\mathsf{Det}}_L$ , ${\Pi}_1^0$ - ${\mathsf{Det}}_L$ , and ${\mathsf{ATR}}_0$ are pairwise equivalent.

2. 2. Over ${\mathsf{ACA}}_0$ , ${\Delta}_1^0$ - ${\mathsf{Det}}_L$ , ${\Delta}_1^0$ - ${\mathsf{SLO}}_L$ , and ${\mathsf{ATR}}_0$ are pairwise equivalent.

3. 3. ${\Pi}_1^1$ - ${\mathsf{CA}}_0$ proves $\left({\Sigma}_1^0\wedge {\Pi}_1^0\right)$ - ${\mathsf{Det}}_{L/W}\!.$

(Work partially supported by grant MTM2017-86777-P, Ministerio de Economía, Industria y Competitividad, Spanish Government)

[1] M. J. S. Loureiro, Semilinear order property and infinite games , Ph.D. thesis, University of Seville, Spain, 2016.

[2] W. W. Wadge, Reducibility and determinateness on the Baire space , Ph.D. thesis, University of California, Berkeley, 1983.

▸ INÉS CRESPO AND ALBA MASSOLO, Arguments against a Bayesian approach to the normativity of argumentation.

New York University Paris, 57 Boulevard Saint-Germain, 75005 Paris, France.

E-mail: inescrespo@gmail.com.

Universidad Nacional de Córdoba, CIFFyH, Pabellón Agustín Tosco, Ciudad Universitaria, X5000, Córdoba, Argentina.

E-mail: albamassolo@gmail.com.

Corner and Hahn [3] argue in favor of a Bayesian grounding of normative standards for rational argumentation. We wish to take issue with this strategy, attacking two different angles.

Corner and Hahn find support in [4], but this sort of study presupposes logical monism, while in the past decades logical pluralism has become a strong position in the philosophy of logic [1, 2]. Assuming a contextual logical pluralism, we argue in favor of an externalist characterization of the normativity of logic, where practices themselves are to be seen as sources of normative standards for rational argumentation. Besides, Corner and Hahn’s endorsement of a Bayesian account assumes that rational argumentation is only, or mostly, evidence-based reasoning. However, this model seems inadequate if one considers different contexts of argumentative practices, such as the case for mathematics.

Corner and Hahn claim that intuitions about argument strength, or logical validity, match the adequacy of Bayesian formalization as providing normative standards for rational argumentation. However, this match doesn’t show whether those intuitions play any role as normative standards. Furthermore, one should wonder whether anyone’s intuitions count. Resnik [5] claims that only expert’s intuitions count when it comes to fixing the reflective equilibrium issued by inferential practices. By contrast, we argue that one can see normative standards be issued, not by individual’s intuitions, but rather by the argumentative practices which take place within different communities.

[1] J. C. Beall and G. Restall, Logical Pluralism , Oxford University Press, Oxford, 2006.

[2] C. Caret, Why logical pluralism? Synthese , vol. 198 (2019), no. 20, pp. 4947–4968.

[3] A. Corner and U. Hahn, Normative theories of argumentation: Are some norms better than others? Synthese , vol. 190 (2013), no. 16, pp. 3579–3510.

[4] M. Oaksford and N. Chater, A rational analysis of the selection task as optimal data selection. Psychological Review , vol. 1 (1994), pp. 608–631.

[5] M. Resnik, Logic: Normative or descriptive? The ethics of belief or a branch of psychology? Philosophy of Science , vol. 52 (1985), no. 2, pp. 221–238.

▸ VINCENZO CRUPI, ANDREA IACONA, AND ERIC RAIDL, The logic of the evidential conditional.

Department of Philosophy and Education, Center for Logic, Language and Cognition, University of Turin, Via S. Ottavio 20, 10124 Torino, Italy.

E-mail: vincenzo.crupi@unito.it.

E-mail: andrea.iacona@unito.it.

Cluster of Excellence “Machine Learning: New Perspectives for Science”, University of Tübingen, Maria von Lindenstrasse 6, 72076 Tübingen, Germany.

E-mail: eric.raidl@uni-tuebingen.de.

In a recent work, Crupi and Iacona [1] have suggested an account of conditionals—the evidential account—which rests on the idea that a conditional is true just in case its antecedent supports its consequent. The idea that $A$ supports $C$ is spelled out in terms of two conditions. One is the Ramsey Test as understood by Stalnaker and Lewis: in the closest possible worlds in which $A$ is true, $C$ must be true as well. The other is the Reverse Ramsey Test: in the closest possible worlds in which $C$ is false, $A$ must be false as well. They call Chrysippus Test the conjunction of the Ramsey Test and the Reverse Ramsey Test.

The paper implements the Chrysippus test in a possible world semantic and presents a system of conditional logic which we show to be sound and complete for the evidential account. The proof adapts a general method elaborated by Raidl [2]. For this, the following insights are used: the evidential conditional can be defined from a known Lewisean conditional as a conjunctive strengthening of the latter. Conversely, and less obviously, the Lewisean conditional is back-definable from the evidential conditional. This is expressed by a translation between the languages of the two conditionals. It is this bridge which allows transferring results from the known Lewisean conditional to the defined conditional, as we show in [3]. We discuss the laws of the new logic for the evidential conditional, as well as some derived laws, including disjunctive rationality and some connexive principles.

[1] V. Crupi and A. Iacona, The evidential conditional. Erkenntnis (2021). https://doi.org/10.1007/s10670-020-00332-2.

[2] E. Raidl, Definable conditionals. Topoi , vol. 40 (2021), pp. 87–105.

[3] E. Raidl, A. Iacona, and V. Crupi, The logic of the evidential conditional. Review of Symbolic Logic (2021), pp. 1–13. https://doi.org/10.1017/S1755020321000071.

▸ AIGERIM DAULETIYAROVA AND VIKTOR VERBOVSKIY, On local monotonicity of unary functions definable in o-stable ordered groups.

Sobolev Institute of Mathematics, 4 Akademika Koptyug Aveneue, 630090 Novosibirsk, Russia.

E-mail: d\_aigera95@mail.ru.

Satbayev University, 22a Satpaev Street, 050013 Almaty, Kazakhstan.

E-mail: viktor.verbovskiy@gmail.com.

Let $\mathrm{\mathcal{M}} = \left(M,<,\dots \right)$ be a totally ordered structure. A partition $\left\langle C,D\right\rangle$ of $M$ is called a cut if $C<D$ . Given a cut $\left\langle C,D\right\rangle$ one can construct a partial type $\left\{c<x<d:c\in C,d\in D\right\}$ , which we also call a cut and use the same notation $\left\langle C,D\right\rangle$ . A cut $\left\langle C,D\right\rangle$ in an ordered group is called non-valuational [2] if $d-c$ converges to $0$ whenever $c$ and $d$ converge to $\mathrm {sup} C$ and $\operatorname{inf}D$ accordingly. An ordered group $G$ is said to be of non-valuational type, if there is no definable non-trivial convex subgroup in $G$ .

Definition 1 [1].

1) An ordered structure $\mathrm{\mathcal{M}}$ is o-stable in $\lambda$ if for any $A\subseteq M$ with $\mid A\mid \le \lambda$ and for any cut $\left\langle C,D\right\rangle$ in $\mathrm{\mathcal{M}}$ there are at most $\lambda$ 1-types over $A$ which are consistent with the cut $\left\langle C,D\right\rangle$ .

2) A theory $T$ is o-stable in $\lambda$ if every model of $T$ is. A theory $T$ is o-stable if there exists an infinite cardinal $\lambda$ in which $T$ is o-stable.

Here we study o-stable ordered groups, and the initial study of them was in [3, 4].

Theorem 2. Any unary function that is definable in an o-stable ordered group of non-valuational type is piecewise continuous and monotone (note that pieces need not be convex).

This work was partially supported by the grant AP09259295 of SC of the MES of RK.

[1] B. Baizhanov and V. Verbovskii, O-stable theories. Algebra and Logic , vol. 50 (2011), no. 3, pp. 211–225.

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

[3] V. V. Verbovskiy, O-stable ordered groups. Siberian Advances in Mathematics , vol. 22 (2012), no. 1, pp. 50–74.

[4] _____, On ordered groups of Morley o-rank 1. Siberian Electronic Mathematical Reports , vol. 15 (2018), no. 1, pp. 314–320.

▸ MATTEO DE CEGLIE, The $V$ -logic multiverse and MAXIMIZE.

Philosophy Department (KGW), Salzburg University, Franziskanergasse, 1, Salzburg, Österreich.

E-mail: decegliematteo@gmail.com.

I argue that classical set theory, $ZFC\!\left(+ LCs\right)$ , is restrictive compared to the $V$ -logic multiverse (a novel set theoretic multiverse developed by the author and Claudio Ternullo). This multiverse is based upon Friedman’s Hyperuniverse and Steel’s set-generic multiverse: like the Hyperuniverse, it uses the infinitary $V$ -logic as background logic (this logic admits formulas of length less than the first successor of the least inaccessible cardinal, but only a finite block of quantifiers in front of them) and admits all kinds of outer models of $V$ (produced by set-generic, class-generic, and hyperclass forcing). Like Steel’s set-generic multiverse, it is recursively axiomatisable and is rooted on a ground universe that satisfies $\mathsf{ZFC}$ . For this proof, I compare $\mathsf{ZFC}+\mathsf{LCs}$ and the $V$ -logic multiverse, characterised as $\mathrm{ZFC}+\mathrm{LCs}+$ the Multiverse Axiom Schema (this axiom tells us that if a sentence $\varphi$ is consistence in $V$ -logic then there is an actual outer model of $V$ satisfying it), following Maddy’s methodological principle MAXIMIZE (introduced in [3]). According to this principle, when comparing two foundational theories we should prefer the one that can prove more isomorphism types. I claim that the $V$ -logic multiverse, as opposed to $\mathrm{ZFC}+\mathrm{LCs}$ , does exactly that. This is because in the $V$ -logic multiverse theory we can prove the existence of proper, uncountable, extensions of $V$ , that we cannot have in $\mathrm{ZFC}+\mathrm{LCs}$ (see [2]). In turn, these extra objects means we can realise more isomorphism types that are not available in $\mathrm{ZFC}+\mathrm{LCs}$ , since in the $V$ -logic multiverse we can prove the existence of iterable class sharps and, more importantly, maps between them (see [1]). Moreover, when moving from $\mathrm{ZFC}+\mathrm{LCs}$ to the $V$ -logic Multiverse we are not losing anything: $\mathrm{ZFC}$ , all the large cardinals, inner models, and $V$ are still there. On the other hand, when moving from the $V$ -logic multiverse to $\mathrm{ZFC}+\mathrm{LCs}$ we lose the actual outer models of $V$ , iterable class sharps, and iterable class sharp generated models. Thus, this latter theory is restrictive compared to the $V$ -logic multiverse theory.

[1] C. Antos, N. Barton, and Sy-D. Friedman, Universism and extensions of $V\!,$ Review of Symbolic Logic , vol. 14 (2021), no. 1, pp. 112–154.

[2] N. Barton, Forcing and the universe of sets: Must we lose insight? Journal of Philosophical Logic , vol. 49 (2020), no. 4, pp. 575–612.

[3] P. Maddy, Naturalism in Mathematics , Oxford University Press, Oxford, 1998.

▸ SAMUEL G. DA SILVA AND VALERIA DE PAIVA, Dialectica and Kolmogorov–Veloso problems.

Departamento de Matemática, Universidade Federal da Bahia, Salvador, Brazil.

E-mail: samuel@ufba.br.

Topos Institute, Berkeley, CA, USA.

E-mail: valeria@topos.institute.

Blass’ paper on questions and answers makes a surprising connection between Dialectica categories (models of Linear Logic), Vojtas’ methods to prove inequalities between cardinal characteristics of the continuum (Set Theory), and complexity theoretical notions of problems (and reductions) between these. We recently realized that Kolmogorov’s very abstract notion of problem, which is not related to specific complexity issues, can also be intrinsically related to Blass’ examples above. Kolmogorov’s notion of abstract problem produces an alternative intuitive semantics for Propositional Intuitionistic Logic, an essential component of the celebrated Brouwer–Heyting–Kolmogorov (BHK) interpretation. We connect Kolmogorov’s problems to objects of the Dialectica construction, thereby connecting also Veloso’s problems. More importantly, we show how category theory gives us a better approach to Kolmogorov’s problems, providing the morphisms that Kolmogorov lacked in 1932. Time allowing, we will discuss possible applications of these problems to multi-agent systems in Artificial Intelligence.

▸ VALERIA DE PAIVA, LUIZ CARLOS PEREIRA, AND ELAINE PIMENTEL, Ecumenic negation: one or two?.

Topos Institute, Berkeley, CA, USA.

E-mail: valeria@topos.institute.

Departamento de Filosofia, Pontifical Catholic University of Rio de Janeiro, Rio de Janeiro, Brazil.

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

Departamento of Matemática, Universidade Federal do Rio Grande do Norte, Natal, Brazil.

E-mail: elaine.pimentel@gmail.com.

Prawitz proposed an ecumenical system where classical logic and intuitionist logic co-exist harmoniously. Previous work on this Ecumenical Logic system has provided a Gentzen Natural Deduction formalization as well as a Gentzen sequent calculus formulation with the expected properties of normalization and cut-elimination. In these formulations Intuitionistic Propositional Logic and Classical Propositional logic, traditionally considered rival logics, accept and reject the same theorems. The ecumenical system as described has two disjunctions and two implications (one classical and one intuitionistic), but only one conjunction, one negation, and one constant for falsum. Given that usually negation is defined as implication into falsum, it would seem reasonable to expect two negations, one the intuitionistic implication into falsum, the other a classical implication into falsum. However it is easy to prove that these two possible negations are interderivable in the Ecumenical system. Is this a sufficient criterium to decide on a single negation? This paper presents two arguments to defend the thesis that in fact there is only one way to assert the negation of a proposition $A$ . The first argument is based on Glivenko’s theorems and the second on the notion of “computational isomorphism.” We discuss these arguments, as well as the failure of Joyal’s collapse in minimal logic, as subsidies for a robust notion of ecumenical negation.

▸ DMITRY EMELYANOV, BEIBUT KULPESHOV, AND SERGEY SUDOPLATOV, On algebras of binary formulas for partially ordered theories.

Novosibirsk State Technical University, Novosibirsk, Russia.

E-mail: dima-pavlyk@mail.ru.

Kazakh-British Technical University, Almaty, Kazakhstan.

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

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

Novosibirsk State University, Novosibirsk, Russia.

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

We consider a generalization, for partially ordered theories, of descriptions for algebras of binary isolating formulas [4] for a series of linearly ordered theories [1–3], based on dense lower semilattices with Ehrenfeucht theories [5, Example 1.1.1.4].

Using Cayley tables for countably categorical weakly o-minimal theories [1] and quite $o$ -minimal theories we explicitly define the classes of commutative monoids ${\mathfrak{A}}_n$ , respectively, ${\mathfrak{A}}_n^{\mathrm{QR}}$ , ${\mathfrak{A}}_n^{\mathrm{QL}}$ , ${\mathfrak{A}}_n^I$ , of isolating formulas for isolated, respectively, quasirational to the right, quasirational to the left, irrational, $1$ -types $p$ of quite $o$ -minimal partially ordered theories with few countable models, with convexity rank $\mathrm{RC}(p) = n$ . For an algebra ${\mathfrak{P}}_{\nu (p)}$ of binary isolating formulas of $1$ -type $p$ , we have:

Theorem 1. Let $T$ be a quite $o$ -minimal partially ordered theory with few countable models, $p\in {S}_1\!\left(\varnothing \right)$ be a non-algebraic type. Then there exists $n<\omega$ such that:

1. (1) if $p$ is isolated then ${\mathfrak{P}}_{\nu (p)}\simeq {\mathfrak{A}}_n$ ;

2. (2) if $p$ is quasirational to the right (left) then ${\mathfrak{P}}_{\nu (p)}\simeq {\mathfrak{A}}_n^{\mathrm{QR}}$ ( ${\mathfrak{P}}_{\nu (p)}\simeq {\mathfrak{A}}_n^{\mathrm{QL}}$ );

3. (3) if $p$ is irrational then ${\mathfrak{P}}_{\nu (p)}\simeq {\mathfrak{A}}_n^I$ .

Corollary 2. Let $T$ be a quite $o$ -minimal partially ordered theory with few countable models, $p,q\in {S}_1\!\left(\varnothing \right)$ be non-algebraic types. Then ${\mathfrak{P}}_{\nu (p)}\simeq {\mathfrak{P}}_{\nu (q)}$ if and only if $\mathrm{RC}(p) = \mathrm{RC}(q)$ and the types $p$ and $q$ are simultaneously either isolated, or quasirational, or irrational.

This research has been funded by RFBR (project No. 20-31-90004), by KN MON RK (Grant No. AP08855544), and by SB RAS (project No. 0314-2019-0002).

[1] D. Yu. Emelyanov, B. Sh. Kulpeshov, and S. V. Sudoplatov, Algebras of distributions for binary formulas in countably categorical weakly o-minimal structures. Algebra and Logic , vol. 56 (2017), no. 1, pp. 13–36.

[2] D. Yu. Emelyanov, B. Sh. Kulpeshov, and S. V. Sudoplatov, On algebras of distributions for binary formulas for quite o-minimal theories. Algebra and Logic , vol. 57 (2019), no. 6, pp. 429–444.

[3] _____, Algebras of binary formulas for compositions of theories. Algebra and Logic , vol. 59 (2020), no. 4, pp. 295–312.

[4] 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.

[5] S. V. Sudoplatov, Classification of Countable Models of Complete Theories , Novosibirsk State Technical University, Novosibirsk, 2018.

▸ MARTA FIORI CARONES, Measuring the strength of Ramsey-theoretic statements over ${\mathsf{RCA}}_0^{\ast }$ .

Institute of Mathematics, University of Warsaw, Banacha 2, 02-097 Warszawa, Poland.

E-mail: marta.fioricarones@outlook.it.

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

(Joint work with Leszek Kołodziejczyk and Katarzyna W. Kowalik)

The common base theory of reverse mathematics is the theory ${\mathsf{RCA}}_0$ , which guarantees the existence of ${\Delta}_1^0$ -definable sets and where mathematical induction for ${\Sigma}_1^0$ -formulae holds. In 1986, Simpson and Smith introduced a different base theory, ${\mathsf{RCA}}_0^{\ast }$ , where induction is weakened to ${\Delta}_1^0$ -formulae. In more recent years Kołodziejczyk, Kowalik, Wong, and Yokoyama started wondering about the strength of Ramsey’s theorem over ${\mathsf{RCA}}_0^{\ast }$ . In this talk we concentrate on three well-known consequences of Ramsey’s theorem for pairs, namely the Ascending Descending Sequence principle $\mathsf{ADS}$ , the Chain/Antichain principle $\mathsf{CAC}$ , and the Cohesive Ramsey theorem for pairs ${\mathsf{CRT}}_2^2$ . We measure the relative strength of these statements in three ways: (1) implications or non-implications among them over ${\mathsf{RCA}}_0^{\ast }$ (and over ${\mathsf{RCA}}_0^{\ast }$ plus negated ${\Sigma}_1^0$ -induction), (2) conservativity over ${\mathsf{RCA}}_0^{\ast }$ , and (3) provable closure properties of the intersection of all ${\Sigma}_1^0$ -cuts. For example, we show that with respect to the last criterion, ${\mathsf{RT}}_2^2$ is stronger than both $\mathsf{CAC}$ and $\mathsf{ADS}$ , while these two are indistinguishable, and it is still open whether ${\mathsf{CRT}}_2^2$ resembles ${\mathsf{RT}}_2^2$ or $\mathsf{CAC}$ / $\mathsf{ADS}$ .

▸ ANDREY FROLOV AND MAXIM ZUBKOV, Spectral universality of linear orders with one binary relation.

Innopolis University, 1, Universitetskaya Street, Innopolis, Russia.

E-mail: a.frolov.kpfu@gmail.com.

N. I. Lobachevsky Institute of Mathematics and Mechanics, Kazan Federal University, Kremlevskaya 18, Kazan, Russia.

E-mail: maxim.zubkov@kpfu.ru.

The set of Turing degrees relative to which a given algebraic structure $\mathcal{A}$ is computably representable is called the degree spectrum of this structure and is denoted by $\mathrm{dgSp}\!\left(\mathcal{A}\right)$ . The question of describing the degree spectra of algebraic structures is one of the fundamental questions in the theory of computable structures and their models. Slinko, Hirschfeldt, Khusainov, and Shore [2] called a class of structures spectrally universal if any possible degree spectrum of an algebraic structure is realized by a degree spectrum of a structure from this class. They also established the spectral universality of a number of classical classes of algebraic structures, for example, classes such as undirected graphs, lattices, commutative semigroups, and others.

The class of countable linear orders is one of the most difficult in terms of describing the spectra of degrees of all representatives of this class. It is not spectrally universal. This follows, for example, from the fact that the spectrum of degrees of linear order, in contrast to graphs, can form an upper cone of degrees if and only if it contains a computable degree [3]. And it is still not known whether there is a linear order whose degree spectrum contains exactly all non-zero degrees.

Miller and Harizanova [1] proved the result of Richter for an arbitrary linear order with an additional unary predicate. Thus, the class of structures that are linear orders whose signature is enriched in a unary relation is not spectrally universal.

In this paper, we prove that the binary (and therefore $n$ -ary for any $n\ge 2$ ) relation on $\mathrm{\mathbb{Q}}$ (the natural ordering of the set of rational numbers) is spectrally universal. Namely, it is shown that for any graph there exists a binary relation on $\mathrm{\mathbb{Q}}$ , whose spectrum coincides with the spectrum of degrees of the graph.

The authors were supported by RFBR Grant No. 20-31-70012.

[1] V. Harizanov and R. Miller, Spectra of structures and relations. Journal of Symbolic Logic , vol. 72 (2007), no. 1, pp. 324–348.

[2] D. R. Hirschfeldt, B. Khoussainov, R. A. Shore, and A. M. Slinko, Degree spectra and computable dimensions in algebraic structures. Annals of Pure and Applied Logic , vol. 115 (2002), nos. 1–3, pp. 71–113.

[3] L. J. Richter, Degrees of structures. Journal of Symbolic Logic , vol. 46 (1981), no. 4, pp. 723–731.

▸ FRANCESCO GALLINARO, Around exponential algebraic closedness.

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

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

Zilber’s quasiminimality conjecture [2, 3] predicts that all subsets of the complex numbers that are definable using the language of rings and the exponential function are either countable or cocountable. Building on Zilber’s work, Bays and Kirby have proved in [1] that the quasiminimality conjecture would follow from the exponential algebraic closedness conjecture, also due to Zilber, which states that all systems of exponential polynomial equations which do not contradict Schanuel’s conjecture can be solved in the complex numbers. Similar questions, based on analogues of Schanuel’s conjecture, arise in the study of other analytic functions, such as the exponential maps of abelian varieties and the modular $j$ -function. The first part of this talk will focus on these conjectures and the interplay between them, while in the second part some results will be discussed, showing how to solve some classes of systems of equations which have a particularly nice geometry.

[1] M. Bays and J. Kirby, Pseudo-exponential maps, variants, and quasiminimality. Algebra & Number Theory , vol. 12 (2018), no. 3, pp. 493–549.

[2] B. Zilber, Analytic and pseudo-analytic structure, Logic Colloquium 2000, Paris (R. Cori, A. Razborov, S. Todorčević, and C. Wood, editors), “Lecture Notes in Logic, vol. 19,” Cambridge University Press, Cambridge, 2005, pp. 392–408.

[3] B. Zilber, Pseudo-exponentiation on algebraically closed fields. Annals of Pure and Applied Logic , vol. 132 (2005), no. 1, pp. 67–95.

▸ VALENTIN GORANKO AND RUAAN KELLERMAN, Approximating trees as coloured linear orders and complete axiomatisations of some classes of trees.

Department of Philosophy, Stockholm University, Universitetsvägen 10 D Frescati, SE-10691 Stockholm, Sweden.

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

Department of Mathematics and Applied Mathematics, University of Pretoria, Private Bag X20, Hatfield, South Africa.

E-mail: ruaan.kellerman@up.ac.za.

We study the first-order theories of some natural classes of coloured trees, including the four classes of trees whose paths have the order type, respectively, of the natural numbers, the integers, the rationals, and the reals. We develop a technique for approximating a tree as a suitably coloured linear order. We then present the first-order theories of certain classes of coloured linear orders and use them, along with the technique for approximating trees as coloured linear orders, and techniques borrowed from [1], to establish complete axiomatisations of the four classes of trees mentioned above. This talk is based on the work presented in [2].

[1] K. Doets, Monadic ${\Pi}_1^1$ -theories of ${\Pi}_1^1$ -properties. Notre Dame Journal of Formal Logic , vol. 30 (1989), no. 2, pp. 224–240.

[2] V. Goranko and R. Kellerman, Approximating trees as coloured linear orders and complete axiomatisations of some classes of trees. Journal for Symbolic Logic , vol. 86 (2021), no. 3, pp. 1035–1065.

▸ MATTIAS GRANBERG OLSSON AND GRAHAM LEIGH, A proof of conservativity of ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}$ over Heyting arithmetic via truth.

Department of Philosophy, Linguistics and Theory of Science, University of Gothenburg, P.O. Box 200, SE405 30 Göteborg, Sweden.

E-mail: mattias.granberg.olsson@gu.se.

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

We present work in progress on a novel proof of the conservativity of the intuitionistic fix-point theory ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}$ over Heyting arithmetic ( $\mathrm{HA}$ ), originally proved in full generality by Arai [1]. We make use of the work of van den Berg and van Slooten [2] on realizability in Heyting arithmetic over Beeson’s logic of partial terms ( $\mathrm{HAP}$ ). The proof is divided into four parts: First we extend the inclusion of $\mathrm{HA}$ into $\mathrm{HAP}$ to ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}$ into a similar theory ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}\mathrm{P}$ in the logic of partial terms. We then show that every theorem of this theory provably has a realizer in the theory ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}\mathrm{P}\left(\Lambda \right)$ of fix-points for almost negative operator forms only. Constructing a hierarchy stratifying the class of almost negative formulae and partial truth predicates for this hierarchy, we use Gödel’s diagonal lemma to show ${\widehat{\mathrm{ID}}}_1^{\mathrm{i}}\mathrm{P}\left(\Lambda \right)$ is interpretable in $\mathrm{HAP}$ . Finally we use the result of [2] that adding the schema of “self-realizability” for arithmetic formulae to $\mathrm{HAP}$ is conservative over $\mathrm{HA}$ .

[1] T. Arai, Quick cut-elimination for strictly positive cuts. Annals of Pure and Applied Logic , vol. 162 (2011), no. 10, pp. 807–815.

[2] B. van den Berg and L. van Slooten, Arithmetical conservation results. Indagationes Mathematicae , vol. 29 (2018), pp. 260–275.

▸ LEW GORDEEV AND EDWARD HERMANN HAEUSLER, On proof theory in computational complexity.

Informatik, Tübingen University, Sand 13, Tübingen, Germany.

E-mail: lew.gordeew@uni-tuebingen.de.

Informatics, Pontifical Catholic University of Rio de Janeiro, Rio de Janeiro, Brazil.

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

In [2] (see also [1, 3]) we presented full proof of the equalities NP = coNP = PSPACE. These results have been obtained by the novel proof theoretic tree-to-dag compressing techniques adapted to Prawitz’s [5] Natural Deduction (ND) for propositional minimal logic coupled with corresponding Hudelmaier’s sequent calculus [4]. Recall that conventional interpretation of ND assumes that derivations are rooted trees whose nodes are labeled with formulas that are ordered according to the inference rules allowed; top formulas and the root formula are called assumptions and conclusion, respectively. Proofs are derivations whose all assumptions are discharged [5]. We use more lliberal interpretation that allows dag-like derivations whose nodes are ordered as DAGs (: directed acyclic graphs), not necessarily trees. Obviously dag-like derivations can be exponentially smaller than corresponding tree-like ones (but note that our dag-like proofs require a special notion of correctness). We elaborated a method of twofold horizontal compression of arbitrary “huge” polynomial-height (though possibly exponential-weight) tree-like proofs $\partial$ into equivalent “small” polynomial-weight dag-like proofs ${\partial}_0$ containing only different formulas at every horizontal level, whose correctness is verifiable in polynomial time by a deterministic TM. First part of compression [1] is defined by plain deterministic recursion on the height that provides us with “small” polynomial-weight dag-like proofs in a modified ND that allows multiple-premise inferences. In the second part [2] we apply nondeterministic recursion to eliminate multiple premises and eventually arrive at “small” dag-like proofs ${\partial}_0$ in basic ND, as desired. As an application [3] we consider simple directed graphs $G$ and canonical “huge” tree-like exponential-weight(though polynomial-height) normal deductions (derivations) $\partial$ whose conclusions are valid iff $G$ have no Hamiltonian cycles. By the horizontal compression we obtain equivalent “small” polynomial-weight dag-like proofs ${\partial}_0$ and observe that the correctness of ${\partial}_0$ is verifiable in polynomial time by a deterministic TM. Since Hamiltonian Graph Problem is coNP-complete, the existence of such polynomial-weight proofs ${\partial}_0$ proves NP = coNP [2, 3]. Now consider problem NP =? PSPACE. We know [6, 7] that the validity problem in propositional minimal logic is PSPACE-complete. Moreover, minimal tautologies are provable in Hudelmaier’s cutfree sequent calculus by polynomial-height tree-like derivations $\partial$ . Standard translation into ND in question yields corresponding “huge” tree-like proofs ${\partial}^{\hbox{'}}$ that can be horizontally compressed into desired “small” dag-like polynomial-weight proofs ${\partial}_0$ whose correctness is deterministically verifiable in polynomial time. This yields NP = PSPACE [2].

[1] L. Gordeev and E. H. Haeusler, Proof compression and NP versus PSPACE. Studia Logica , vol. 107 (2019), no. 1, pp. 55–83.

[2] _____, Proof compression and NP versus PSPACE II. Bulletin of the Section of Logic , vol. 49 (2020), no. 3, pp. 213–230.

[3] _____, Proof compression and NP versus PSPACE II: Addendum. Bulletin of the Section of Logic , 9 pp. https://doi.org/10.18778/0138-0680.2022.01.

[4] J. Hudelmaier, An $O\!\left(n\log n\right)$ -space decision procedure for intuitionistic propositional logic. Journal of Logic and Computation , vol. 3 (1993), pp. 1–13.

[5] D. Prawitz, Natural Deduction: A Proof-Theoretical Study , Almqvist & Wiksell, Stockholm, 1965.

[6] R. Statman, Intuitionistic propositional logic is polynomial-space complete. Theoretical Computer Science , vol. 9 (1979), pp. 67–72.

[7] V. Ŝvejdar, On the polynomial-space completeness of intuitionistic propositional logic. Archive for Mathematical Logic , vol. 42 (2003), pp. 711–716.

▸ MARTINA IANNELLA, The complexity of convex bi-embeddability among countable linear orders.

Department of Mathematics, Computer Science and Physics, University of Udine, Via delle Scienze, 206, Udine, Italy.

E-mail: iannella.martina@spes.uniud.it.

Consider the set $\mathrm{LO}$ of countable linear orders and the following “convex embeddability” relation among them:

One easily gets that ${\trianglelefteq}_{\mathrm{LO}}$ is an analytic quasi-order on the Polish space $\mathrm{LO}$ . We first show that, in contrast to the usual embeddability between linear orders, the relation ${\trianglelefteq}_{\mathrm{LO}}$ is combinatorially complicated: it is not a well quasi-order, indeed it has both infinite descending chains and antichains of size the continuum.

Denote by $\underline{\bowtie}_{\mathrm{LO}}$ the equivalence relation on $\mathrm{LO}$ induced by ${\trianglelefteq}_{\mathrm{LO}}$ .

Theorem 1. (i) The isomorphism relation ${\cong}_{\mathrm{LO}}$ between linear orders is Borel reducible to $\underline{\bowtie}_{\mathrm{LO}}$ . In particular, $\underline{\bowtie}_{\mathrm{LO}}$ is a proper analytic equivalence relation.

(ii) There is a Baire measurable reduction from $\underline{\bowtie}_{\mathrm{LO}}$ to ${\cong}_{\mathrm{LO}}$ .

(iii) If $X$ is a turbulent Polish $G$ -space, then the equivalence relation induced by the group $G$ on $X$ is not Borel reducible to $\underline{\bowtie}_{\mathrm{LO}}$ .

In particular, $\underline{\bowtie}_{\mathrm{LO}}$ is not complete for analytic equivalence relations.

Finally, we define the “(finite) piecewise convex embeddability” on $\mathrm{LO}$ , denoted by ${\trianglelefteq}_{\mathrm{LO}}^{<\omega }$ : given $L,{L}^{\prime}\in \mathrm{LO}$ , we write $L{\trianglelefteq}_{\mathrm{LO}}^{<\omega }{L}^{\prime }$ if $L$ is the sum of $k$ disjoint convex subsets ${L}_i\subseteq L$ , with $i = 0,\dots, k<\omega$ , such that each ${L}_i{\trianglelefteq}_{\mathrm{LO}}{L}^{\prime }$ via some map ${f}_i$ , and the ${f}_i\left({L}_i\right)$ ’s are pairwise disjoint in ${L}^{\prime }$ and ordered by ${<}_{L^{\prime }}$ . We consider its associated equivalence relation $\underline{\bowtie}_{\mathrm{LO}}^{<\omega }$ , and show the following result.

Theorem 2. ${E}_1{\le}_B\underline{\bowtie}_{\mathrm{LO}}^{<\omega }$ .

As a corollary, we have that $\underline{\bowtie}_{\mathrm{LO}}^{<\omega }$ is not Baire reducible to any orbit equivalence relation, and by $(ii)$ of Theorem 1 it does not reduce to $\underline{\bowtie}_{\mathrm{LO}}$ .

This is joint work with Vadim Kulikov, Alberto Marcone, and Luca Motto Ros.

▸ AIGUL ISSAYEVA, NAZGUL SHAMATAYEVA, AND AIBAT YESHKEYEV, On atomic and algebraically prime definable subsets of semantic model.

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

E-mail: isa\_aiga@mail.ru.

E-mail: naz.kz85@mail.ru.

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

In the current abstract we are giving the result which connected with the different types of atomic and prime models in the frame of Jonsson theories investigations. In first time definable atomic and algebraically prime subsets of semantic model was defined in [2]. Such point of view is a refining of some questions which raised in [1], where relations between atomic and algebraically prime models was studied.

Let us give a necessary definitions.

Definition 1. 1) $\alpha$ -type is called any set of formulas consistent with $T$ , the free variables of which are found in ${\overline{x}}^{\alpha }$ ;

2) $\alpha$ -type $\rho$ is called $\Gamma$ - $\omega$ -type, if $\rho \subseteq \Gamma$ ;

3) $\Gamma$ - $\omega$ -type $\rho$ is called ${\Gamma}_1$ -principle type, if there exists such a sequence $\left\langle {\psi}_n\!\left({\overline{x}}^n\right):1\le n <\omega \right\rangle$ ${\Gamma}_1$ -formulas, such that:

a) $T\cup {\psi}_n\!\left({\overline{x}}^n\right)$ is consistent, $1\le n<\omega$ ;

b) ${\psi}_n\!\left({\overline{x}}^n\right)$ generates $\rho \upharpoonright {\overline{x}}^n$ , where $\rho \upharpoonright {\overline{x}}^n$ is set of formulas from $\rho$ , the free variables of which are among $\left({x}_1,\dots, {x}_n\right)$ , $1\le n<\omega$ ;

c) $T\vdash {\psi}_n\!\left({\overline{x}}^n\right)\leftrightarrow \exists {\overline{x}}^{n+1}{\psi}_{n+1}\left({\overline{x}}^{n+1}\right)$ , $1\le n<\omega$ .

Definition 2. A set ${A}_1$ is called fine almost weakly $\left({\Gamma}_1,{\Gamma}_2\right)$ - $\mathrm{cl}$ -atomic in the theory $T$ , if

1) every $\omega$ sequence of elements ${A}_1$ satisfied ${\Gamma}_1$ -principle type for ${\Gamma}_2$ - $\omega$ -type;

2) $\mathrm{cl}\left({A}_1\right) = {M}_1,{M}_1\in {E}_T$ , where ${E}_T$ is a class of all existentially closed models of the theory $T$ ;

and obtained model ${M}_1$ is said to be fine almost weakly $\left({\Gamma}_1,{\Gamma}_2\right)$ - $\mathrm{cl}$ -atomic model of the theory $T\!.$

Definition 3. A set ${A}_2$ is called a fine almost weakly $\left({\Gamma}_1,{\Gamma}_2\right)$ - $\mathrm{cl}$ -algebraically prime in the theory $T$ , if

1) ${A}_2$ is a fine almost weakly $\left({\Gamma}_1,{\Gamma}_2\right)$ - $\mathrm{cl}$ -atomic set of theory $T$ ;

2) $\mathrm{cl}\left({A}_2\right) = {M}_2,{M}_2\in {E}_T\cap {\mathrm{AP}}_T$ , where ${\mathrm{AP}}_T$ is a class of algebraically prime models the theory $T$ ;

and obtained model ${M}_2$ is called a fine almost weakly $\left({\Gamma}_1,{\Gamma}_2\right)$ - $\mathrm{cl}$ -algebraically prime model of the theory $T\!.$

And in the frame abovementioned notions one of the obtained results is the following theorem:

Theorem 4. Let $T$ be complete for $\exists$ -sentences perfect Jonsson theory and we have a fine almost weakly $\left({\Sigma}_1,{\Sigma}_1\right)$ - $\mathrm{cl}$ -atomic set of ${A}_1$ and a fine almost weakly $\left({\Sigma}_1,{\Sigma}_1\right)$ - $\mathrm{cl}$ algebraically prime set of ${A}_2$ . Then ${M}_1 = \mathrm{cl}\left({A}_1\right)$ isomorphic to ${M}_2 = \mathrm{cl}\left({A}_2\right)$ .

All additional information regarding Jonsson theories can be found in [3].

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

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

[2] A. R. Yeshkeyev, A. K. Issayeva, and N. M. Mussina, The atomic definable subsets of semantic model. Bulletin of the Karaganda University—Mathematics , vol. 2 (2019), no. 94, pp. 84–91.

[3] A. R. Yeshkeyev and M. T. Kassymetova, Jonsson theories and their classes of models , Monograph, KSU, 2016.

▸ JOSIAH JACOBSEN-GROCOTT, A characterization of the strongly n-representable many-one degrees.

University of Wisconsin–Madison, Madison, WI, USA.

E-mail: jacobsengroc@wisc.edu.

$\eta$ -representations are a way of coding sets in computable linear orders that were first introduced by Fellner in his thesis. Limitwise monotonic functions have been used to characterize the sets with $\eta$ -representations, and give characterizations for several variations of $\eta$ -representations. The one exception is the class of sets with strong $\eta$ -representations, the only class where the order type of the representation is unique.

We introduce the notion of a connected approximation of a set, a variation on ${\Sigma}_2^0$ approximations. We use connected approximations to give a characterization of the many-one degrees of sets with strong $\eta$ -representations as well new characterizations of the variations of $\eta$ -representations with known characterizations.

▸ MARCIN JUKIEWICZ DOROTA LESZCZYŃSKA-JASION, Genetic algorithms in proof-search tasks.

Department of Logic and Cognitive Science, Adam Mickiewicz University, Poznań, Poland.

E-mail: marcin.jukiewicz@amu.edu.pl.

E-mail: dorota.leszczynska@amu.edu.pl.

The aim of our work is an optimization of proof-search in a sequent system by a Genetic Algorithm (GA). In [1] we report on the satisfactory preliminary results: our GA provides derivation trees which are significantly shorter than trees built in a more standard manner. Moreover, a trend that shows up on the examined data is that the difference in the size of trees between the standard approach and GA grows exponentially with the size of tested formulas. Our solution had one weakness—as the complexity of sequents increased, the effectiveness in finding the correct proof decreased. The problem lies in too extensive search space that made it difficult for GA to find the correct proof. Therefore we focused on improving our previous solution and our goal was to reduce computations performed by GA. In the previous work, some repetitive patterns could be seen in most of the outlined derivation trees. Since these elements are repeatable, it is possible to include them in the tree-building algorithm. Then GA should select these elements that cannot be built into the algorithm, because they strongly depend on a formula.

[1] M. Jukiewicz, D. Leszczynska-Jasion, and A. Czyż, Genetic algorithms in proof-search tasks, submitted.

▸ MOHAMED KHALED, Algebras of concepts and their networks: Boolean algebras.

Faculty of Engineering and Natural Sciences, Bahçeşehir University, Istanbul, Turkey.

E-mail: mohamed.khalifa@eng.bau.edu.tr.

The network $\mathcal{N}$ of Boolean algebras is defined to be the graph whose vertices are all Boolean algebras, and which has two types of edges: red edges connecting the isomorphic algebras, and blue edges connecting two Boolean algebras if they are not isomorphic and one of them is a large subalgebra of the other one. A large subalgebra of an algebra $\mathfrak{B}$ is a proper subalgebra that needs only one extra element to generate the whole $\mathfrak{B}$ . With the aid of this network, we introduce a notion of distance that conceivably counts the minimum number of “dissimilarities” between two given Boolean algebras, with the possibility that this distance may take the value $\infty$ . See [1].

Viewing Boolean algebras as Lindenbaum–Tarski algebras of some propositional theories, this distance thus counts the minimum number of concepts that distinguish these theories from each other [1, 2]. A connected component of the network $\mathcal{N}$ is a maximal subclass of Boolean algebras with the property that the distance between any two of its members is finite. Thus, the distance between any member of a connected component and an algebra outside this component must be infinite. In this talk, we calculate distances between some special Boolean algebras and we give two interesting examples of connected components of the network $\mathcal{N}$ of Boolean algebras.

[1] M. Khaled and G. Székely, Algebras of concepts and their networks, Progress in Intelligent Decision Science, IDS 2020 (T. Allahviranloo, S. Salahshour, and N. Arica, editors), Advances in Intelligent Systems and Computing, vol. 1301, Springer, Cham, 2021, pp. 611–622.

[2] M. Khaled, G. Székely, K. Lefever, and M. Friend, Distances between formal theories. Review of Symbolic Logic , vol. 13 (2020), no. 3, pp. 633–654.

▸ B. SH. KULPESHOV, On criterion for binarity of almost $\omega$ -categorical weakly o-minimal theories.

Kazakh-British Technical University, Almaty, Kazakhstan.

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

This lecture concerns the notion of weak o-minimality which was initially deeply studied by Macpherson, Marker, and Steinhorn in [3]. A weakly o-minimal structure is a linearly ordered structure $M = \left\langle M, = ,<,\dots \right\rangle$ such that any definable (with parameters) subset of $M$ is a union of finitely many convex sets in $M$ . The rank of convexity of a formula with one free variable was introduced in [2].

The following notion was introduced in [1] and investigated in [4]. Let $T$ be a complete theory, and ${p}_1\!\left({x}_1\right),\dots, {p}_n\!\left({x}_n\right)\in {S}_1\!\left(\varnothing \right)$ . A type $q\!\left({x}_1,\dots, {x}_n\right)\in {S}_n\!\left(\varnothing \right)$ is said to be a $\left({p}_1,\dots, {p}_n\right)$ -type if $q\!\left({x}_1,\dots, {x}_n\right)\supseteq \underset{i = 1}{\overset{n}{\cup }}{p}_i\left({x}_i\right)$ . The set of all $\left({p}_1,\dots, {p}_n\right)$ -types of the theory $T$ is denoted by ${S}_{p_1,\dots, {p}_n}(T)$ . A countable theory $T$ is said to be almost $\omega$ -categorical if for any types ${p}_1\!\left({x}_1\right),\dots, {p}_n\!\left({x}_n\right)\in {S}_1\!\left(\varnothing \right)$ there are only finitely many types $q\!\left({x}_1,\dots, {x}_n\right)\in {S}_{p_1,\dots, {p}_n}(T)$ .

Theorem 1. Let $T$ be an almost $\omega$ -categorical weakly o-minimal theory. Then $T$ is binary iff every non-algebraic $p\in {S}_1\!\left(\varnothing \right)$ has finite convexity rank.

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

[1] K. Ikeda, A. Pillay, and A. Tsuboi, On theories having three countable models. Mathematical Logic Quarterly , vol. 44 (1998), no. 2, pp. 161–166.

[2] B. Sh. Kulpeshov, Weakly o-minimal structures and some of their properties. Journal of Symbolic Logic , vol. 63 (1998), pp. 1511–1528.

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

[4] S. V. Sudoplatov, Classification of Countable Models of Complete Theories, Part 1 , Novosibirsk State Technical University, Novosibirsk, 2018.

▸ SOHEI IWATA, TAISHI KURAHASHI, AND YUYA OKAWA, Craig’s interpolation and the fixed point properties for sublogics of interpretability logic $\mathbf{IL}$ .

Graduate School of System Informatics, Kobe University, 1-1, Rokkodai-Cho, Nada, Kobe, Hyogo 657-8501, Japan.

E-mail: soh.iwata@people.kobe-u.ac.jp.

E-mail: kurahashi@people.kobe-u.ac.jp.

Graduate School of Science and Engineering, Chiba University, 1-33 Yayoi-cho, Inage-ku, Chiba-shi, Chiba 263-8522, Japan.

E-mail: ahga4770@chiba-u.jp.

The interpretability logic $\mathbf{IL}$ is a basic logic for investigating the notion of relative interpretability. De Jongh and Visser proved that the fixed point property (FPP) holds for $\mathbf{IL}$ [2]. Also, Areces, Hoogland, and de Jongh proved that Craig’s interpolation property holds for $\mathbf{IL}$ [1].

In a previous work [3], several sublogics of $\mathbf{IL}$ were introduced and the modal completeness of 20 sublogics of $\mathbf{IL}$ were investigated. The weakest logic of them is ${\mathbf{IL}}^{-}$ and other logics are obtained by adding some $\mathbf{IL}$ -provable axioms to ${\mathbf{IL}}^{-}$ .

In this talk, we discuss the fixed point property and Craig’s interpolation property for sublogics of $\mathbf{IL}$ . Firstly, we completely reveal whether the fixed point property holds for the 20 sublogics of $\mathbf{IL}$ . The logic ${\mathbf{IL}}^{-}\left(\mathbf{J}{\mathbf{2}}_{+},\mathbf{J}\mathbf{5}\right)$ is the weakest logic of them having FPP, and ${\mathbf{IL}}^{-}\left(\mathbf{J}\mathbf{4},\mathbf{J}\mathbf{5}\right)$ is the weakest logic of them having a newly introduced weaker property $\mathrm{\ell}$ FPP. Moreover, we reveal whether Craig’s interpolation property holds for the 17 logics. Secondly, we introduce countably many sublogics of ${\mathbf{IL}}^{-}\left(\mathbf{J}{\mathbf{2}}_{+},\mathbf{J}\mathbf{5}\right)$ (resp. ${\mathbf{IL}}^{-}\left(\mathbf{J}\mathbf{4},\mathbf{J}\mathbf{5}\right)$ ) having FPP (resp. $\mathrm{\ell}$ FPP).

[1] C. Areces, E. Hoogland, and D. de Jongh, Interpolation, definability and fixed points in interpretability logics. Advances in Modal Logic , vol. 2 (1998), pp. 35–58.

[2] D. de Jongh and A. Visser, Explicit fixed points in interpretability logic. Studia Logica , vol. 50 (1991), pp. 39–50.

[3] T. Kurahashi and Y. Okawa, Modal completeness of sublogics of the interpretability logic IL. Mathematical Logic Quarterly , vol. 67 (2021), no. 2, pp. 164–185.

▸ BORIŠA KUZELJEVIĆ AND STEVO TODORČEVIĆ, Cofinal types on ${\omega}_2$ .

University of Novi Sad, Novi Sad, Serbia.

E-mail: borisha@dmi.uns.ac.rs.

University of Toronto, Toronto, ON, Canada.

Institut de Mathématiques de Jussieu, Paris, France.

Mathematical Institute SANU, Beograd, Serbia.

E-mail: stevo@math.utoronto.ca.

We will present the preliminary analysis of the class ${\mathcal{D}}_{\aleph_2}$ , the class of directed sets whose cofinality is ${\aleph}_2$ . We compare orders in ${\mathcal{D}}_{\aleph_2}$ using the notion of Tukey reducibility ${\le}_T$ , and we isolate some simple cofinal types in this class. We will explain why all of the simple types are pairwise non-equivalent. Then we proceed to show for which pairs ${E}_1$ , ${E}_2$ of these simple types there is no directed set $D$ such that ${E}_1{<}_TD{<}_T{E}_2$ . We also show that for the remaining pairs of these simple types, if GCH holds and there is a non-reflecting stationary subset of ${S}_0^2 = \left\{\alpha <{\omega}_2:\mathrm{cof}\left(\alpha \right) = \omega \right\}$ , then there is a directed set which is strictly between them in the Tukey ordering.

▸ DOROTA LESZCZYŃSKA-JASION AND MICHAŁ SOCHAŃSKI, On the representation of logical formulas as cographs.

Department of Logic and Cognitive Science, Adam Mickiewicz University, Poznań, Poland.

E-mail: dorota.leszczynska@amu.edu.pl.

E-mail: michal.sochanski@amu.edu.pl.

In our talk, we propose a novel method of representing semantic information contained in formulas of propositional logic in the language of graph theory. The method starts with creation of a syntax tree of a formula, with every subformula in the tree labelled with $\alpha$ or $\beta$ —depending on their type according to Smullyan’s uniform notation—and with every leaf corresponding to an occurrence of a literal. Such labelled tree can be used to construct a graph $G$ —further denoted as “semantic graph”—where $V(G)$ is the set of leafs of the tree, and two vertices ${x}_i$ , ${x}_j\in G$ are connected by an edge if the lowest common ancestor of ${x}_i$ and ${x}_j$ in the tree is a formula of type $\alpha$ . The resulting graph turns out to be a cograph and its properties can be used to analyse certain semantic properties of the formula. The most important property of semantic graphs is that every maximal clique in $G$ corresponds to a set of literals $L$ , such that any valuation that satisfies the formula contains $L$ . In addition to that it is known that every cograph is a permutation graph, which allows a representation of formulas—or the semantic dependencies between occurrences of literals in formulas—as a permutation. Many properties of cographs translate to properties of permutations; for example, maximal cliques in the cograph correspond to decreasing subsequences in the permutation. Both cographs and permutations allow the construction of efficient algorithms, which makes such representation of particular interest for computational logic.

▸ NURLAN MARKHABATOV AND SERGEY SUDOPLATOV, On closures for partially ordered families of theories.

Novosibirsk State Technical University, Novosibirsk, Russia.

E-mail: nur24.08.93@mail.ru.

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

Novosibirsk State University, Novosibirsk, Russia.

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

We apply a general approach for closures of families of theories [1, 2] for some special cases of partially ordered families.

Definition [2]. For a family $\mathcal{T}$ of theories in a language $\Sigma$ and a theory $T$ we put $T\in {\mathrm{Cl}}_1\!\left(\mathcal{T}\right)$ if $T\in \mathcal{T}$ , or $T$ is nonempty and $T = \big\{\varphi \in \mathrm{Sent}\left(\Sigma \right)\big\Vert {\left(\mathcal{T}\hbox{'}\right)}_{\varphi }|\ge \omega \big\}$ for some $\mathcal{T}\hbox{'}\subseteq \mathcal{T}$ . If $\mathcal{T}\hbox{'}$ is fixed then we say that $T$ belongs to the ${\mathrm{Cl}}_1$ -closure of $\mathcal{T}$ with respect to $\mathcal{T}\hbox{'}$ , and $T$ is an accumulation point of $\mathcal{T}$ with respect to $\mathcal{T}\hbox{'}$ .

Theorem 1 [2]. For any linearly $\subseteq$ -ordered family $\mathcal{T}$ , ${\mathrm{Cl}}_1\!\left(\mathcal{T}\right)$ consists of unions for subfamilies of $\mathcal{T}$ , and of intersections for countable subfamilies of $\mathcal{T}$ ordered by the type ${\omega}^{\ast }$ .

Theorem 2. For any partially $\subseteq$ -ordered family $\mathcal{T}$ with finitely many maximal chains, ${\mathrm{Cl}}_1\!\left(\mathcal{T}\right)$ consists of unions for unions of chains of $\mathcal{T}$ and for intersections of countable chains of $\mathcal{T}$ which are ordered by the type ${\omega}^{\ast }$ .

Theorem 2 can fail for the case of infinitely many maximal chains.

This research has been funded by RFBR (project No. 20-31-90003), by KN MON RK (Grant No. AP08855497), and by SB RAS (project No. 0314-2019-0002).

[1] N. D. Markhabatov and S. V. Sudoplatov, Topologies, ranks and closures for families of theories. I. Algebra and Logic , vol. 59 (2020), no. 6, pp. 649–679.

[2] _____, Topologies, ranks and closures for families of theories. II. Algebra and Logic , vol. 60 (2021), no. 1, pp. 57–80.

▸ YUKIHIRO MASUOKA AND MAKOTO TATSUTA, Counterexample to cut-elimination in cyclic proof system.

Department of Informatics, The Graduate University for Advanced Studies, SOKENDAI, Tokyo, Japan.

E-mail: yukihiro\_m@nii.ac.jp.

National Institute of Informatics, Tokyo, Japan.

The Graduate University for Advanced Studies, SOKENDAI, Tokyo, Japan.

E-mail: tatsuta@nii.ac.jp.

A cyclic proof system or a circular proof system, whose proof figures are finite trees with cycles, is an alternative proof system to the proof system with explicit induction. Brotherston defined the cyclic proof system ${\mathrm{CLKID}}^{\omega }$ for first-order logic with inductive definitions [1]. Conjecture 5.2.4. of [1] states the cut rule could not be eliminated in ${\mathrm{CLKID}}^{\omega }$ . We show that the conjecture is correct by giving a counterexample. The counterexample is a sequent which states that an inductive predicate of the addition implies another inductive predicate of the addition. We give a ${\mathrm{CLKID}}^{\omega }$ proof of the sequent with the cut rule and show that there is no ${\mathrm{CLKID}}^{\omega }$ proof of the sequent without the cut rule.

[1] J. Brotherston, Sequent calculus proof systems for inductive definitions , Ph.D. thesis, University of Edinburgh, 2006.

▸ LACHLAN MCPHEAT, MEHRNOOSH SADRZADEH, HADI WAZNI, AND GIJS WIJNHOLDS, Vectorial discourse analysis in Lambek calculus with a bounded relevant modality.

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

Institute of Linguistics, Utrecht University, Utrecht, The Netherlands.

E-mail: m.sadrzadeh@ucl.ac.uk.

Lambek calculus, the Gentzen-style sequent calculus of a residuated non-commutative monoid, provides a logic for the syntactic structure of preliminary fragment of natural language. Categorial grammarians such as Moortgat and Morrill showed how adding extra operators to the calculus makes it applicable to fragments witnessing phenomena that involve a form of movement, as in relative clauses. More recently, [2] showed that adding a relevant modality makes the calculus applicable to the notoriously complex phenomena of parasitic gaps. In previous work [3], we developed a categorical vector space semantics for this calculus where modal types were interpreted as Fock spaces and copying was obtained via a Frobenius comultiplication. We later showed that the calculus can also be applied to co-reference resolution and can distinguish between the strict/sloppy readings of ambiguous sentences. That framework faced two problems. Firstly, the calculus was undecidable. Secondly, the Frobenius comultiplication only provided approximations of the desired vector copying. In this paper, we redo all the previous work for the newly developed Soft Subexponentials of Lambek calculus [1], which is decidable. We show how the required full copying operation is now obtainable via the layer-wise projections of bounded Fock spaces. We implement the constructions on a large-scale corpus, build vector semantics for datasets of parasitic gap noun phrases and elliptic sentences, and show how our constructions advance the natural language processing tasks of disambiguation and similarity.

[1] M. Kanovich, S. Kuznetsov, V. Nigam, and A. Scedrov, Soft subexponentials and multiplexing, Automated Reasoning: 10th International Joint Conference, IJCAR 2020 , Lecture Notes in Computer Science, vol. 12166, Springer, Cham, 2020, pp. 500–517.

[2] M. Kanovich, S. Kuznetsov, and A. Scedrov, Undecidability of the Lambek calculus with a relevant modality. Lecture Notes in Computer Science , vol. 9804 (2016), pp. 240–256.

[3] L. McPheat, M. Sadrzadeh, H. Wazni, and G. Wijnholds, Categorical vector space semantics for Lambek calculus with a relevant modality. Electronic Proceedings in Theoretical Computer Science , vol. 333 (2021), pp. 168–182.

▸ JOSÉ M. MÉNDEZ, GEMMA ROBLES, AND FRANCISCO SALTO, Three-valued relevance logics.

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

E-mail: sefus@usal.es.

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

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

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

URL Address: http://grobv.unileon.es.

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

E-mail: francisco.salto@unileon.es.

Given a matrix semantics, a conditional is natural if the following conditions are fulfilled. (1) It coincides with the classical conditional when restricted to the classical values $T$ and $F$ ; (2) it satisfies the Modus Ponens; and (3) it is assigned a designated value whenever the antecedent and consequent are assigned the same value. This sense of “natural” being supposed, the class of all natural three-valued implicative expansions of Kleene’s strong logic is defined in [4]. It developed that a subclass of this class consists of relevance logics in Anderson and Belnap’s minimal sense of the term (cf. [1]): they have the “variable-sharing property.” The aim of this paper is to axiomatize the relevance logics in the aforementioned subclass by leaning upon an overdetermined two-valued Belnap–Dunn semantics (cf., e.g., [2, 3]).

Acknowledgement. Work supported by research project PID2020-116502GB-I00, financed by the Spanish Ministry of Science and Innovation (MCIN/AEI/10.13039/501100011033).

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

[2] N. D. Belnap, A useful four-valued logic, Modern Uses of Multiple-Valued Logic (G. Epstein and J. M. Dunn, editors), D. Reidel, Dordrecht, 1976, pp. 8–37.

[3] J. M. Dunn, Intuitive semantics for first-degree entailments and “coupled trees”. Philosophical Studies , vol. 29 (1976), pp. 149–168.

[4] G. Robles and J. M. Méndez, The class of all natural implicative expansions of Kleene’s strong logic functionally equivalent to Łukasiewicz’s 3-valued logic Ł3. Journal of Logic, Language and Information , vol. 29 (2020), no. 3, pp. 349–374.

▸ D. J. H. MOORE, Naturality as universal normative authority in Stoic logic.

Independent.

E-mail: djhmoore@gmail.com.

To be tractable, every science requires first principles. Each special science embarks from a foundation A of axioms, empirical laws, etc., thus employing a rule-based ethic to deductively arrive at consequent knowledge B. The construct can be represented schematically as

At the other limit we find metaphysics, the only science lacking determined genus and thus devoid of a priori knowledge. This leads to a right-side rationality schematic

Here, rationality flows in the opposite direction with a priori knowledge C on the right and the consequent D on the left. This schematic no longer illustrates a syllogism but its converse, a emphcosyllogism (not to be confused with Peirce’s abductions). For that the cosyllogism be tractable, empha priori knowledge C must be formalised in some way. We resort to the only viable normative authority available—naturality. In mathematics, naturality is colloquially regarded as involving constructs that are free of emphad hoc subjective choices. Traditional set theory mathematics is ill-equipped to formalise the ethics of naturality. The alternative is Category Theory originally developed “to study functors and natural transformations.” Natural transformations can be formalised in the form of naturality squares that commute where two sides are left and right adjoints making up “natural” symmetries—arguably the most ubiquitous and fundamental generic structure underlying mathematics.

In this paper, category theory will be shown to participate in its own natural symmetry with its “right adjoint” complementary opposite providing a natural way of formalising the cosyllogistic logic in P2.

The paper then goes on to show that the resulting cosyllogistic “right-side” rationality provides a means of reverse engineering the natural rationality underlying the five indemonstrables of ancient Stoic logic.

Key words and phrases. cosyllogism, metaphysics, naturality, adjunctions, Stoic indemonstrables.

▸ NAZERKE MUSSINA, OLGA ULBRIKHT, AND AIBAT YESHKEYEV, On the categoricity of the class of the Jonsson spectrum.

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

E-mail: nazerke170493@mail.ru.

E-mail: ulbrikht@mail.ru.

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

Let $L$ be countable language of an arbitrary signature $\sigma$ and $\mathcal{A}$ be an arbitrary model of this signature, i.e., $\mathcal{A}\in \mathrm{Mod}\kern0.1em \sigma$ . Let us call the Jonsson spectrum of model $\mathcal{A}$ a set:

The relation of cosemanticness on a set of theories is an equivalence relation. Then $\mathrm{JSp}\left(\mathcal{A}\right){/}_{\bowtie}$ is the factor set of Jonsson spectrum of the model $\mathcal{A}$ with respect to ${\bowtie}$ [3].

Denote by ${E}_{\left[T\right]} = \underset{\nabla \in \left[T\right]}{\cup }{E}_{\nabla }$ the class of all existentially closed models of class $\left[T\right]\in \mathrm{JSp}\left(\mathcal{A}\right){/}_{\bowtie}$ , where ${E}_{\nabla }$ is a class of all existentially closed models of $\nabla$ .

A formula $\varphi \left(\overline{x}\right)$ is called a $\Delta$ -formula [1] with respect to the theory $T$ if there are existential formulas ${\psi}_1\!\left(\overline{x}\right)$ and ${\psi}_2\left(\overline{x}\right)$ such that $T\models \left(\varphi \leftrightarrow {\psi}_1\right)$ and $T\models \left(\neg \varphi \leftrightarrow {\psi}_2\right)$ .

We say that a theory $T$ admits ${R}_1$ [1], if for any existential formula $\varphi \left(\overline{x}\right)$ consistent with $T$ there is a formula $\psi \left(\overline{x}\right)\in \Delta$ consistent with $T$ such that $T\models \left(\psi \to \varphi \right)$ .

Using the above mentioned notions, we have the following results.

Theorem 1. Let $\mathcal{A}$ be an arbitrary model of signature $\sigma$ , $\left[T\right]\in \mathrm{JSp}\left(\mathcal{A}\right){/}_{\bowtie}$ and $\left[T\right]$ be complete for $\exists$ -sentences class of universal theories for which holds ${R}_1$ . Then the following are equivalent:

1) The theory ${\left[T\right]}^{\ast }$ is ${\omega}_1$ -categorical.

2) Any countable model from ${E}_{\left[T\right]}$ has an algebraically prime model extension in ${E}_{\left[T\right]}$ .

Theorem 2. Let $L$ be a countable language, $\mathcal{A}$ be an arbitrary model of this language $L$ , and $\left[T\right]\in \mathrm{JSp}\left(\mathcal{A}\right){/}_{\bowtie}$ . If $\left[T\right]$ is $\forall \exists$ -complete $\omega$ -categorical class, then $\left[T\right]$ has $\omega$ -categorical model companion ${\left[T\right]}^M$ .

Theorem 3. Let $L$ be a countable language, $\mathcal{A}$ be an arbitrary model of this language, and $\left[T\right]\in \mathrm{JSp}\left(\mathcal{A}\right){/}_{\bowtie}$ . If $\left[T\right]$ is $\forall \exists$ -complete $\mathrm{\varkappa}$ -categorical class, then ${\left[T\right]}^{\ast }$ is model complete.

All additional information regarding Jonsson theories can be found in [2].

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

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

[2] A. R. Yeshkeyev and M. T. Kassymetova, Jonsson theories and their classes of models , Monograph, KSU, 2016.

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

▸ INESSA PAVLYUK AND SERGEY SUDOPLATOV, On rich properties for the family of theories of Abelian groups.

Novosibirsk State Technical University, Novosibirsk, Russia.

E-mail: inessa7772@mail.ru.

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

Novosibirsk State University, Novosibirsk, Russia.

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

We continue to study families of theories of Abelian groups [1, 2] describing possibilities for sentences with respect to rich properties following a general approach for links between formulas $\varphi$ and properties $P$ using the ranks ${\mathrm{RS}}_P$ [3].

Following [3], for a property $P\subseteq {\mathcal{T}}_{\Sigma}$ , a sentence $\varphi \in \mathrm{Sent}\left(\Sigma \right)$ is called $P$ -generic if ${\mathrm{RS}}_P\left(\varphi \right) = \mathrm{RS}(P)$ , and ${\mathrm{ds}}_P\left(\varphi \right) = \mathrm{ds}(P)$ if $\mathrm{ds}(P)$ is defined.

Let $\overline{\mathcal{TA}}$ be the family of all theories of Abelian groups in a language ${\Sigma}_0$ . A property $P\subseteq \overline{\mathcal{TA}}$ is called rich if $P\cap {P}^{\prime}\ne \varnothing$ for each nonempty property ${P}^{\prime} = {(\overline{\mathcal{TA}})}_{\varphi }$ defined by a sentence $\varphi$ locally describing linear (in)dependence, (in)divisibilities, and orders of elements.

Theorem 1. A property $P\subseteq \overline{\mathcal{TA}}$ is rich if and only if ${\mathrm{Cl}}_E(P) = \overline{\mathcal{TA}}$ .

Theorem 2. $\mid \left\{P\subseteq \overline{\mathcal{TA}}|P\kern0.22em is\kern0.17em rich\kern0.1em \right\}\mid = {2}^{\omega }$ ; moreover, $\mid \big\{P\subseteq \overline{\mathcal{TA}}\mid P$ is rich and countable $\big\}\mid = {2}^{\omega }$ .

Theorem 3. For any sentence $\varphi \in \mathrm{Sent}\left({\Sigma}_0\right)$ and a rich property $P\subseteq \overline{\mathcal{TA}}$ the following possibilities hold:

$(1)$ ${\mathrm{RS}}_P\left(\varphi \right) = -1$ , if $\varphi$ is $\overline{\mathcal{TA}}$ -inconsistent;

$(2)$ ${\mathrm{RS}}_P\left(\varphi \right) = 0$ , if $\varphi$ is $\overline{\mathcal{TA}}$ -consistent and belongs to (finitely many) theories in $\overline{\mathcal{TA}}$ with finite models only;

$(3)$ ${\mathrm{RS}}_P\left(\varphi \right) = \infty$ , if $\varphi$ belongs to a theory $T\in \overline{\mathcal{TA}}$ with an infinite model.

Corollary 4. For any sentence $\varphi \in \mathrm{Sent}\left({\Sigma}_0\right)$ and rich $P\subseteq \overline{\mathcal{TA}}$ either $\varphi$ is represented by a disjunction of finitely many sentences ${\varphi}_i$ isolating theories ${T}_i\in \overline{\mathcal{TA}}$ with finite models, or $\varphi$ is $P$ -generic.

Notice that the assertions above can fail if $P\subseteq \overline{\mathcal{TA}}$ is not rich.

The study was carried out within the framework of the state contract of the Sobolev Institute of Mathematics (project No. 0314-2019-0002) and the Committee of Science in Education and the Science Ministry of the Republic of Kazakhstan (Grant No. AP08855544).

[1] In. I. Pavlyuk and S. V. Sudoplatov, Families of theories of abelian groups and their closures. Bulletin of Karaganda University. Series “Mathematics” , vol. 90 (2018), pp. 72–78.

[2] _____, Ranks for families of theories of abelian groups. Bulletin of Irkutsk State University. Series “Mathematics” , vol. 28 (2019), pp. 95–112.

[3] S. V. Sudoplatov, Formulas and properties, preprint, 2021, arXiv:2104.00468v1 [math.LO].

▸ IOSIF PETRAKIS, Chu representations of categories related to constructive mathematics.

Mathematisches Institut, Ludwig-Maximilians-Universität München, Theresienstrasse 39, D-80333 Munich, Germany.

E-mail: petrakis@math.lmu.de.

If $\mathcal{C}$ is a closed symmetric monoidal category, the Chu category $\mathbf{CHU}\!\left(\mathcal{C},\gamma \right)$ over $\mathcal{C}$ and an object $\gamma$ of it was defined by Chu in [1], as a $\ast$ -autonomous category generated from $\mathcal{C}$ . In [2] Bishop introduced the category of complemented subsets of a set, in order to overcome the problems generated by the use of negation in constructive measure theory. In [4] Shulman mentions that Bishop’s complemented subsets correspond roughly to the Chu construction. In this talk, based on [3], we explain this correspondence by showing that there is a Chu representation (a full embedding) of the category of complemented subsets of a set $X$ into $\mathbf{CHU}\!\left(\mathbf{Set},X\times X\right)$ . A Chu representation of the category of Bishop spaces into $\mathbf{CHU}\!\left(\mathbf{Set},\mathrm{\mathbb{R}}\right)$ is shown, as the constructive analogue to the standard Chu representation of the category of topological spaces into $\mathbf{CHU}\!\left(\mathbf{Set},2\right)$ . In order to represent the category of predicates (with objects pairs $\left(X,A\right)$ , where $A$ is a subset of $X$ , and the category of complemented predicates (with objects pairs $\left(X,A\right)$ , where $A$ is a complemented subset of $X\!,$ we generalise the Chu construction on a Cartesian closed category by defining the Chu category over a Cartesian closed category $\mathcal{C}$ and an endofunctor on $\mathcal{C}$ . Finally, we introduce the antiparallel Grothendieck construction over a product category and a contravariant $\mathbf{Set}$ -valued functor on it, of which the Chu construction is a special case, if $\mathcal{C}$ is a locally small, Cartesian closed category.

[1] M. Barr, ${}^{\ast }$ -Autonomous Categories , Lecture Notes in Mathematics, vol. 752, Springer, Berlin–Heidelberg, 1979.

[2] E. Bishop, Foundations of Constructive Analysis , McGraw-Hill, New York, 1967.

[3] I. Petrakis, Chu representations of categories related to constructive mathematics, preprint, 2021, arXiv:2106.01878v1.

[4] M. Shulman, Linear logic for constructive mathematics, preprint, 2021, arXiv:1805.07518v1.

▸ ALEXEJ PYNKO, Finite Hilbert-style calculi for disjunctive and implicative finitely valued logics with equality determinant.

Institute of Cybernetics, Glushkov Prospect 40, Kiev 03680, Ukraine.

E-mail: pynko@i.ua.

The main result of the work is the fact that any propositional finitely valued logic (viz., logical matrix) $\mathrm{\mathcal{M}}$ having both distinguished and non-distinguished values, connectives in a [finite] propositional language $L$ , and equality determinant $\Im (p)\subseteq {\mathrm{Fm}}_L$ (in the sense of [1]) as well as (possibly, secondary) disjunction $\mid$ implication $\left(\vee |\supset \right)$ is axiomatized by any finite Hilbert-style calculus for the $\left(\vee |\supset \right)$ -fragment of the classical logic supplemented by [finitely many] rules $\mid$ axioms to be [effectively] constructed in the following way. Given any fixed total ordering $\leqslant$ of the finite set $\Im$ and any $L$ -sequential $\Im$ -table $\mathcal{T}$ of rank $\left(0,0\right)$ for $\mathrm{\mathcal{M}}$ (in the sense of [1]) to be found [effectively] (cf. Theorem 1 therein), let $\mathcal{A}$ be the [finite] set constituted by:

1. 1. those of the finitely many $L$ -sequents, true in $\mathrm{\mathcal{M}}$ , with disjoint left and right sides without repetitions, constituted by elements of $\Im$ and ordered according to $\leqslant$ , which are minimal under subsuming partial (because, for all formulas $\eta (p)$ and $\zeta (p)$ , $\eta = p = \zeta$ , whenever $\eta \left(\zeta \right) = p$ ) ordering between such sequents to be treated as clauses of the first-order signature $L\cup \left\{D\right\}$ with function symbols in $L$ and the only relation unary one $D$ ;

2. 2. for each $\iota \in \Im$ and every nullary $c\in L$ , that (unique) of the sequents $\iota (c)\vdash$ or $\vdash \iota (c)$ , which is true in $\mathrm{\mathcal{M}}$ ;

3. 3. for each $\iota \in \Im$ and every $F\in L$ distinct from $\left(\vee |\supset \right)$ of arity $n>0$ such that, whenever $n = 1$ , all those sequents, which are resulted from sequents in ${\left(\lambda /\rho \right)}_{\mathcal{T}}\left(\iota (F)\right)$ by adding the formula $\iota \left(F\left({p}_1,\dots, {p}_n\right)\right)$ to their right/left sides.

Then, we have the [finite] set $\mathrm{\mathcal{B}}\triangleq \big\{\left(\left({\phi}_0\vee q,\dots, {\phi}_{k-1}\vee q\right)\vdash \left({\psi}_0,\dots, {\psi}_{m-1},q\right)\right)\mid \left(\varnothing \vdash \left({\psi}_0/q,{\phi}_{k-1},\dots, {\phi}_0/,{\psi}_{m-1}\supset q,\dots, {\psi}_0\supset q\right)\right)\mid$ $0\ne k\in \omega \ni m\mid = /\ne 1,\overline{\phi}\in {\mathrm{Fm}}_L^k, \overline{\psi} \in {\mathrm{Fm}}_L^m, (\overline{\phi}\vdash \overline{\psi})\in \mathcal{A}\big\}$ of $L$ -sequents with non-empty right sides $\mid$ “and empty left ones.” (Note that $q\not\in(\{p\}\cup\{p_i\}_{0\neq i\in\omega})$ is a variable occurring in no sequent in $\mathcal{A}$ .) Finally, the supplementary rules $\mid$ axioms are as follows: for each $(\overline{\phi}\vdash \overline{\psi})\in \mathrm{\mathcal{B}}$ , where $\overline{\phi}\in {\mathrm{Fm}}_L^k$ and $\overline{\psi}\in {\mathrm{Fm}}_L^m$ , while $k,m\in \omega$ , whereas $m\ne 0\mid = k$ , the $L$ -rule $\mid$ -axiom $\left\{{\phi}_0,\dots, {\phi}_{k-1}\right\}\to \left(\dots \left({\psi}_0\left(\vee |\subset \right)\dots \right)\left(\vee |\subset \right){\psi}_{m-1}\right)$ , respectively, as well as, for each $\left(\varnothing \vdash \overline{\psi}\right)\in \mathcal{A}$ , where $\overline{\psi}\in {\mathrm{Fm}}_{\Sigma_n}^m$ , while $0\ne m\in \omega$ , the $L$ -axiom $\big(\dots ({\psi}_0{\vee}_{\mid \supset}\dots )({\vee}_{\mid \supset }{\psi}_{m-1})\mid$ “, where $\left(p{\vee}_{\supset }q\right)\triangleq \left(\left(p\supset q\right)\supset q\right)$ ,” respectively. In view of Examples 1–3 of [1], this universal [effective] construction is well applicable (and has been successfully applied) to [both disjunctive $\mid$ implicative fragments of the classical logic and] arbitrary $\mid$ implicative four-valued expansions of Belnap’s “useful” four-valued logic [by finitely many connectives] $\mid$ “as well as to [both arbitrary ukasiewicz’ finitely valued logics and] certain implicative paraconsistent three-valued logics [with finitely many connectives like $\mathrm{HZ}$ , providing its first finite Hilbert-style axiomatization].”

[1] A. P. Pynko, Sequential calculi for many-valued logics with equality determinant. Bulletin of the Section of Logic , vol. 33 (2004), no. 1, pp. 23–32.

▸ ERIC RAIDL, Definable conditionals.

Cluster of Excellence “Machine Learning: New Perspectives for Science”, University of Tübingen, Maria von Lindenstrasse 6, 72076 Tübingen, Germany.

E-mail: eric.raidl@uni-tuebingen.de.

Conditionals “if $A$ , [then] $C$ ” are difficult to analyze. A standard account has however emerged [3]: a conditional $A>C$ is true in the actual world (roughly) if and only if the closest $A$ -worlds are $C$ -worlds. However, recent reflections suggest to strengthen the defining clause by additional conditions. Different approaches argue for different additional conditions [1, 2, 4, 9–11]. In this talk, I present a general method to prove completeness results for such definable or strengthened conditionals, as I developed it in [5].

The problem is this: Imagine you have a conditional of the form

• • $\varphi \vartriangleright \psi$ in world $w$ iff closest $\varphi$ -worlds are $\psi$ -worlds and $X$ .

Suppose that $X$ is also formulated in terms of closeness. One can then rephrase $\varphi \vartriangleright \psi$ as $\left(\varphi >\psi \right)\wedge \chi$ , where $\chi$ is the expression corresponding to the condition $X$ . The central question is whether known completeness results for $>$ can be used to obtain completeness results for $\vartriangleright$ . The answer is yes and the paper provides a general method: First, redefine $>$ in terms of $\vartriangleright$ . This backtranslation of $\varphi >\psi$ yields a formula $\alpha$ in the language for $\vartriangleright$ . One can then use this backtranslation to translate axioms for $>$ into axioms for $\vartriangleright$ . This is a looking glass which provides a distorted picture of the logic for $>$ , in terms of $\vartriangleright$ . The picture is a logic for $\vartriangleright$ . The method can be applied to many conditional constructions [5–8]. In this talk I present the logic of a new example—the connective because, based on the semantic analysis by [9].

[1] V. Crupi and A. Iacona, The Evidential Conditional, Erkenntnis (2021). https://doi.org/10.1007/s10670-020-00332-2.

[2] D. Lewis, Causation. Journal of Philosophy , vol. 70 (1973), no. 17, pp. 556–567.

[3] _____, Counterfactuals , Blackwell, Oxford, 1973.

[4] E. Raidl, Completeness for counter-doxa conditionals—using ranking semantics. Review of Symbolic Logic , vol. 12 (2019), no. 4, pp. 861–891.

[5] _____, Definable conditionals. Topoi , vol. 40 (2021), pp. 87–105.

[6] _____, Strengthened conditionals, Context, Conflict and Reasoning (B. Liao and Y. Wáng, editors), Springer, Singapore, 2020, pp. 139–155.

[7] _____, Three conditionals: Contraposition, difference-making, and dependency, Logica Yearbook 2020 (M. Blicha and I. Sedlár, editors), College Publications, London, 2021, pp. 201–217.

[8] E. Raidl, A. Iacona, and V. Crupi, The logic of the evidential conditional. Review of Symbolic Logic (2021), pp. 1–13. https://doi.org/10.1017/S1755020321000071.

[9] H. Rott, Ifs, though and because. Erkenntnis , vol. 25 (1986), no. 3, pp. 345–370.

[10] _____, Difference-making conditionals and the relevant Ramsey test. Review of Symbolic Logic , vol. 15 (2022), no. 1, pp. 133–164.

[11] W. Spohn, Conditionals: A unifying ranking-theoretic perspective. Philosophers’ Imprint , vol. 15 (2015), no. 1, pp. 1–30.

▸ CARMEN REQUENA AND FRANCISCO SALTO, Brain activity marks of logical validity: results from EEG and MEG studies.

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

E-mail: c.requena@unileon.es.

E-mail: francisco.salto@unileon.es.

The objective of this research is to verify or refute the presence of specific cerebral electrical marks in logically valid inferences. The studies focus on extensional bivalent truth-functional inferences in which logical validity (in classical sense) and probabilistic p-validity (in Adam’s sense) coincide. Remarkably, it is not presupposed that any inference exemplifying a deductive argument is eo ipso a deductive inference. This has been an a priori assumption in cognitive neuroscience and it is important because, if understood as abstract relations among propositions or probabilities [2], deductive arguments are clearly distinct from non-deductive arguments. However, as time-consuming cortical events, deductive inferences are far less clearly distinct from non-deductive inferential processes [1]. Twenty-three subjects in the MEG study and 20 in the EEG research were placed into a two conditions paradigm framed in the SET game, with 100 trials for each condition, logically valid vs invalid [3]. Results show: (i) deductive inferences with the same content evoke the same electromagnetic response pattern in both logically valid and invalid conditions, (ii) the amplitude and intensity is lower in valid deductions, significantly in the MEG study (p = 0.0003), (iii) reaction time in valid deductions was significantly higher (54.37% in MEG and 61.54% in EEG), (iv) time/frequency patterns of valid deductions show beta-2 band activations at early (300 ms) and late (650 ms) stages (p-value 0.005), and (v) valid deductions involve frontal connectivity patterns and bands dynamically distinct from invalid inferences. As a conclusion, validity leaves a measurable electrical trait in brain processing. Valid inference is a less-demanding and slow automatism, probably attributable to the recursive and automatable character of valid deductions, suggesting a physical indicator of computational deductive properties.

[1] A. Chuderski, The relational integration task explains fluid reasoning above and beyond other working memory tasks. Memory & Cognition , vol. 42 (2014), no. 3, pp. 448–463.

[2] G. Harman, The relational integration task explains fluid reasoning above and beyond other working memory tasks, Foundations: Logic, Language and Mathematics (H. Leblanc, E. Mendelson, and A. Orenstein, editors), Springer, New York, 1984, pp. 107–127.

[3] F. Salto, C. Requena, P. Álvarez-Merino, L. Antón, and F. Maestú, Brain electrical traits of logical validity. Scientific Reports , vol. 11 (2021), no. 7982, pp. 1–13.

▸ DAVID REYES AND PEDRO H. ZAMBRANO, Co-quantale valued logics.

Universidad Nacional de Colombia, Bogotá, Colombia.

E-mail: davreyesgao@unal.edu.co.

E-mail: phzambranor@unal.edu.co.

In this talk, we present a generalization of Continuous Logic (see [3]) where the distances take values in suitable co-quantales (in the way as it was proposed in [1]).

Co-quantales are somehow an interesting setting because Flagg [1] proved that any general topological space can be viewed as a generalized pseudo-metric space where the distance takes values on a suitable co-quantale.

By assuming suitable conditions (e.g., being co-divisible, co-Girard, and a V-domain), we provide, as test questions, a proof of a version of the Tarski–Vaught test and Łoś Theorem in our setting.

Hopefully, this approach would provide an interesting setting to do Model Theory for general Topological Spaces.

[1] R. Flagg, Quantales and continuity spaces. Algebra universalis , vol. 37 (1997), pp. 257–276.

[2] D. Reyes and P. Zambrano, Co-quantale valued logics, preprint, 2021, arXiv:2102.06067.

[3] I. B. Yaacov, A. Berenstein, C. W. Henson, and A. Usvyatsov, Model theory for metric structures, Model Theory with Applications to Algebra and Analysis , London Mathematical Society Lecture Notes Series, vol. 349, Cambridge University Press, Cambridge, 2008, pp. 315–427.

▸ GEMMA ROBLES, Alternative semantical interpretations of the paraconsistent and paracomplete four-valued logic PŁ4.

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

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

URL Address: http://grobv.unileon.es.

The logic PŁ4 is characterized by a modification of the matrix determining Łukasiewicz’s four-valued modal logic Ł (cf. [2]). It is a strong and rich paraconsistent and paracomplete four-valued logic where necessity and possibility (among other) operators are definable without “Łukasiewicz-type modal paradoxes” being provable (cf. [3]). The logic PŁ4 is introduced in [3], but in [1] it is remarked that De and Omori’s logic BD ${}_{+}$ , Zaitsev’s paraconsistent logic FDEP, and Beziau’s four-valued logic PM4M are equivalent to PŁ4 (cf. [1] and references therein). The fact that the four systems just quoted have been obtained independently and from different motivations seems to suggest that they are four versions of a strong and rich natural logic.

PŁ4 is originally interpreted with a two-valued Belnap–Dunn semantics (cf. [3] and references therein). Nevertheless, the aim of the present paper is to provide still another perspective on PŁ4 by endowing it with both a ternary Routley–Meyer semantics and a binary Routley-semantics together with their respective restriction to the 2 setup case (cf. [4]).

Acknowledgement. Work supported by research project PID2020-116502GB-I00, financed by the Spanish Ministry of Science and Innovation (MCIN/AEI/10.13039/501100011033).

[1] N. Kamide and H. Omori, An extended first-order Belnap–Dunn logic with classical negation, Logic, Rationality, and Interaction (6th International Workshop, LORI 2017, Sapporo, Japan, September 11–14, 2017) (A. Baltag, J. Seligman, and T. Yamada, editors), Lecture Notes in Computer Science, vol. 10455, Springer, Berlin–Heidelberg, 2017, pp. 79–63.

[2] J. Łukasiewicz, A system of modal logic. Journal of Computing Systems , vol. 1 (1953), pp. 111–149.

[3] J. M. Méndez and G. Robles, A strong and rich 4-valued modal logic without Łukasiewicz-type paradoxes. Logica Universalis , vol. 9 (2015), no. 4, pp. 501–522.

[4] R. Routley, R. K. Meyer, V. Plumwood, and R. T. Brady, Relevant Logics and Their Rivals, vol. 1 , Ridgeview, Atascadero, 1982.

▸ ANTON SETZER, A model of computation for single threaded sequential interactive programs.

Department of Computer Science, Swansea University, Swansea SA1 8EN, UK.

E-mail: a.g.setzer@swansea.ac.uk.

URL Address: http://www.cs.swan.ac.uk/csetzer/.

We present two models of computation derived from our formalisation (together with Peter Hancock) of interactive programs in dependent type theory, which define the IO monad using weakly final coalgebras.

The first model covers non-state-dependent interactive programs. An interface consists of commands $\mathrm{C}\in \mathcal{P}\!\left(\mathrm{\mathbb{N}}\right)$ and responses $\mathrm{R}:\mathrm{C}\to \mathcal{P}\!\left(\mathrm{\mathbb{N}}\right)$ . Examples of commands are the printing of a string with response set a singleton set, or reading input from console with response the string being read. Instructions to actuators and reading from sensors can be represented similarly.

The set of interactive programs for an interface $\left(\mathrm{C},\mathrm{R}\right)$ is the largest set $\mathrm{IO}$ of pairs $\left\langle c,f\right\rangle$ with $c\in \mathrm{C}$ and $\left\{f\right\}:\mathrm{R}(c)\to \mathrm{IO}$ . In order to define a monadic version $\mathrm{IO}(A)$ , we add to $\mathrm{C}$ termination commands $\mathrm{return}(a)$ for $a\in A$ with $\mathrm{R}\left(\mathrm{return}(a)\right) = \varnothing$ . One can define monadic composition $\_ \gg \_ :\left(\mathrm{IO}(A)\times \left(A\to \mathrm{IO}(B)\right)\right)\to \mathrm{IO}(B)$ .

The second model adds a state to the interface, which determines the set of commands available, and which changes depending on commands and responses issued. So, we have states $\mathrm{S}\in \mathcal{P}\left(\mathrm{\mathbb{N}}\right)$ , $\mathrm{C}\in \mathrm{S}\to \mathcal{P}\left(\mathrm{\mathbb{N}}\right)$ , $\mathrm{R}\in \prod s\in \mathrm{S}.\mathrm{C}(s)\to \mathcal{P}\left(\mathrm{\mathbb{N}}\right)$ , and $\mathrm{next}\in \prod s\in \mathrm{S}.\prod r\in \mathrm{C}(s).\mathrm{R}\left(s,r\right)\to \mathrm{S}$ . We define $\mathrm{IO}(s)$ as the largest set of pairs $\left\langle c,f\right\rangle$ with $c\in \mathrm{C}(s)$ and $\left\{f\right\}\in \prod r\in \mathrm{R}\left(s,r\right).\mathrm{IO}\left(\mathrm{next}\left(s,c,r\right)\right)$ . A monadic version $\mathrm{IO}\left(s,A\right)$ for $A\in \mathrm{S}\to \mathcal{P}\left(\mathrm{\mathbb{N}}\right)$ can be defined similarly. Equality is bisimulation.

[1] A. Abel, S. Adelsberger, and A. Setzer, Interactive programming in Agda—Objects and graphical user interfaces. Journal of Functional Programming , vol. 27 (2017), p. E8.

▸ PAUL SHAFER, An infinite ${\Pi}_1$ set with no ${\Delta}_2$ cohesive subset.

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

E-mail: p.e.shafer@leeds.ac.uk.

A classic theorem of D. Martin states that there is a co-infinite recursively enumerable set with no maximal superset. By taking complements and appealing to the correspondence between maximal sets and ${\Pi}_1$ cohesive sets, Martin’s result may be rephrased as stating that there is an infinite ${\Pi}_1$ set with no ${\Pi}_1$ cohesive subset. We generalize this result by showing that there is an infinite ${\Pi}_1$ set with no ${\Delta}_2$ cohesive subset. We describe how this generalization naturally arises from recent work on cohesive powers, and, time permitting, we sketch a direct proof.

▸ RAFFAEL STENZEL, $\left(\infty, 1\right)$ -Categorical comprehension schemes.

Department of Mathematics and Statistics, Masaryk University, Building 8, Kotlářská 2, 611 37 Brno, Czech Republic.

E-mail: stenzelr@math.muni.cz.

Comprehension schemes arose as a crucial notion in the early work on the foundations of set theory, and hence found expression in a variety of foundational settings for mathematics. In particular, Bénabou [1] provided an intuition to define the notion of comprehension schemes for arbitrary fibered categories in a syntax-free way. The notion has been made precise in considerable generality by Johnstone in [2], tying together the elementary examples given in the glossary of [1] to a structurally well-behaved theory.

In this talk—based on [3]—we generalize Johnstone’s notion of comprehension schemes to the context of Cartesian fibrations over $\left(\infty, 1\right)$ -categories. In doing so it turns out not only that many results do carry over, but that some pivotal constructions are in fact better behaved for the reason that “evil” meta-mathematical equalities naturally arising in the context of ordinary category theory are implicitly replaced by “good” instances of equivalences between $\left(\infty, 1\right)$ -categories. Much in the spirit of Univalent Foundations, the study of equality becomes a study of equivalence.

The aim of the talk will be to present some of the central results in [3] and show how to apply them to natural examples arising in higher topos theory as well as higher category theory in general.

[1] J. Bénabou, Fibered categories and the foundations of naive category theory. Journal of Symbolic Logic , vol. 50 (1985), no. 1, pp. 10–37.

[2] P. T. Johnstone, editor, Sketches of an Elephant: A Topos Theory Compendium , Oxford University Press, Oxford, 2002.

[3] R. Stenzel, $\left(\infty, 1\right)$ -Categorical comprehension schemes, preprint, 2020, arXiv:2010.09663.

▸ SOURAV TARAFDER AND GIORGIO VENTURI, ZF between classicality and non-classicality.

Department of Commerce, St. Xavier’s College, 30 Mother Teresa Sarani, Kolkata 700016, India.

E-mail: souravt09@gmail.com.

Instituto de Filosofia e Ciências Humanas, Universidade Estadual de Campinas, Barão Geraldo, R. Cora Coralina, 100-Cidade Universitária, Campinas, SP 13083-896, Brazil.

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

Using a model $\mathbf{V}$ of Zarmelo–Fraenkel set theory ( $\mathsf{ZFC}$ ) and a complete Boolean algebra $\mathbb{B}$ one can construct Boolean-valued model ${\mathbf{V}}^{\left(\mathbb{B}\right)}$ of $\mathsf{ZFC}$ . This is done by assigning to every set theoretic sentence an algebraic (truth) value by means of a map ; a sentence $\varphi$ is said to be valid in ${\mathbf{V}}^{\left(\mathbb{B}\right)}$ , denoted by ${\mathbf{V}}^{\left(\mathbb{B}\right)}\models \varphi$ , if , the top element of $\mathbb{B}$ . This construction was generalised in [57] to get algebra-valued models ${\mathbf{V}}^{\left(\mathbb{A}\right)}$ of classical and non-classical set theories, where $\mathbb{A}$ is a reasonable implication algebra ( $\mathsf{RIA}$ ).

If we now fix a model $\mathbf{V}$ of $\mathsf{ZF}$ and an algebra $\mathbb{A}$ , but change the notion of validity as ${\mathbf{V}}^{\left(\mathbb{A}\right)}\models \varphi$ iff , where $D\subseteq \mathbb{A}$ is called a designated set, then we get a more liberal interpretation of this method. The new class of algebras found in this way will be called reasonable implication designated algebra ( $\mathsf{RIDA}$ ), whose properties will depend on the interaction between the operations and the designated set. We will show how $\mathsf{RIDA}$ ’s offer a generalisation of $\mathsf{RIA}$ ’s. If $\mathbb{A}$ is an $\mathsf{RIDA}$ then ${\mathbf{V}}^{\left(\mathbb{A}\right)}\models \mathrm{NFF}$ - $\mathsf{ZF}$ , the negation-free fragment of $\mathrm{ZF}$ . Finally a property regarding complementation will be added to $\mathsf{RIDA}$ to have a new algebra, reasonable implication complemented designated algebra ( $\mathsf{RICDA}$ ). For an $\mathsf{RICDA}$ , $\mathbb{A}$ we will show ${\mathbf{V}}^{\left(\mathbb{A}\right)}\models \mathsf{ZF}$ .

Class many examples of $\mathsf{RICDA}$ , $\mathbb{A}$ will be provided so that the logic of the algebra is non-classical, but the logic of the set theory corresponding to ${\mathbf{V}}^{\left(\mathbb{A}\right)}$ is classical.

[1] B. Löwe and S. Tarafder, Generalized algebra-valued models of set theory. Review of Symbolic Logic , vol. 8 (2015), no. 1, pp. 192–205.

▸ YANA RUMENOVA AND TINKO TINCHEV, Undecidability of modal definability: the class of frames with two commuting equivalence relations.

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

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

Let $\mathcal{K}$ be the class of all relational structures with two commuting equivalence relations and ${\mathcal{K}}^{\mathrm{fin}}$ be the class of all finite structures from $\mathcal{K}$ . Our goal is to study the modal definability of sentences with respect to $\mathcal{K}$ (resp. ${\mathcal{K}}^{\mathrm{fin}}$ ). Remind that a sentence $A$ from a first-order language with two binary predicate symbols is modally definable with respect to some class of frames if there is a modal formula $\varphi$ from the propositional modal language with two unary modalities such that $A$ and $\varphi$ are valid in the same frames from the class. In this talk we prove the following.

Theorem 1. The problem of deciding the validity of sentences in $\mathcal{K}$ (resp. ${\mathcal{K}}^{\mathrm{fin}}$ ) is reducible to the problem of deciding the modal definability of sentences with respect to $\mathcal{K}$ (resp. ${\mathcal{K}}^{\mathrm{fin}}$ ).

Theorem 2. The first-order theories of $\mathcal{K}$ and ${\mathcal{K}}^{\mathrm{fin}}$ are heretitarily undecidable.

Corollary 3. The problem of deciding the modal definability of sentences with respect to $\mathcal{K}$ (resp. ${\mathcal{K}}^{\mathrm{fin}}$ ) is undecidable.

▸ URSZULA WYBRANIEC-SKARDOWSKA, A formal-logic approach to the ontology of language.

Department of Philosophy, Cardinal Stefan Wyszyński University, Warsaw, Poland.

E-mail: uws@uni.opole.pl.

E-mail: skardowska@gmail.com.

The ontology of language is understood here as a general formal-logical theory of language, considered as a particular ontological being and generated by the classical categorial grammar. The main goal of this paper is to outline the theory in accordance with the logical conception of language proposed by Ajdukiewicz [1] and formalized on the basis of classical logic and set theory. The theory is sketched with respect to the dual ontological status of linguistic expressions as either concreta—i.e., tokens, in the sense of material, physical objects—or types, in the sense of classes of tokens—i.e., abstract, ideal objects. Such a duality takes into account two different levels of formalization of the theory of linguistic syntax, semantics, and pragmatics, one stemming from concreta, construed as linguistic tokens of expressions, the other—from their classes, namely types, conceived as abstract beings. The two dual-aspect theoretical approaches to linguistic syntax are logically equivalent. The outcome of the considerations is recognition of complete analogousness between the syntactic notions of the two levels, so logic does not settle which view pertaining to the nature of linguistic objects—the concretistic one or the idealistic, platonizing, one—is correct. The basic semantic-pragmatic notions of “meaning” and ‘”denotation” are used only with reference to expressions-types of language, but their definitions require using some notions for expressions-tokens. Considerations related to the formalization of the categorial language lead to the statement that the logic applied here (using set theory) is ontologically neutral due to the existential assumptions regarding the existence of linguistic expressions and their extra linguistic counterparts.

[1] K. Ajdukiewicz, Pragmatic logic. Synthese Library , vol. 62 (1975), p. 12.

[2] U. Wybraniec -Skardowska, Logic and ontology of language, Contemporary Polish Ontology (B. Skowron, editor), De Gruyter, Berlin–Boston, 2020, pp. 109–132.

▸ OLGA ULBRIKHT AND AIBAT YESHKEYEV, The Jonsson nonforking notion under some positiveness.

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

E-mail: ulbrikht@mail.ru.

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

Let $L$ be a first-order language. Denote by $\mathrm{At}$ the set of atomic formulas of the language $L$ and by ${B}^{+}\left(\mathrm{At}\right)$ the set of all positive Boolean combinations (conjunction and disjunction) of atomic formulas. ${L}^{+} = Q\left({B}^{+}\left(\mathrm{At}\right)\right)$ is a set of formulas in normal prenex form obtained by applying quantifiers ( $\forall$ and $\exists$ ) to ${B}^{+}\left(\mathrm{At}\right)$ . A formula will be called positive if it belongs to ${L}^{+}$ . Let ${\Pi}_2^{+}$ be the set of all $\forall \exists$ -formulas of a language ${L}^{+}$ . Let $\Delta \subseteq {\Pi}_2^{+}\subseteq {L}^{+}.$ All morphisms which we are considering below will be immersions as in [2].

Definition 1. Theory $T$ will be called $\Delta$ - $J$ -theory, if it satisfies the following conditions:

1) theory $T$ has infinite model;

2) theory $T$ is ${\Pi}_2^{+}$ -axiomatizable;

3) theory $T$ admits $\Delta$ -JEP;

4) theory $T$ admits $\Delta$ -AP.

Let $T$ be a $\Delta$ - $J$ -theory, and $M$ be the semantic model of $T$ . Let $\mathcal{A}$ be the class of all subsets of semantic model $M$ , let $\mathcal{P}$ be the class of all positive $\exists$ -types (not necessarily complete), and let $\mathrm{PJNF}$ (positive Jonsson nonforking) $\subseteq \mathcal{P}\times \mathcal{A}$ be a binary relation. There is the list of the axioms 1–7 which defined positive Jonsson nonforking notion $\mathrm{PJNF}$ and we have result for $\Delta$ - $J$ -theory $T$ .

Theorem 2. The following conditions are equivalent:

1) the relation $\mathrm{PJNF}$ satisfies the axioms 1–7 relative to $\Delta$ - $J$ -theory $T$ ;

2) ${T}^{\ast }$ stable and for all $p\in \mathcal{P}$ , $A\in \mathcal{A}$ ( $\left(p,A\right)\in \mathrm{PJNF}\iff p$ not fork over $A$ ) (in the classical meaning of S. Shelah), where ${T}^{\ast }$ is the center of the $\Delta$ - $J$ -theory $T$ .

Further we considered on the $\mathcal{P}\times \mathcal{A}$ the relation $\mathrm{PJNFLP}$ which is $\Delta$ -positive analog of the notion of forking by Lascar–Poizat [1]. The following theorem was obtained.

Theorem 3. Let $T$ be $J$ -stable existentially complete perfect $\Delta$ - $J$ -theory, then the following conditions are equivalent:

1) the relation $\mathrm{PJNFLP}$ satisfies the axioms 1–7;

2) the concepts of $\mathrm{PJNF}$ and $\mathrm{PJNFLP}$ coincide.

All concepts that are not defined in this note will be able to extract from [3].

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

[1] D. Lascar and B. Poizat, An introduction to forking. Journal of Symbolic Logic , vol.44 (1979), no. 3, pp. 330–350.

[2] B. Poizat and A. Yeshkeyev, Positive Jonsson theories. Logica Universalis , vol.12 (2018), nos. 1–2, pp. 101–127.

[3] A. R. Yeshkeyev and M. T. Kassymetova, Jonsson theories and their classes of models , Monograph, KSU, 2016.

Abstracts of talks presented by title

▸ JOACHIM MUELLER-THEYS, Mathematical theorems on equality and unequality.

Independent, Heidelberg, Germany.

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

Let $P,Q,\dots$ be properties over some domain $M$ , and $a,b,\dots \in M$ . We have defined $a{\equiv}_Pb$ by $P(a)\iff P(b)$ . For instance, $7{\equiv}_{\mathrm{odd}}5$ , $4{\equiv}_{\mathrm{odd}}8$ , . $a{\equiv}_{\mathcal{P}}b$ : iff $a{\equiv}_Pb$ for all $P\in \mathcal{P}\subseteq \wp (M)$ . Thereby we could—among other things—analyze statements of the form “all $M$ are equal” naturally through the totality of ${\equiv}_{P/\mathcal{P}}$ . We have proven that $P = M$ is the one and only non-vacuous $P$ such that all $M$ are $P$ -equal and that $\mathcal{P} = \left\{M\right\}$ is the unique $\mathcal{P}$ (with $P\ne \varnothing$ for all $P\in \mathcal{P}$ ) such that all $M$ are $\mathcal{P}$ -equal. Cf. “Similarity and Equality,” 2021 ASL Annual Meeting.

We shall now, more generally, analyze statements of the form “all $P$ are equal.” Let us first regard the tempting interpretation of “equal” by identical, yielding $P(a)\&P(b)$ $\Rightarrow$ $a = b$ , which, however, is equivalent to $\mid P\kern0.1em \mid \le 1$ , whence $\mathrm{AllId}(P)$ becomes false for, e.g., $P:=$ human (unless restricted to the residents of the Island of Despair, before Friday came).

So we interprete “equal” by $Q$ -equal again: ${\mathrm{AllEq}}_Q(P)$ : iff for all $a,b\in M$ : $P(a)$ $\&$ $P(b)$ implies $a{\equiv}_Qb$ . We have recently found and proven that ${\mathrm{AllEq}}_Q(P)$ is equivalent to the homogeneity of $P$ with respect to $Q$ , viz. $P$ is a sub-property (subset) of $Q$ or $P$ is a sub-property of $-Q$ . This General Equality Theorem, triggered by discussions with P. Maier-Borst proves mathematically that, for instance, human beings are equal only with respect to (extensional) attributes, like primate and creature, and to properties they are not joint with, like fish. This may be called the “tertium non datur” or dichotomy of equality.

The result relies on the following three propositions:

$P\subseteq Q$ $\Rightarrow$ ${\mathrm{AllEq}}_Q(P)$ ;

$P\cap Q = \varnothing$ $\Rightarrow$ ${\mathrm{AllEq}}_Q(P)$ ;

${\mathrm{AllEq}}_Q(P)\&P\cap Q\ne \varnothing$ $\Rightarrow$ $P\subseteq Q$ .

It is a theorem of (augmented) logic.

As a consequence, ${\mathrm{Uneq}}_Q(P)$ is always the case if (and only if) $P$ is heterogeneous with respect to $Q$ , viz. $P$ is joint with $Q$ and $P$ is joint with $-Q$ . Particularly, ${\mathrm{Uneq}}_P(M)$ if (and only if) $\varnothing \subset P\subset M$ . For example, the property human is heterogeneous with respect to the property woman, as there are human beings that are women and human beings that are no women.

Recognise that there is an astounding relationship to the syllogistic propositions and their relationships.

Let us eventually look at $P(a)\&P(b)$ $\Rightarrow$ $a{\equiv}_{\mathcal{P}}b$ . Then ${\mathrm{AllEq}}_{\mathcal{P}}(P)$ iff ${\mathrm{Hom}}_{\mathcal{P}}(P)$ , and ${\mathrm{Uneq}}_{\mathcal{P}}(P)$ if(f) ${\mathrm{Het}}_Q(P)$ for some $Q\in \mathcal{P}$ . If $\mathcal{P}$ is a system of disjoint properties $P$ , ${\mathrm{AllEq}}_{\mathcal{P}}(P)$ .