Seminars
Seminars, workshops and other events organised by our group
The Logic Group runs a bi-weekly Research Seminar in Logic, monthly Nordic Online Logic Seminar and the annual Lindström Lecture series, as well as other events. See below for a list of recent and upcoming events or follow the links to jump straight to a category.
The research seminar in Logic meets on alternate Fridays at 10.15. Unless otherwise stated, seminars are held at the department building (Humanisten). Details of online talks are distributed in the GU Logic mailing list. Alternatively, contact Graham E Leigh directly.
-
-
The problem of optimising automated explanations for entailments in knowledge bases is tackled by modelling deductive reasoning processes using the cognitive architecture ACT-R. This results in the model SHARP which simulates a tableau algorithm for deciding inconsistency of an ABox in the description logic 𝒜ℒℰ as executed by a human. SHARP enables predicting the inference time of this task, which is assumed to reflect human performance. With the inference time, two complexity measures on ABoxes are defined that cognitively adequate by design.
Opponent: Jakub Szymanik, Associate professor in the Center for Brain/Mind Sciences and the Computer Science Department at the University of Trento.
-
Frame definability is a well-studied notion for a plethora of logics: a class of frames is defined by a set of formulas if and only if such formulas are validities for all and only the frames in such class.
In this talk, I will present a series of results about frame definability in a fragment of conditional logic. Conditional logic is an extension of propositional logic that includes a binary “counterfactual” conditional operator \(\leadsto\). We specifically make the following choices: (i), we consider the non-nested fragment of conditional logic (i.e., where conditionals are not allowed in the scope of other conditionals), and (ii), we consider only finite posets as the underlying structure of the models of our logic. Given these assumptions, a formula of the form \(\varphi \leadsto \psi\) is intuitively true if the consequent \(\psi\) is true in all the minimal (with respect to the partial order of the poset) worlds where the antecedent \(\varphi\) is true. Via these semantics, this fragment of conditional logic becomes relevant in several fields, such as default reasoning and belief revision.
I will present the following results: (i) a set of non-nested conditional formulas each defining a different class of finite posets; (ii) a characterization theorem identifying the classes of finite posets that can be defined by a non-nested conditional formula; and (iii), a Sahlqvist-like theorem proving that every class of finite posets definable via a non-nested conditional formula is definable also by a first-order formula.
This talk is based on the paper Frame Definability in Conditional Logic, a joint work with Damiano Fornasiere and Johannes Marti, which was published at AiML 2024.
-
-
-
-
-
-
What is the meaning of a logical connective? This is a very difficult and controversial question, primarily because its answer depends on the underlying logical framework. In model-theoretic semantics, the meaning of logical connectives is grounded in mathematical structures that define validity in terms of truth. Proof-theoretic semantics (PtS), by contrast, offers an alternative perspective in which truth is replaced by proof. This shift highlights the role of proofs as the foundation for demonstrative knowledge, particularly in mathematical reasoning. Philosophically, PtS aligns with inferentialism, which holds that the meaning of expressions is determined by inference rules. This makes PtS particularly well-suited for understanding reasoning, as it defines logical connectives based on their role in inference.
Base-extension semantics (BeS) is a strand of PtS where proof-theoretic validity is defined relative to a given collection of inference rules regarding basic formulas of the language. Although the BeS project has been successfully developed for intuitionistic propositional logic, first-order classical logic and the multiplicative fragment of linear logic among others, its progression as a comprehensive foundation for logical reasoning is still in its early stages.
In this talk, we will explore Pt-S with a focus on BeS. First, we will introduce an ecumenical perspective to BeS, inspired by Prawitz’s proposal of a system combining classical and intuitionistic logics. The aim is to deepen our understanding of logical reasoning disagreements by investigating the ecumenical approach and developing a unified proof-theoretic foundation for logical reasoning.
We will then address a major challenge in PtS, often called its “original sin”, which is its strong reliance on the natural deduction framework. To overcome this, we propose a version of BeS that employs atomic systems based on sequent calculus rules rather than natural deduction. In this approach, structural rules are treated as properties of atomic systems rather than the logical calculus itself. This allows for a semantics of substructural logics to emerge naturally by modifying the underlying atomic systems. Furthermore, this framework supports a Sandqvist-style completeness proof, but instead of extracting a proof in natural deduction, we obtain one in sequent calculus.
This is based is an ongoing and joint work with Victor Barroso-Nascimento, Luiz Carlos Pereira and Katya Piotrovskaya.
-
We extend homotopy type theory with four extra axioms. The resulting theory should describe the higher topos of light condensed sets. From the axioms, we can prove Markov’s principle, the lesser limited principle of omniscience, and the negation of the weak lesser principle of omniscience. We define a type of open propositions, which induces a topology on each type. With this topology, every map is continuous. We then introduce Stone and compact Hausdorff spaces internally, and the induced topologies on these types are as expected. In particular, we can deduce that all maps from the real unit interval to itself are continuous in the epsilon-delta sense.
This talk is based on a paper submitted to TYPES24, which was authored by Felix Cherubini, Thierry Coquand, Freek Geerligs and Hugo Moeneclaey. The paper is part of the synthetic algebraic geometry project.