Archive of events from 2023

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.

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.

I will present recent results and work in progress on adapting proof theoretic methods to non-well-founded notions of proof.

Public defence of Tjeerd Fokkens’ Licentiate thesis.

Opponent Dr Ing Stefan Borgwardt, Technische Universität Dresden
Examiner Professor Simon Dobnik, Göteborgs universitet

One of the major problems in formal epistemology is the difficulty of combining probabilistic and full (dichotomous, all-or-nothing) 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 real-life 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.

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 flatness-principle, 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 (set-theoretic) set of connectives. Furthermore, we present a well-motivated 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.

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, Zermelo-Fraenkel 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.

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)

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.

Held on 27-28 April, 2023 at the University of Gothenburg, this workshop brought together researchers working on various aspects of fixed point logics and ill-founded 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.

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.

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 co-author 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.

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 well-established areas of logic can advance the state of the art in this emerging field.

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 cut-elimination and how we can transform proofs using inductive reasoning. In this talk, we discuss cut-elimination by resolution, how to extend the method to proof schema, infinite sequences of proofs, and the framework presented in “Schematic Refutations of Formula Schemata.”

In this talk, we introduce a general family of sequent-style 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)

Normal modal logics are closed under conjunctive closure. There are, however, interesting non-normal 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: somebody-knows. While something is general knowledge if it is known by everyone, this notion holds if it is known by someone. Somebody-knows is thus weaker than general knowledge but stronger than distributed knowledge. We introduce a modality for somebody-knows in the style of standard group knowledge modalities, and study its properties. Unlike most other group knowledge modalities, somebody-knows 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 somebody-knows modality, together with a completeness result: the somebody-knows 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 so-called 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.

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.

We investigate non-wellfounded 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 cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressive criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

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 human-robot collaboration.

Compositional theories of truth tend to follow the Tarskian tradition, either the model-theoretic semantics for classical predicate logic or its natural generalisations to many-value and possible-worlds. 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).

Boole, Tarski, Stone, Lawvere, Reyes, Makkai

We prove that ω² 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 alternation-free μ-calculus. The new approach sees a reincarnation of Kozen’s well-annotations, originally devised for showing the finite model property for the modal μ-calculus. We develop a theory of conservative well-annotations where minimality of the annotation is guaranteed, and isolate relevant parts of the structure that necessitate an unfolding of fixed points. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between ω² and the limit of countability.

One quarter of the talk presents background on how facts about entailments and non-entailments 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 (model-theoretic) 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 well-known semantics for IPL, such as Kripke semantics, Beth semantics, Dragalin semantics, topological semantics, and algebraic semantics.

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 non-propositional 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:90-110, 2020. https://doi.org/10.29007/plm4

The model SHARP is a result of (somewhat naively) implementing a tableaux-based reasoning algorithm of the description logic ALE into the cognitive architecture ACT-R. 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.