Archive of events from 2023
An archive of events from the year

Göran Sundholm (Leiden University)
CurryHoward: a meaning explanation or just another realizability interpretation?
Around 1930 a major paradigm shift occurred in the foundations of mathematics; we may call it the METAMATHEMATICAL TURN. Until then the task of a logician had been to design and explain a fullscale formal language that was adequate for the practice of mathematical analysis in such a way that the axioms and rules of inference of the theory were rendered evident by the explanations.
The metamathematical turn changed the status of the formal languages: now they became (meta)mathematical objects of study. We no longer communicate with the aid of the formal systems – we communicate about them. Kleene’s realizability (JSL 1945) gave a metamathematical (re)interpretation of arithmetic inside arithmetic. Heyting and Kolmogorov (19312), on the other hand, had used “proofs” of propositions, respectively “solutions” to problems, in order to explain the meaning of the mathematical language, rather than reinterpret it internally.
We now have the choice to view the CurryHoward isomorphism, say, as a variant of realizability, when it will be an internal mathematical reinterpretation, or to adopt an atavistic, Fregelike, viewpoint and look at the language as being rendered meaningful. This perspective will be used to discuss another paradigm shift, namely that of distinguishing constructivism and intuitionism. The hesitant attitude of Gödel, Kreisel, and Michael Dummett, will be spelled out, and, at the hand of unpublished source material, a likely reason given.

Tjeerd Fokkens (FLoV)
Cutting through SHARP
The model SHARP is a result of (somewhat naively) implementing a tableauxbased reasoning algorithm of the description logic ALE into the cognitive architecture ACTR. Its aim is to predict the inference time of human performance on deciding inconsistency of an ALE ABox, thereby giving rise to a complexity measure on ABoxes that is cognitively adequate. Ten predictions following from SHARP are tested against empirical data and their implications for the model are discussed.

Sonja Smets (Institute for Logic, Language and Computation, University of Amsterdam)
Reasoning about Epistemic Superiority and Data Exchange
In this presentation I focus on a framework that generalizes dynamic epistemic logic in order to model a wider range of scenarios including those in which agents read or communicate (or somehow gain access to) all the information stored at specific sources, or possessed by some other agents (including information of a nonpropositional nature, such as data, passwords, secrets etc). The resulting framework allows one to reason about the state of affairs in which one agent (or group of agents) has ‘epistemic superiority’ over another agent (or group). I will present different examples of epistemic superiority and I will draw a connection to the logic of functional dependence by A. Baltag and J. van Benthem. At the level of group attitudes, I will further introduce the new concept of ‘common distributed knowledge’, which combines features of both common knowledge and distributed knowledge. This presentation is based on joint work with A. Baltag in [1].
[1] A. Baltag and S. Smets, Learning what others know, in L. Kovacs and E. Albert (eds.), LPAR23 proceedings of the International Conference on Logic for Programming, AI and Reasoning, EPiC Series in Computing, 73:90110, 2020. https://doi.org/10.29007/plm4

Dag Westerståhl (Stockholm University, Tsinghua University)
From consequence to meaning: the case of intuitionistic propositional logic (IPL)
One quarter of the talk presents background on how facts about entailments and nonentailments can single out the constants in a language, and in particular on an idea originating with Carnap that the standard relation of logical consequence in a formal language should fix the (modeltheoretic) meaning of its logical constants. Carnap’s focus was classical propositional logic (CPL), but his question can be asked for any logical language. The rest of the talk gives a very general positive answer to this question for IPL: the usual IPL consequence relation does indeed determine the standard intuitionistic meaning of the propositional connectives, according to most wellknown semantics for IPL, such as Kripke semantics, Beth semantics, Dragalin semantics, topological semantics, and algebraic semantics.

Giacomo Barlucchi (FLoV)
The Limit of Recursion in Statebased Systems
We prove that ω^{2} strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. In doing so, we both extend and correct the previously claimed result on closure ordinals of the alternationfree μcalculus. The new approach sees a reincarnation of Kozen’s wellannotations, originally devised for showing the finite model property for the modal μcalculus. We develop a theory of conservative wellannotations where minimality of the annotation is guaranteed, and isolate relevant parts of the structure that necessitate an unfolding of fixed points. This adoption of wellannotations enables a direct and clear pumping process that rules out closure ordinals between ω^{2} and the limit of countability.

Ivan Di Liberti (FLoV)
Pictures at an exhibition: (1)70 years of functorial semantics
Boole, Tarski, Stone, Lawvere, Reyes, Makkai

Graham E Leigh (FLoV)
An axiomatic theory of falsity
Compositional theories of truth tend to follow the Tarskian tradition, either the modeltheoretic semantics for classical predicate logic or its natural generalisations to manyvalue and possibleworlds. Other realisations of truth, which includes computational interpretations and game semantics, have been largely ignored by truth theorists. In this talk I will present axiomatic rendering of Krivine’s “classical realisability”, a ‘truth as programs’ semantics for classical logic that validates extensions of Peano arithmetic. What sets this conception of truth apart from the Tarskian view is its treatment of falsity as primitive and truth as a derived notion. This is joint work with Daichi Hayashi (Hokkaido University, Japan).

Thomas Bolander (Technical University of Denmark)
Epistemic Planning: Logical formalism, computational complexity, and robotic implementations
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, e.g. robots, 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. The talk will introduce epistemic planning based on DEL, address issues of computational complexity, and demonstrate applications in cognitive robotics and humanrobot collaboration.

Gianluca Curzi (FLoV)
Infinitary cutelimination via finite approximations
We investigate nonwellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cutelimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns welldefined nonwellfounded proofs at its limit. Furthermore, we show that cutelimination preserves the progressive criterion and various regularity conditions internalizing degrees of prooftheoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

CLASP Conference on Learning with Small Data (LSD)
There is now an acute need for intensive research on the possibility of effective learning with small data. The conference LSD running 11–12 September, organised by the Centre for Linguistic Theory and Studies in Probability (CLASP) and at the department of Philosophy, Linguistics and Theory of Science is devoted to work on this problem, with application to computational linguistics.
See the conference webpage for details.

Thomas Ågotnes (University of Bergen and Shanxi University)
Somebody Knows and Weak Conjunctive Closure in Modal Logic
Normal modal logics are closed under conjunctive closure. There are, however, interesting nonnormal logics that are not, but which nevertheless satisfy a weak form of conjunctive closure. One example is a notion of group knowledge in epistemic logic: somebodyknows. While something is general knowledge if it is known by everyone, this notion holds if it is known by someone. Somebodyknows is thus weaker than general knowledge but stronger than distributed knowledge. We introduce a modality for somebodyknows in the style of standard group knowledge modalities, and study its properties. Unlike most other group knowledge modalities, somebodyknows is not a normal modality; in particular it lacks the conjunctive closure property. We provide an equivalent neighbourhood semantics for the language with a single somebodyknows modality, together with a completeness result: the somebodyknows modalities are completely characterised by the modal logic EMN extended with a particular weak conjunctive closure axiom. The neighbourhood semantics and the completeness and complexity results also carry over other logics with weak conjunctive closure, including the logic of socalled local reasoning (Fagin et al., 1995) with bounded “frames of mind”, correcting an existing completeness result in the literature (Allen 2005). The talk is based on joint work with Yi N. Wang.

Raheleh Jalali (Czech Academy of Sciences)
General form of rules implies feasible admissibility
In this talk, we introduce a general family of sequentstyle calculi over the modal language and its fragments to capture the essence of all constructively acceptable systems. Calling these calculi constructive, we show that any strong enough constructive sequent calculus, satisfying a mild technical condition, feasibly admits all Visser’s rules, i.e., there is a polynomial time algorithm that reads a proof of the premise of a Visser’s rule and provides a proof for its conclusion. As a positive application, we show the feasible admissibility of Visser’s rules in several sequent calculi for intuitionistic modal logics, including CK, IK and their extensions by the modal axioms T, B, 4, 5, the modal axioms of bounded width and depth and the propositional lax logic. On the negative side, we show that if a strong enough intuitionistic modal logic (satisfying a mild technical condition) does not admit at least one of Visser’s rules, then it cannot have a constructive sequent calculus. Consequently, no intermediate logic other than IPC has a constructive sequent calculus. (joint work with Amir Tabatabai)

David Cerna (Czech Academy of Sciences)
Cutelimination, Schematic Refutations, and Formula Schemata
There are interpretations of Herbrand’s theorem extending its scope to formal number theory, though at the expense of analyticity, its most desirable property. Therefore, deepening our understanding of the analyticity boundary is important to many areas of computer science, as inductive theorem proving has a wide range of applications. One approach to studying this bound is through cutelimination and how we can transform proofs using inductive reasoning. In this talk, we discuss cutelimination by resolution, how to extend the method to proof schema, infinite sequences of proofs, and the framework presented in “Schematic Refutations of Formula Schemata.”

Magdalena Ortiz (Umeå University)
A Short Introduction to SHACL for Logicians
The SHACL Shapes Constraint Language was recommended in 2017 by the W3C for describing constraints on web data (specifically, on RDF graphs) and validating them. At first glance, it may not seem to be a topic for logicians, but as it turns out, SHACL can be approached as a formal logic, and actually quite an interesting one. In this paper, we give a brief introduction to SHACL tailored towards logicians and frame key uses of SHACL as familiar logic reasoning tasks. We discuss how SHACL relates to description logics, which are the basis of the OWL Web Ontology Languages, a related yet orthogonal standard for web data. Finally, we summarize some of our recent work in the SHACL world, hoping that this may shed light on how ideas, results, and techniques from wellestablished areas of logic can advance the state of the art in this emerging field.

Research Lindström Lecture: Rineke Verbrugge (University of Groningen)
Aspects of provability and interpretability
In 1994, Rineke Verbrugge did a postdoc in Gothenburg, as a scientific guest of Professor Per Lindström, who was writing his landmark book Aspects of Incompleteness at the time. Even though the two of them did not coauthor any papers that year, there was still significant mutual influence and there were very lively discussions in the weekly seminars of the logic group. In this research lecture, Rineke Verbrugge will present some of the questions and results around bounded arithmetic, provability and interpretability logic that she was working on that year, for example, a small reflection principle for bounded arithmetic and the lattice of feasible interpretability types.

Public Lindström Lecture: Rineke Verbrugge (University of Groningen)
Combining probability and provability logic
It has been shown in the late 1960s that each formula of firstorder logic without constants and function symbols obeys a zeroone law: As the number of elements of finite models increases, every formula holds either in almost all or in almost no models of that size. For modal logics, limit behavior for models and frames may differ. In 1994, Halpern and Kapron proved zeroone laws for classes of models corresponding to the modal logics K, T, S4, and S5. They also proposed zeroone laws for the corresponding classes of frames, but their zeroone law for Kframes has since been disproved, and so has more recently their zeroone law for S4frames.
Provability logic was one of the main interests of Per Lindström. In this talk, we prove zeroone laws for provability logic with respect to both model and frame validity. Moreover, we axiomatize validity in almost all irreflexive transitive finite models and in almost all irreflexive transitive finite frames, leading to two different axiom systems. In the proofs, we use a combinatorial result by Kleitman and Rothschild about the structure of finite (strict) partial orders: almost all of them consist of only three layers. Finally, we present empirical results in order to give an idea of the number of elements from which onwards a formula’s almost sure validity or almost sure invalidity stabilizes in such threelayer KleitmanRothschild frames. We also discuss possible extensions of the zeroone laws to the modal logics S4 and K4.

Licentiate defence: Dominik Wehr (FLoV)
Representation matters in cyclic proof theory
Public defence of Dominik Wehr’s Licentiate thesis.
Opponent Associate Professor Anupam Das, University of Birmingham
Examiner Docent Fredrik Engström, Göteborgs universitet
Thesis available at the Gothenburg University Library Archive. 
Workshop on Fixed Points and Illfounded Proofs
Held on 2728 April, 2023 at the University of Gothenburg, this workshop brought together researchers working on various aspects of fixed point logics and illfounded proofs. The event was sponsored by the Knut and Alice Wallenberg Foundation via the research project Taming Jörmungandr: The Logical Foundations of Circularity and the Department of Philosophy, Linguistics and Theory of Science.

Neil Tennant (Ohio State University)
It's All or Nothing: Explosion v. Implosion
We set out five basic requirements for a logical system to be adequate for the regimentation of deductive reasoning in mathematics and science. We raise the question whether there are any further requirements, not entailed by these five, that ought to be imposed. One possible reply is dismissed: that the logical system should allow one to infer any proposition at all from an inconsistent set—i.e., it should have as primitive, or allow one to derive, the rule Ex Falso Quodlibet. We then propose that the logic should be implosive: it should not allow an inconsistent set to have any consequences other than absurdity. This proposal may appear to be very radical; but we hope to show that it is robust against objections.

Johannes Kloibhofer (ILLC, Amsterdam)
Using automata theory to obtain a new proof system for the modal µcalculus
Automata theory has various applications in the theory of the modal µcalculus. One such application is for the tableaux games for the modal µcalculus introduced by Niwinski and Walukiewicz, in which one player has a winning strategy iff the formula is satisfiable. The winning condition of that game can be naturally checked by a nondeterministic parity automaton. We show how the determinisation of that automaton may be used to obtain a proof system. We then introduce a determinisation method for nondeterministic parity automata, which will be used to define a new annotated cyclic proof system for the modal µcalculus.
(joint work with Johannes Marti and Yde Venema)

Anouk Oudshoorn (TU Wien)
Reconciling SHACL and Ontologies
The World Wide Web Consortium (
w3c ) set Web Ontology Language (owl ) and Shape Constraint Language (shacl ) as international standards for managing semantically enriched data on the web. However, there is a difference in how these languages handle the completeness of data. Inowl , not all information has to be explicitly present; part of the information can be implied by logical rules. Whereasshacl , which enables us to check for certain structures in a given knowledge graph, assumes completeness of it. Thus, withshacl we can validate the given data, while withowl we can infer knowledge. Combining the functionalities of the two into one standard is relevant and not straightforward.In this seminar talk, we will introduce a new semantics for validating stratified
shacl constraints, a specific family of queries, in presence of an ontology. We developed a refined chase technique, producing for each ontology a minimal model, i.e., a labeled graph, in which we can evaluateshacl constraints. However, this technique might still produce infinite models. This can be avoided by rewriting theshacl constraints with respect to the ontology, resulting in a standalone set ofshacl constraints that can directly be verified only over the data; our second contribution. 
Ali Enayat (University of Gothenburg)
Arithmetic and set theory through the lens of interpretability
The notion of (relative) interpretation for first order theories was introduced in a landmark 1953 monograph by Alfred Tarski, Andrzej Mostowski and Raphael Robinson, where it was developed as a powerful tool for establishing undecidability results. By now the domain of interest and applicability of interpretability theory far exceeds undecidability theory owing to its multifaceted interactions with both proof theory and model theory. Special attention will be paid to recent advances in the subject that indicate the distinctive character of Peano Arithmetic, ZermeloFraenkel set theory, and their higher order analogues in the realm of interpretability theory. This talk will present a personal overview of the interpretability analysis of arithmetical and set theoretical theories.

Orvar Lorimer Olsson (FLoV)
The propositional logic of teams
Starting from a logic given by traditional semantics formulated in terms of semantic objects (assignments, valuations or worlds) team semantics lifts the denotations of formulas to sets, or teams, of semantic objects instead enabling the formulation of properties, such as variable dependency, not available in the traditional setting. Since the introduction by Hodges, and refinement by Väänänen, team semantic constructions have been used to generate expressively enriched logics still conserving nice properties, such as compactness or decidability. In contrast these logics fail to be substitutional, limiting any algebraic treatment, and rendering fully schematic proof systems impossible. This shortcoming can be attributed to the flatness principle, commonly adhered to when generating team semantics.
Investigating the formation of team logics from an algebraic perspective, and disregarding the flatnessprinciple, I will present the logic of teams (LT), a substitutional logic for which important propositional team logics are axiomatisable as fragments. Starting from classical propositional logic and Boolean algebras, we give semantics for LT by considering algebras of the form P(B) being the powerset of a Boolean algebra B, treated with treated with an internal (derived from B) and an external (settheoretic) set of connectives. Furthermore, we present a wellmotivated labelled natural deduction system for LT, for which a further analysis motivates a generalisation to constructions of logics by combinations of an internal and an external logic, where for LT both are classical propositional logic.
This is joint work with Fredrik Engström.

Sven Ove Hansson (KTH)
How to combine probabilities and full beliefs in a formal system
One of the major problems in formal epistemology is the difficulty of combining probabilistic and full (dichotomous, allornothing) beliefs in one and the same formal framework. Major properties of actual human belief systems, including how they are impacted by our cognitive limitations, are used to introduce a series of desiderata for realistic models of such belief systems. This leads to a criticism of previous attempts to combine representations of both probabilistic and full beliefs in one and the same formal model. Furthermore, a formal model is presented in which this is done differently. One of its major features is that contingent propositions can be transferred in both directions between full beliefs and lower degrees of belief, in a way that mirrors reallife acquisitions and losses of full beliefs. The subsystem consisting of full beliefs has a pattern of change that constitutes a credible system of dichotomous belief change.

Licentiate defence: Tjeerd Fokkens (FLoV)
Modelling the logical mind – Using the cognitive architecture ACTR to model human symbolic reasoning in the description logic ALE
Public defence of Tjeerd Fokkens’ Licentiate thesis.
Opponent Dr Ing Stefan Borgwardt, Technische Universität Dresden
Examiner Professor Simon Dobnik, Göteborgs universitet 
Graham Leigh (FLoV)
Coinductive Proof Theory
I will present recent results and work in progress on adapting proof theoretic methods to nonwellfounded notions of proof.

Vann McGee (MIT)
Boolean Degrees of Truth and Classical Rules of Inference
Compositional semantics that acknowledge vagueness by positing degrees of truth intermediate between truth and falsity can retain classical sentential calculus, provided the degrees form a Boolean algebra. A valid deduction guarantees that the degree of truth of the conclusion be at least as great as every lower bound on the degrees of the premises. If we extend the language to allow infinite disjunctions and conjunctions, the Boolean algebra will need to be complete and atomic. If we extend further by adding quantifiers ranging over a fixed domain, we get the supervaluations proposed by Bas van Fraassen.

Vlad Lazar (FLoV)
An introduction to (classical) Realizability
I will present some of the fundamental aspects of classical realizability. Firstly, we will have a brief look into the history and motivation behind the study of realizability, starting from the Brouwer–Heyting–Kolmogorov interpretation of intuitionistic logic and Kleene’s original number realizability. Afterwards we will examine how these ideas can be adapted to classical logic by exploring the mechanisms behind Krivine’s classical realizability. This talk is the result of a reading course in the Master of Logic programme.