Logic@GU

The notion of pure extension of modules, and the corresponding notions of pure-injectivity and pure-projectivity, play a central role in commutative algebra, aspecially in its connections to model theory. In joint work with Casarosa, motivated by applications to algebraic topology and operator algebras, we have introduced the first “higher order” generalization of purity, defining “pure extensions of order α” for every countable ordinal α. Classical purity corresponds to the particular case when α=0.

In this talk I will present connections with logic: as classical purity is characterized in terms of first order logic, we will show that higher order purity has a natural interpretation in terms of infinitary logic, in such a way that the order of purity corresponds to length of infinitary formulae.

Justification logic is an explication of modal logic: boxes are replaced with proof terms formally through realisation theorems. This can be achieved syntactically using a cut-free proof system for a modal logic, e.g., using sequent, hypersequent, or nested sequent calculi. In constructive modal logic, boxes and diamonds are decoupled and not De Morgan dual. Previous work provides a justification counterpart to constructive modal logic CK (and some extensions) by making diamonds explicit and introducing new terms called satisfiers. We continue this line of work and provide a justification counterpart to intuitionistic modal logic IK and its extensions with the t and 4 axioms. We extend the syntax of proof terms to accommodate the additional axioms of intuitionistic modal logic and provide an axiomatisation of these justification logics with a syntactic realisation procedure using a cut-free nested sequent system for intuitionistic modal logic.

A 2½-day workshop dedicated to current and future trends in cyclic and illfounded forms of provability and justification. The event is sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity, the Swedish Research Council through the research project Proofs with Cycles and Computation, and the Department of Philosophy, Linguistics and Theory of Science at the University of Gothenburg.

Speakers

• Henning Basold (Leiden University)
• Anupam Das (University of Birmingham)
• Sebastian Enqvist (Stockholm University)
• Zeinab Galal (RIMS, Kyoto)
• Iris van der Giessen (University of Amsterdam)
• Marianna Girlando (University of Amsterdam)
• Helle Hvid Hansen (University of Groningen)
• Stefan Hetzl (TU Wien)
• Alex Leitsch (TU Wien)
• Reuben Rowe (Royal Holloway)
• Alexis Saurin (IRIF)
• Takeshi Tsukada (Chiba University)

Location

The workshop will be held at the Faculty of Humanities of the University of Gothenburg, address Renströmsgatan 6, Gothenburg. It is adjacent to the Korsvägen transport hub and within walking distance from the city centre.

Registration

Attendence is free but registration is required. The deadline for registration is Monday, 1 September. To register fill the form at: https://forms.cloud.microsoft/e/bFQJayDiKe

Schedule

Morning of Wednesday, 24 September until afternoon of Friday, 26 September 2025.

Organisors

• Graham E Leigh
• Gianluca Curzi
• Bahareh Afshari
• Ivan Di Liberti
• Dominik Wehr
• Giacomo Barlucchi

In case of questions, contact Graham Leigh

Opponent: TBA

Abstract Description logics are designed to reason efficiently with ontologies in knowledge bases, which are widely used in several industries. Human errors commonly cause mistakes to occur in the axioms of these ontologies, which leads to the logics deducing false conclusions. Ontology engineers spend much time on finding these false axioms to repair the ontology. This process can be facilitated by presenting a justification of the false conclusion, i.e. a set of axioms that entail the conclusion. Typically, the number of justifications for a given conclusion is very large and it is not clear which one should be presented.

It is therefore useful to estimate the cognitively adequate complexity of description logic so that the simplest justification(s) can be identified and selected. This work focusses on the cognitive complexity of deciding the consistency of ABoxes in the description logic $\mathcal{ALE}$. Conceptual considerations entail that the complexity of the ABox consistency problem is expressed as a linear preorder on a large enough set of ABoxes. This linear preorder can be estimated by an ACT-R model called SHARP. The model is a tableau algorithm implemented in a cognitive architecture, thereby modelling a human brain executing the tableau algorithm, which forms an approximation of the cognitive complexity ordering.

A complexity ordering that is a linear preorder can be obtained from experimental data by aggregating the different individual orders from a sample into one so-called proto-order, in which the largest transitive subrelation is the desired linear pre-order. The predicted complexity ordering by SHARP agrees well with the empirical data.

To enable applications in ontology debugging, a surrogate model is needed that accurately approximates SHARP’s output with great computational efficiency. Such a surrogate model can be obtained by the Random Forest algorithm trained on an appropriate dataset generated by SHARP. The complexity ordering thus obtained agrees well with the one predicted by SHARP but can be estimated in a fraction of the time enabling it for practical applications.

Examination committee:

• TBC

Dependence and independence concepts are ubiquitous in natural science, social science, humanities as well as in everyday life. The sentences “I park on this side of the road depending only on the day of the week” and “the time of descent is independent of the weight of the object” are examples of this. The question arises, do these concepts possess enough exactness for us to investigate their logic? There is currently a whole literature on this topic. It is the purpose of this talk to give a non-technical overview of this area of logic.

The combination of Löwenheim-Skolem Theorem and Compactness Theorem limits the expressive power of a logic to that of first order logic. This maximality principle is the famous Lindström Theorem for first order logic. It reveals that first order logic is at an optimal point of balance: by adding expressive power to it one necessarily loses model-theoretic properties. Soon after Lindström’s result, the question was raised, whether there are other logics at a similar point of equilibrium. More precisely: are there strict strengthenings of first order logic satisfying a Lindström-type characterization? Despite the naturality of this question, it remained unanswered, until recently.

In 2012 Saharon Shelah offered a solution to this problem in the form of a new infinitary logic. It has a Lindström-type characterization in terms of model-theoretic properties combining weak forms of Compactness and a Löwenheim-Skolem type property. In all known cases, a proof of a Lindström-type characterization automatically gives a proof of Craig Interpolation. This is the case for Shelah’s logic, too. There is, however, one aspect where Shelah’s logic seems to be rather weak: the syntax. The logic is derived from a game, in the sense that a sentence is, by definition, a class of structures, closed under a certain Ehrenfeucht-Fraïssé type of a game. This results in the absence of a syntax defined in such a way that the set of all formulas could be obtained by closing the set of atomic formulas under negation, conjunction, quantifiers, and possibly other logical operations. The lack of syntax complicates further study of it and logics in its neighborhood. In the present talk, we address the general question of deriving a syntax from a game, and the more localized question of finding a syntax for Shelah’s logic. Partial answers are provided to both questions. This is joint work with Andres Villaveces and Siiri Kivimäki.