Archive of events from 2025

An archive of events from the year

  • Guillermo Badia (University of Queensland)

    Descriptive Complexity and Weighted Turing Machines

    Fagin’s seminal result characterizing NP in terms of existential second-order logic started the fruitful field of descriptive complexity theory. In recent years, there has been much interest in the investigation of quantitative (weighted) models of computations. In this paper, we start the study of descriptive complexity based on weighted Turing machines over arbitrary semirings. We provide machine-independent characterizations (over ordered structures) of the weighted complexity classes NP[S], FP[S], FPLOG[S], FPSPACE[S], and FPSPACEpoly[S] in terms of definability in suitable weighted logics for an arbitrary semiring S. In particular, we prove weighted versions of Fagin’s theorem (even for arbitrary structures, not necessarily ordered, provided that the semiring is idempotent and commutative), the Immerman–Vardi’s theorem (originally for P) and the Abiteboul–Vianu–Vardi’s theorem (originally for PSPACE). We also discuss a recent open problem proposed by Eiter and Kiesel.

    Recently, the above mentioned weighted complexity classes have been investigated in connection to classical counting complexity classes. Furthermore, several classical counting complexity classes have been characterized in terms of particular weighted logics over the semiring N of natural numbers. In this work, we cover several of these classes and obtain new results for others such as NPMV, ⊕P, or the collection of real-valued languages realized by nondeterministic polynomial-time real-valued Turing machines. Furthermore, our results apply to classes based on many other important semirings, such as the max-plus and the min-plus semirings over the natural numbers which correspond to the classical classes MaxP[O(log n)] and MinP[O(log n)], respectively.

  • World Logic Day Pub Quiz

    The Logic Group at the University of Gothenburg hosts its annual World Logic Day Pub Quiz. For information on World Logic Day events around the world, see http://wld.cipsh.international/wld2025.html.

  • Lukas Melgaard (University of Birmingham)

    Cyclic proofs for arithmetic with least and greatest fixed points

    We investigate the cyclic proof theory of extensions of Peano Arithmetic, in particular µPA, a theory that extends Peano Arithmetic with least and greatest fixed point operators. Our cyclic system CµPA subsumes Simpson’s cyclic arithmetic and the stronger CID<ω. Our main result, which is still work in progress, is that the inductive system µPA and the cyclic system CµPA prove the same arithmetical theorems. We intend to conduct a metamathematical argument for Cyclic Arithmetic to formalize the soundness of cyclic proofs within second-order arithmetic by a form of induction on closure ordinals and then appealing to conservativity results. Since the closure ordinals of our inductive definitions far exceed the recursive ordinals we cannot rely on ordinal notations and must instead formalize a theory of ordinals within second-order arithmetic. This is similar to what is for CID<ω except here we also need to use the reverse mathematics of a more powerful version of Knaster-Tarski.

  • Fredrik Engström (University of Gothenburg)

    Team semantics and substitutional logics

    Team semantics extends traditional semantics by shifting the interpretation of formulas from individual semantic objects (e.g., assignments, valuations, or worlds) to sets of such objects, commonly referred to as teams. This approach enables the expression of properties, such as variable dependency, that are inaccessible in traditional semantics. Since its introduction by Hodges and subsequent refinement by Väänänen, team semantics has been used to develop expressively enriched logics that retain desirable properties such as compactness.

    However, these logics are typically non-substitutional, limiting their algebraic treatment and preventing the development of schematic proof systems. This limitation can be attributed to the flatness principle which is commonly adhered to in many constructions of team semantics for logics.

    In this talk, we approach the formation of propositional logic of teams from an algebraic perspective, explicitly discarding the flatness principle. We propose a substitutional logic of teams that is expressive enough to axiomatize key propositional team logics, such as propositional dependence logic.

    Our construction parallels the algebraic construction of classical propositional logic from Boolean algebras. The algebras we are using are powersets of Boolean algebras equipped with both internal (pointwise) and external (set-theoretic) operations. The resulting logic is clearly substitutional, and is shown to be sound and complete with respect to a labelled natural deduction system.

    If time permits, we will also discuss how we might do to extend this construction to the framework of first-order logic.

  • Freek Geerligs (Chalmers University of Technology)

    A Foundation for Synthetic Stone Duality

    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.

  • Elaine Pimentel (University College London)

    Proof-theoretic semantics: from intuitionism to classical, from natural deduction to sequents

    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.

  • Ivan Di Liberti (Gothenburg University)

    A modular approach to completeness, Beth-definability and Craig interpolation

  • Errol Yuksel (Stockholm University)

    Logic Seminar

  • Peter van Emde Boas and Ghica van Emde Boas (University of Amsterdam; Bronstee)

    Nordic Online Logic Seminar

  • Paula Quinon (Warsaw University of Technology and FLoV)

    Logic Seminar

  • Nordic Online Logic Seminar

  • Logic Seminar

  • Giovanni Varricchione (Utrecht University)

    Defining finite posets via non-nested Conditional Logic

    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 . 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 φψ is intuitively true if the consequent ψ is true in all the minimal (with respect to the partial order of the poset) worlds where the antecedent φ 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.

  • Tjeerd Fokkens (FLoV)

    Modelling the logical mind – Using the cognitive architecture ACT-R to model human symbolic reasoning in the description logic ALE (final seminar)

    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.

  • Hannes Leitgeb (LMU München)

    Nordic Online Logic Seminar

  • Logic Seminar

  • Logic Seminar