We study cyclic proof systems for $μ\mathsf{PA}$, an extension of Peano arithmetic by positive inductive definitions that is arithmetically equivalent to the (impredicative) subsystem of second-order arithmetic $Π^1_2$-$\mathsf{CA}_0$ by Möllefeld. The main result of this paper is that cyclic and inductive $μ\mathsf{PA}$ have the same proof-theoretic strength. First, we translate cyclic proofs into an annotated variant based on Sprenger and Dam's systems for first-order $μ$-calculus, whose stronger validity condition allows for a simpler proof of soundness. We then formalise this argument within $Π^1_2$-$\mathsf{CA}_0$, leveraging Möllerfeld's conservativity properties. To this end, we build on prior work by Curzi and Das on the reverse mathematics of the Knaster-Tarski theorem. As a byproduct of our proof methods we show that, despite the stronger validity condition, annotated and "plain" cyclic proofs for $μ\mathsf{PA}$ prove the same theorems. This work represents a further step in the non-wellfounded proof-theoretic analysis of theories of arithmetic via impredicative fragments of second-order arithmetic, an approach initiated by Simpson's Cyclic Arithmetic, and continued by Das and Melgaard in the context of arithmetical inductive definitions.

Circular (or cyclic ) proofs have received increasing attention in recent years and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common ‘recursion schemes’. This article attempts to bridge the gap between circular proofs and implicit computational complexity (ICC). Namely, we introduce a circular proof system based on Bellantoni and Cook’s famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way, we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.

We study the computational expressivity of proof systems with fixed point operators, within the 'proofs-as-programs' paradigm. We start with a calculus muLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, muLJ admits a standard extension to a 'circular' calculus CmuLJ. Our main result is that, perhaps surprisingly, both muLJ and CmuLJ represent the same first-order functions: those provably total in $Π^1_2$-$\mathsf{CA}_0$, a subsystem of second-order arithmetic beyond the 'big five' of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points. For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to $Π^1_2$-$\mathsf{CA}_0$ (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within $Π^1_2$-$\mathsf{CA}_0$ in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.

We investigate non-wellfounded proof systems based on parsimonious logic, a weaker variant of linear logic where the exponential modality ! is interpreted as a constructor for streams over finite data. Logical consistency is maintained at a global level by adapting a standard progressing criterion. We present an infinitary version of cut-elimination based on finite approximations, and we prove that, in presence of the progressing criterion, it returns well-defined non-wellfounded proofs at its limit. Furthermore, we show that cut-elimination preserves the progressing criterion and various regularity conditions internalizing degrees of proof-theoretical uniformity. Finally, we provide a denotational semantics for our systems based on the relational model.

Trust is an extremely helpful construct when reasoning under uncertainty. Thus, being able to logically formalize the concept in a suitable language is important. However, doing so is problematic for three reasons. First, in order to keep track of the contextual nature of trust, situation trackers are required inside the language. Second, in order to produce trust estimations, agents rely on evidence personally gathered or reported by other agents; this requires elements in the language that can track which agents are used as referrals and how much weight is placed on their opinions. Finally, trust is subjective in nature, thus, personal thresholds are needed to track the trust-propensity of different evaluators. In this paper we propose an interpretation of a probabilistic modal language à la Hennessy-Milner in order to capture a context-aware quantitative notion of trust based on evidence. We also provide an axiomatization for the language and prove soundness, completeness, and decidability results.

Cyclic and non-wellfounded proofs are now increasingly employed to establish metalogical results in a variety of settings, in particular for type systems with forms of (co)induction. Under the Curry-Howard correspondence, a cyclic proof can be seen as a typing derivation 'with loops', closer to low-level machine models, and so comprise a highly expressive computational model that nonetheless enjoys excellent metalogical properties. In recent work, we showed how the cyclic proof setting can be further employed to model computational complexity, yielding characterisations of the polynomial time and elementary computable functions. These characterisations are 'implicit', inspired by Bellantoni and Cook's famous algebra of safe recursion, but exhibit greater expressivity thanks to the looping capacity of cyclic proofs. In this work we investigate the capacity for non-wellfounded proofs, where finite presentability is relaxed, to model non-uniformity in complexity theory. In particular, we present a characterisation of the class $\mathsf{FP/poly}$ of functions computed by polynomial-size circuits. While relating non-wellfoundedness to non-uniformity is a natural idea, the precise amount of irregularity, informally speaking, required to capture $\mathsf{FP/poly}$ is given by proof-level conditions novel to cyclic proof theory. Along the way, we formalise some (presumably) folklore techniques for characterising non-uniform classes in relativised function algebras with appropriate oracles.

We study the computational expressivity of proof systems with fixed point operators, within the ‘proofs-as-programs’ paradigm. We start with a calculus μLJ (due to Clairambault) that extends intuitionistic logic by least and greatest positive fixed points. Based in the sequent calculus, μLJ admits a standard extension to a ‘circular’ calculus CμLJ.Our main result is that, perhaps surprisingly, both μLJ and CμLJ represent the same first-order functions: those provably total in $\Pi _2^1 - {\text{C}}{{\text{A}}_0}$, a subsystem of second-order arithmetic beyond the ‘big five’ of reverse mathematics and one of the strongest theories for which we have an ordinal analysis (due to Rathjen). This solves various questions in the literature on the computational strength of (circular) proof systems with fixed points.For the lower bound we give a realisability interpretation from an extension of Peano Arithmetic by fixed points that has been shown to be arithmetically equivalent to $\Pi _2^1 - {\text{C}}{{\text{A}}_0}$ (due to Möllerfeld). For the upper bound we construct a novel computability model in order to give a totality argument for circular proofs with fixed points. In fact we formalise this argument itself within $\Pi _2^1 - {\text{C}}{{\text{A}}_0}$ in order to obtain the tight bounds we are after. Along the way we develop some novel reverse mathematics for the Knaster-Tarski fixed point theorem.

Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common ‘recursion schemes’.

We consider the probabilistic applicative bisimilarity (PAB) --- a coinductive relation comparing the applicative behaviour of probabilistic untyped λ-terms according to a specific operational semantics. This notion has been studied by Dal Lago et al. with respect to the two standard parameter passing policies, call-by-value (cbv) and call-by-name (cbn), using a lazy reduction strategy not reducing within the body of a function. In particular, PAB has been proven to be fully abstract with respect to the contextual equivalence in cbv [6] but not in lazy cbn [16].