Abstract This paper presents a formal theory of Krivine’s classical realizability 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 realizability, similar to Kleene’s intuitionistic realizability for Heyting arithmetic. By axiomatizing our realizability with additional predicate symbols, we obtain a first-order theory of compositional realizability ($\mathsf{CR}$), which can formally realize every theorem of $\mathsf{PA}$. Although $\mathsf{CR}$ itself is conservative over $\mathsf{PA}$, adding a type of reflection principle that roughly states that ‘realizability implies truth’ results in $\mathsf{CR}$ being essentially equivalent to the Tarskian compositional truth theory ($\mathsf{CT}$) of typed compositional truth, which is known to be proof-theoretically stronger than $\mathsf{PA}$. We also prove that a weaker reflection principle, which preserves the distinction between realizability 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.

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.

Abstract We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

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 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 conditions from systems 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.

Abstract We introduce ill-founded sequent calculi for two intuitionistic linear-time temporal logics. Both logics are based on the language of intuitionistic propositional logic with ‘next’ and ‘until’ operators and are evaluated on dynamic Kripke models wherein the intuitionistic and temporal accessibility relations are assumed to satisfy one of two natural confluence properties: forward confluence in one case, and both forward and backward confluence in the other. The presented sequent calculi are cut-free and incorporate a simple form of formula nesting. Soundness of the calculi is shown by a standard argument and completeness via proof search.

This article examines the computational content of the classical Gentzen sequent calculus. There are a number of well-known methods that extract computational content from first-order logic but applying these to the sequent calculus involves first translating proofs into other formalisms, Hilbert calculi or Natural Deduction for example. A direct approach which mirrors the symmetry inherent in sequent calculus has potential merits in relation to proof-theoretic considerations such as the (non-)confluence of cut elimination, the problem of cut introduction, proof compression and proof equivalence. Motivated by such applications, we provide a representation of sequent calculus proofs as higher order recursion schemes. Our approach associates to an LK proof π of ⇒∃vF, where F is quantifier free, an acyclic higher order recursion scheme H with a finite language yielding a Herbrand disjunction for ∃vF. More generally, we show that the language of H contains all Herbrand disjunctions computable from π via a broad range of cut elimination strategies.

We present two finitary cut-free sequent calculi for the modal μ-calculus. One is a variant of Kozen's axiomatisation in which cut is replaced by a strengthening of the induction rule for greatest fixed point. The second calculus derives annotated sequents in the style of Stirling's `tableau proof system with names' (2014) and features a generalisation of the ν-regeneration rule that allows discharging open assumptions. Soundness and completeness for the two calculi is proved by establishing a sequence of embeddings between proof systems, starting at Stirling's tableau-proofs and ending at the original axiomatisation of the μ-calculus due to Kozen. As a corollary we obtain a new, constructive, proof of completeness for Kozen's axiomatisation which avoids the usual detour through automata and games.

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

The closure ordinal of a formula of modal mu-calculus mu X phi is the least ordinal kappa, if it exists, such that the denotation of the formula and the kappa-th iteration of the monotone operator induced by phi coincide across all transition systems (finite and infinite). It is known that for every alpha < omega^2 there is a formula phi of modal logic such that mu X phi has closure ordinal alpha (Czarnecki 2010). We prove that the closure ordinals arising from the alternation-free fragment of modal mu-calculus (the syntactic class capturing Sigma_2 \cap Pi_2) are bounded by omega^2. In this logic satisfaction can be characterised in terms of the existence of tableaux, trees generated by systematically breaking down formulae into their constituents according to the semantics of the calculus. To obtain optimal upper bounds we utilise the connection between closure ordinals of formulae and embedded order-types of the corresponding tableaux.

Abstract This paper compares the roles classical and intuitionistic logic play in restricting the free use of truth principles in arithmetic. We consider fifteen of the most commonly used axiomatic principles of truth and classify every subset of them as either consistent or inconsistent over a weak purely intuitionistic theory of truth.