Logic@GU

On Monday, 25 August the Nordic Online Logic Seminar will host a special event in memory of Krister Segerberg, who passed away in January this year. Krister Segerberg was Professor of Theoretical Philosophy at Uppsala and, among logicians, is widely known for his pioneering work in modal logic where he initiated an influential systematic study of completeness proofs that still is standard in the field.

The seminar will feature talks by two academics that knew Krister Segerberg well:

• Johan van Benthem (UvA), Building Modern Modal Logic: Honoring Krister Segerberg
• John Cantwell (KTH), Some reflections on Krister’s philosophy of philosopy

A URL for this seminar will be distributed via the GU Logic and Nordic Online Logic mailing lists.

Krister Segerberg was one of the architects of modal logic as we know it today. I will highlight a few of his major contributions and show some of their subsequent impact in various academic communities. I conclude with some thoughts on the blend of philosophical logic and formal philosophy embodied in Krister’s distinguished career.

In this talk I will briefly outline Krister’s biography, focusing mainly on the early nineties onwards when I became Krister’s first PhD student. By appeal (mostly) to anecdote I will try to highlight what I take to be some of the most notable features in Krister’s approach to and views on pilosophically inspired logical research and education.

Gödel intended his Dialectica interpretation to provide a foundational reduction of first-order arithmetic to a quantifier-free theory T. It has widely been objected, however, that this theory T tacitly presupposes the very quantificational logic that Gödel was trying to eliminate, hidden within its complicated definition of “computable function of finite type.” This would render the translation philosophically circular. Gödel was adamant that there was no circularity here. He sketched a defense of this claim in a page-long footnote, which however has left readers baffled. In this talk, I will explain Gödel’s footnote and show that there really is no circularity here. Thus, Gödel has achieved a significant foundational reduction. The foundations of T turn out to be stranger than meets the eye; they utilize a (broadly) Leibnizian notion of analyticity in a surprising way.

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