</p>

In this talk, I will present a category theoretical notion, the trace category, which generalizes the trace condition of many cyclic proof systems. Indeed, a handful of different trace categories are sufficient to capture the trace conditions of all cyclic proof systems from the literature I have examined so far. The arising abstract notion of cyclic proof allows for the derivation of generalized renditions of standard results of cyclic proof theory, such as the decidability of proof-checking and the regularizability of certain non-wellfounded proofs. It also opens the door to broader inquiries into the structural properties of trace condition based cyclic and non-wellfounded proof systems, some of which I will touch on in this talk, time permitting. The majority of this talk will be based on my Master’s thesis.

</p>

As theoretical background, we assume that numbers are properties of collections (Simons 1982, 2007, 2011; Johansson 2015; Angere 2014). We observe that the domain of number is determined by two types of invariances. First, the concept of collection itself depends on being invariant under the location of its objects. Second, the determinant invariance of the domain of number is the fungibility of objects: If an object in a collection is exchanged for another object, the collection will still contain the same number of objects. Fungibility will be shown to be closely related to one-to-one correspondences.

We first introduce the concept of a collection and show how it differs from the concept of a set. Then we present the invariance of location of objects that applies to collections and we introduce fungibility as a second type of invariance. We illustrate our theoretical analysis by empirical material from experiments of developmental psychologists.

This is joint work with Peter Gärdenfors (Lund).

In almost all (with only one exception that I’m aware of) logical systems based on team semantics this lifting operation is the power set operation, and as a result the set of teams satisfying a formula is closed downwards. This is often taken as a basic and foundational principle of team semantics.

In this talk I will discuss this principle and present some ideas on why, or why not, the power set operation is the most natural lift operation. By using other lift operations we can get a more powerful semantics, but, it seems, also a more complicated one.

References:

• Engström, F. (2012) “Generalized quantifiers in dependence logic”
• Nurmi, V. (2009) “Dependence Logic: Investigations into Higher-Order Semantics Defined on Teams”
• Väänänen, J. (2007) “Dependence logic: A new approach to independence friendly logic”

This can also be used for strategy analysis in games. Evaluating formulae that define winning regions in a given game in an appropriate semiring of polynomials provides not only the Boolean information on who wins, but also tells us how they win and which strategies they might use. For this approach, the case of Büchi games is of special interest, not only due to their practical importance, but also because it is the simplest case where the logical definition of the winning region involves a genuine alternation of a greatest and a least fixed point. We show that, in a precise sense, semiring semantics provide information about all absorption-dominant strategies – strategies that win with minimal effort, and we discuss how these relate to positional and the more general persistent strategies. This information enables further applications such as game synthesis or determining minimal modifications to the game needed to change its outcome.

The first part of the talk focuses on the axiomatizations of type (1). We adapt the argument by Visser and Pakhomov (“On a question of Krajewski’s”, JSL 84(1), 2019) to show that there is no weakest axiomatization of this form (even if the axiomatizations are ordered by relative interpretability). Secondly, we sketch an argument showing that such axiomatizations with the given ordering form a countably universal partial order. This part is based on our joint work with Ali Enayat, available at https://www.researchgate.net/publication/353496287_Axiomatizations_of_Peano_Arithmetic_A_truth-theoretic_view

In the second part of the talk we discuss axiomatizations of type (2). We narrow our attention to such axiomatizations A for which CT^-[EA] + “All axioms from A are true” is a conservative extension of PA. We explain why such theories have very diverse metamathematical properties (e.g. large speed-up). To illustrate our methods we show that, with the given ordering, such axiomatizations do not form a lattice. This is a work still in progress.

In this talk I will discuss a line of work that attempts to understand the expressivity of circular reasoning via forms of proof theoretic strength. Namely, I address predicate logic in the guise of first-order arithmetic, and type systems in the guise of higher-order primitive recursion, and establish a recurring theme: circular reasoning buys precisely one level of ‘abstraction’ over inductive reasoning.

This talk will be based on the following works:

• https://arxiv.org/abs/1807.10248
• https://arxiv.org/abs/2012.14421

In this work, we take a semantic approach to normalization, called Normalization by Evaluation (NbE) (Berger and Schwichtenberg 1991), by leveraging the possible world semantics of Fitch-style calculi. We show that NbE models can be constructed for calculi that incorporate the K, T and 4 axioms, with suitable instantiations of the frames in their possible world semantics. In addition to existing results that handle beta reduction (or computational rules), our work also considers eta expansion (or extensional equality rules).

References:

• Borghuis, V.A.J. (1994). “Coming to terms with modal logic : on the interpretation of modalities in typed lambda-calculus”.
• Clouston, Ranald (2018). “Fitch-Style Modal Lambda Calculi”.
• Berger, Ulrich and Helmut Schwichtenberg (1991). “An Inverse of the Evaluation Functional for Typed lambda-calculus”.

In 2005, Ulrich Kohlenbach introduced higher order reverse mathematics, and we give a brief explanation of the what and why? of Kohlenbach’s approach. In an ongoing project with Sam Sanders we have studied the strength of classical theorems of late 19th/early 20th century mathematics, partly within Kohlenbach’s formal typed theory and partly by their, in a generalised sense, constructive content. In the final part of the talk I will give some examples of results from this project, mainly from the perspective of higher order computability theory. No prior knowledge of higher order computability theory is needed.

The fact that this remains open stands in stark contrast to the fact that the first order theory of the much similar object Q_p, the field of p-adic numbers, is completely understood thanks to the work by Ax, Kochen and, independently, Ershov. In light of this dichotomy, I will present new decidability results obtained during my doctoral research on extensions of F_p((t)). This work is motivated by recent progress on Hilbert’s tenth problem for F_p((t)) by Anscombe and Fehm and builds on previous decidability results by Kuhlman.</p>

We consider which characteristics of logics, such as variants of the Löwenheim-Skolem Theorem, Completeness Theorem, and absoluteness, are relevant from the logicality point of view, continuing earlier work by Bonnay, Feferman, and Sagi. We suggest that a logic is the more logical the closer it is to first order logic, and offer a refinement of the result of McGee that logical properties of models can be expressed in L_∞∞ if the expression is allowed to depend on the cardinality of the model, based on replacing L_∞∞ by a “tamer” logic. This is joint work with Jouko Väänänen.</p>

Six months ago I started to examine this report - I suspect I am the first logician to do that. It contains many surprising things. Besides introducing some new ideas that readers of Avicenna know from his later works, it also identifies some specific points of modal logic where Avicenna was sure that Aristotle had made a mistake. People had criticised Aristotle’s logic before, but not at these points. At first Avicenna had no clear understanding of how to do modal logic, and it took him another thirty years to justify all the criticisms of Aristotle in his report. But meanwhile he discovered for himself how to defend a new logic by building new foundations. I think the logic itself is interesting, but the talk will concentrate on another aspect. These recent discoveries mean that Avicenna is the earliest known logician who creates new logics and tells us what he is doing, and why, at each stage along the way.

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 (HAP). Let IF be the extension of Heyting arithmetic by fix-points, denoted \hat{ID}ⁱ₁ in the literature. The proof is divided into four parts: First we extend the inclusion of HA into HAP to IF into a similar theory IFP in the logic of partial terms. We then show that every theorem of this theory provably has a realizer in the theory IFP(Λ) 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 IFP(Λ) is interpretable in HAP. Finally we use use the result of [2] that adding the schema of “self-realizability” for arithmetic formulae to HAP is conservative over HA. The result generalises the work presented at my half-time seminar 2020-08-28.

References

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

[2] Benno van den Berg and Lotte van Slooten. Arithmetical conservation results. Ind- agationes Mathematicae, 29:260–275, 2018.

However, since focusing was traditionally specified as a restriction of the sequent calculus, the technique had not been transferred to logics that lack a (shallow) sequent presentation, as is the case for some modal or substructural logics.

With K. Chaudhuri and L. Straßburger, we extended the focusing technique to nested sequents, a generalisation of ordinary sequents, which allows us to capture all the logics of the classical and intuitionistic S5 cube in a modular fashion. This relied on an adequate polarisation of the syntax and an internal cut-elimination procedure for the focused system which in turn is used to show its completeness.

Recently, with A. Gheorghiu, we applied a similar method to the logic of Bunched Implications (BI), a substructural logic that freely combines intuitionistic logic and multiplicative linear logic. For this we had first to reformulate the traditional bunched calculus for BI using nested sequents, followed again by a polarised and focused variant that we show is sound and complete via a cut-elimination argument.

Examples of semantic concepts available in team semantics but not in traditional Tarskian semantics are the concepts of dependence and independence. Dependence logic is an extension of first-order logic based on team semantics. It has emerged that teams appear naturally in several areas of sciences and humanities, which has made it possible to apply dependence logic and its variants to these areas. In my talk I will give a quick introduction to the basic ideas of team semantics and dependence logic as well as an overview of some new developments, such as quantitative analysis of team properties, a framework for a multiverse approach to set theory, and probabilistic independence logic inspired by the foundations of quantum mechanics.

Conservativity is typically proved model-theoretically, or proof-theoretically via the elimination of cuts on formulae containing truth (Tr-cuts). The original Tr-cut-elimination argument for the theory of Tarskian, compositional truth CT[B] by Halbach is not conclusive. This strategy has been corrected by Graham Leigh: Leigh supplemented Halbach’s strategy with the machinery of approximations (introduced by Kotlarski, Krajewski and Lachlan in the context of their M-Logic). In the talk we investigate a different, and arguably simpler way of supplementing Halbach’s original strategy. It is based on an adaptation of the Takeuti/Buss free-cut elimination strategy for first-order logic to the richer truth-theoretic context. If successful, the strategy promises to generalize to the type-free setting in a straightforward way. This is joint work with Luca Castaldo.

An argument is valid when all its inferences are valid, and it then amounts to a proof in case it has no unbound assumptions or variables. The validity of an inference – not to confuse with the conclusion being a logical consequence of the premisses – seems in turn best explained in terms of proofs. This means that the concepts of valid inference and valid argument depend on each other and cannot be defined independently but have to be described by principles that state how they are related. A number of such principles will be proposed. It is conjectured that inferences that can be expressed in the language of first order intuitionistic predicate logic and are implied to be valid by these principles are all provable in that logic.

This is the idea that conditional perfection is a form of exhaustification, triggered by a question that the conditional answers. If a speaker is asked how B comes about, then the answer “If A, B” is interpreted exhaustively to meaning that A is the only way to bring about B. Hence, “A if and only if B.” The evidence suggests that conditional perfection is a form of exhaustification, but not that it is triggered by a relationship to a salient question. (This is joint work with Fabrizio Cariani.)

They are, however, an important alternative to finitary proofs and in the last decade have helped break some important barriers in the proof theory of logics formalising inductive and co-inductive concepts. In this talk we focus on cyclic proofs for modal logics, ranging from Gödel-Löb logic to more expressive languages such as the modal mu-calculus, and reflect on how they can contribute to the development of the theory of fixed point modal logic.