arXiv subjects

Graham E. Leigh

Publications and source records attributed to Graham E. Leigh.

11 recordsLinked to original sources

arXiv2026

Making progress: Reducibility Candidates and Cut Elimination in the Ill-founded Realm

Ill-founded (or non-wellfounded) proof systems have emerged as a natural framework for inductive and coinductive reasoning. In such systems, soundness relies on global correctness criteria, such as the progressivity condition. Ensuring that these criteria are preserved under infinitary cut elimination remains a central technical challenge in ill-founded proof theory. In this paper, we present two cut elimination arguments for ill-founded $μ\mathsf{MALL}$ - a fragment of linear logic extended with fixed-points - based on the reducibility candidates technique of Tait and Girard. In both arguments, preservation of progressivity follows directly from the defining properties of the reducibility candidates. In particular, the second argument is derived from the topological notion of internally closed set developed in previous work by Afshari and Leigh.

cs.LO↗

arXiv2025

The Limit of Recursion in State-based Systems

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 the previously claimed result by the first and third authors on closure ordinals of the alternation-free mu-calculus in [3]. The new approach sees a reincarnation of Kozen's well-annotations, devised for showing the finite model property for the modal mu-calculus. We develop a theory of 'conservative' well-annotations where minimality of annotations is guaranteed, and isolate parts of the structure that locally determine the closure ordinal of relevant formulas. This adoption of well-annotations enables a direct and clear pumping process that rules out closure ordinals between omega^2 and the limit of countability.

cs.LO↗

arXiv2025

Demystifying $μ$

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 a novel bridge between finitary, cyclic and illfounded conceptions of proof and re-enforces the importance of two normal form theorems for the logic: guardedness and disjunctiveness.

math.LO↗

arXiv2025

Unravelling Cyclic First-Order Arithmetic

Cyclic proof systems for Heyting and Peano arithmetic eschew induction axioms by accepting proofs which are finite graphs rather than trees. Proving that such a cyclic proof system coincides with its more conventional variants is often difficult: Previous proofs in the literature rely on intricate arithmetisations of the metamathematics of the cyclic proof systems. In this article, we present a simple and direct embedding of cyclic proofs for Heyting and Peano arithmetic into purely inductive, i.e. 'finitary', proofs by adapting a translation introduced by Sprenger and Dam for a cyclic proof system of $μ\text{FOL}$ with explicit ordinal approximations. We extend their method to recover Das' result of $\text{C}Π_n \subseteq \text{I}Π_{n + 1}$ for Peano arithmetic. As part of the embedding we present a novel representation of cyclic proofs as a labelled sequent calculus.

math.LO↗

arXiv2025

Tarskian Theories of Krivine's Classical Realisability

This paper presents a formal theory of Krivine's classical realisability interpretation for first-order Peano arithmetic ($\mathsf{PA}$). To formulate the theory as an extension of $\mathsf{PA}$, we first modify Krivine's original definition to the form of number realisability, similar to Kleene's intuitionistic realisability for Heyting arithmetic. By axiomatising our realisability with additional predicate symbols, we obtain a first-order theory $\mathsf{CR}$ which can formally realise every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ``realisability implies truth'' results in $\mathsf{CR}$ being essentially equivalent to the Tarskian theory $\mathsf{CT}$ of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. Thus, $\mathsf{CT}$ can be considered a formal theory of classical realisability. We also prove that a weaker reflection principle which preserves the distinction between realisability and truth is sufficient for $\mathsf{CR}$ to achieve the same strength as $\mathsf{CT}$. Furthermore, we formulate transfinite iterations of $\mathsf{CR}$ and its variants, and then we determine their proof-theoretic strength.

math.LO↗

arXiv2025

A Friedman--Sheard-style Theory for Classical Realisability

In Hayashi and Leigh (2024), the authors formulate classical number realisability for first-order arithmetic and a corresponding axiomatic system based on Krivine's classical realisability interpretation. This paper presents a self-referential generalisation of previous results in the spirit of Friedman and Sheard (1987).

math.LO↗

arXiv2023

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

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 'proofs', known as a the soundness condition. This soundness condition frequently takes the form of either a global trace condition, a property dependent on all infinite paths in the proof-graph, or a reset condition, a 'local' condition depending on the simple cycles only which, as a result, is typically stable under more proof transformations. In this article we present a general method for constructing cyclic proof systems with reset condition from cyclic proof with global trace conditions. In contrast to previous approaches, this method of generation is entirely independent of logic's semantics, only relying on combinatorial aspects of the notion of 'trace' and 'progress'. We apply this method to present reset proof systems for three cyclic proof systems from the literature: cyclic arithmetic, cyclic Gödel's T and cyclic tableaux for the modal μ-calculus.

math.LO↗

arXiv2021

Revisiting the conservativity of fixpoints over intuitionistic arithmetic

This paper presents a novel proof of the conservativity of the intuitionistic theory of strictly positive fixpoints, $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$, over Heyting arithmetic (HA), originally proved in full generality by Arai (2011). The proof embeds $\widehat{\mathrm{ID}}{}_{1}^{\mathrm{i}}$ into the corresponding theory over Beeson's logic of partial terms and then uses two consecutive interpretations, a realizability interpretation of this theory into the subtheory generated by almost negative fixpoints, and a direct interpretation into Heyting arithmetic with partial terms using a hierarchy of satisfaction predicates for almost negative formulae. It concludes by applying van den Berg and van Slooten's result (2018) that Heyting arithmetic with partial terms plus the schema of self realizability for arithmetic formulae is conservative over HA.

math.LO↗

arXiv2021

The Copernican Multiverse of Sets

We develop an untyped framework for the multiverse of set theory. $\mathsf{ZF}$ is extended with semantically motivated axioms utilizing the new symbols $\mathsf{Uni}(\mathcal{U})$ and $\mathsf{Mod}(\mathcal{U, σ})$, expressing that $\mathcal{U}$ is a universe and that $σ$ is true in the universe $\mathcal{U}$, respectively. Here $σ$ ranges over the augmented language, leading to liar-style phenomena that are analysed. The framework is both compatible with a broad range of multiverse conceptions and suggests its own philosophically and semantically motivated multiverse principles. In particular, the framework is closely linked with a deductive rule of Necessitation expressing that the multiverse theory can only prove statements that it also proves to hold in all universes. We argue that this may be philosophically thought of as a Copernican principle that the background theory does not hold a privileged position over the theories of its internal universes. Our main mathematical result is a lemma encapsulating a technique for locally interpreting a wide variety of extensions of our basic framework in more familiar theories. We apply this to show, for a range of such semantically motivated extensions, that their consistency strength is at most slightly above that of the base theory $\mathsf{ZF}$, and thus not seriously limiting to the diversity of the set-theoretic multiverse. We end with case studies applying the framework to two multiverse conceptions of set theory: arithmetic absoluteness and Joel D. Hamkins' multiverse theory.

math.LO↗

arXiv2016

On the Herbrand content of LK

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-deterministic tree grammar of order 2 which generates a finite language of first-order terms that appear in the Herbrand expansions obtained through cut-elimination. In particular, for every Gentzen-style reduction between LK-proofs we study the induced grammars and classify the cases in which language equality and inclusion hold.

cs.LO↗

arXiv2013

Conservativity for theories of compositional truth via cut elimination

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 weak subsystem of arithmetic. In doing so we also fix a critical error in Halbach's original presentation. Our methods show that the admission of these axioms determines a hyper-exponential reduction in the size of derivations of truth-free statements.

math.LO↗