Abstract We present an intuitionistic counterpart of the modal $$\mu $$ μ -calculus formulated with the binary Lewis arrow, a generalisation of the $$\Box $$ □ -operator. Using Ruitenburg’s theorem, we prove that every formula is equivalent to a guarded one. We then provide a sound and complete non-wellfounded proof system for the logic that is cut-free, and obtain as a corollary that the logic is decidable and admits a cyclic proof system. A game semantics for the logic is developed which acts as a mediator between the formal proof system and the relational semantics.

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.

Abstract Cyclic proof systems permit derivations that are finite graphs in contrast to conventional derivation trees. The soundness of such proofs is ensured by imposing a soundness condition on derivations. The most common such condition is the global trace condition (GTC), a condition on the infinite paths through the derivation graph. To give a uniform treatment of such cyclic proof systems, Brotherston proposed an abstract notion of trace. We extend Brotherston’s approach into a category theoretical rendition of cyclic derivations, advancing the framework in two ways: first, we introduce activation algebras which allow for a more natural formalisation of trace conditions in extant cyclic proof systems. Second, accounting for the composition of trace information allows us to derive novel results about cyclic proofs, such as introducing a Ramsey-style trace condition. Furthermore, we connect our notion of trace to automata theory and prove that verifying the GTC for abstract cyclic proofs with certain trace conditions is PSPACE-complete.

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.

Beckmann [1] derives bounds on the length of reduction chains of classes of simply typed λ-calculus terms which are exact up-to a constant factor in their highest exponent. Afshari et al. [2] obtain similar bounds on acyclic higher-order recursion schemes (HORS) by embedding them in the simply typed λ-calculus and applying Beckmann's result. In this article, we apply Beckmann's proof strategy directly to acyclic HORS, proving exactness of the bounds on reduction chain length and obtaining exact bounds on the size of languages generated by acyclic HORS.

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.

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.

This article extends Post's; programme to finite levels of the Ershov hierarchy of Δ2 sets. Our initial characterization, in the spirit of Post (1994, Bulletin of the American Mathematical Society, 50, 284–316), of the degrees of the immune and hyperimmune n-enumerable sets leads to a number of results setting other immunity properties in the context of the Turing and wtt-degrees derived from the Ershov hierarchy. For instance, we show that any n-enumerable hyperhyperimmune set must be co-enumerable, for each n ≥ 2. The situation with regard to the wtt-degrees is particularly interesting, as demonstrated by a range of results concerning the wtt-predecessors of hypersimple sets. Finally, we give a number of results directed at characterizing basic classes of n-enumerable degrees in terms of natural information content. For example, a 2-enumerable degree contains a 2-enumerable dense immune set iff it contains a 2-enumerable r-cohesive set iff it bounds a high enumerable set. This result is extended to a characterization of n-enumerable degrees which bound high enumerable degrees. Furthermore, a characterization for n-enumerable degrees bounding only low2 enumerable degrees is given.