activity
20132025
most citedOn the Herbrand content of LK

3 citations · 6 across the 6 of their papers we have counts for

collaborators

7 papers

cs.LO2025

The Limit of Recursion in State-based Systems

Bahareh Afshari, Giacomo Barlucchi, Graham E. Leigh

We prove that omega^2 strictly bounds the iterations required for modal definable functions to reach a fixed point across all countable structures. The result corrects and extends…

math.LO2024★ 1 cited

Demystifying

Bahareh Afshari, Graham E. Leigh, Guillermo Menèndez Turata

We explore the theory of illfounded and cyclic proofs for the propositional modal -calculus. A fine analysis of provability for classical and intuitionistic modal logic provides…

math.LO2023★ 1 cited

From GTC to Reset: Generating Reset Proof Systems from Cyclic Proof Systems

Graham E. Leigh, Dominik Wehr

We consider cyclic proof systems in which derivations are graphs rather than trees. Such systems typically come with a condition that isolates which derivations are admitted as 'pr…

math.LO2021

Revisiting the conservativity of fixpoints over intuitionistic arithmetic

Mattias Granberg Olsson, Graham E. Leigh

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, , over Heyting arithm…

math.LO2020★ 1 cited

The Copernican Multiverse of Sets

Paul K. Gorbow, Graham E. Leigh

We develop an untyped framework for the multiverse of set theory. is extended with semantically motivated axioms utilizing the new symbols …

cs.LO2016★ 3 cited

On the Herbrand content of LK

Bahareh Afshari, Stefan Hetzl, Graham E. Leigh

We present a structural representation of the Herbrand content of LK-proofs with cuts of complexity prenex Sigma-2/Pi-2. The representation takes the form of a typed non-determinis…

math.LO2013

Conservativity for theories of compositional truth via cut elimination

Graham E. Leigh

We present a cut elimination argument that witnesses the conservativity of the compositional axioms for truth (without the extended induction axiom) over any theory interpreting a…