Welcome to the webpage of the logic group at the University of Gothenburg. Information about our research and activities can be found through the links to the left. More detailed information is available through the personal pages of group members and our homepage at the University of Gothenburg.
Cyclic (or circular) proofs are now a common technique for demonstrating metalogical properties of systems incorporating (co)induction, including modal logics, predicate logics, type systems and algebras. Inspired by automaton theory, cyclic proofs encode a form of self-dependency of which induction/recursion comprise special cases. An overarching question of the area, the so-called ‘Brotherston-Simpson conjecture’, asks to what extent the converse holds.
We employ the lens provided by formal truth theory to study axiomatizations of PA (Peano Arithmetic). More specifically, let EA (Elementary Arithmetic) be the fragment I∆0 + Exp of PA, and CT−[EA] be the extension of EA by the commonly studied axioms of compositional truth CT−. The truth theory delivers a natural preorder on the set of axiomatizations: an axiomatization A is greater or equal to an axiomatization B if and only if, over CT-[EA], the assertion “All axioms from A are true” implies “All axioms from B are true”. Our focus is dominantly on two types of axiomatizations, namely: (1) schematic axiomatizations that are deductively equivalent to PA, and (2) axiomatizations that are proof-theoretically equivalent to the canonical axiomatization of PA.