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