ABSTRACT. Urban and Bierman introduced a calculus of proof terms for the sequent calculus LK with a strongly normalizing reduction relation. We extend this calculus to simply-typed higher-order logic with inferences for induction and equality, albeit without strong normalization. We implement this calculus in GAPT, our library for proof transformations. Evaluating the normalization on both artificial and real-world benchmarks, we show that this algorithm is typically several orders of magnitude faster than the existing Gentzen-like cut-reduction, and an order of magnitude faster than any other cut-elimination procedure implemented in GAPT.

ABSTRACT. In pursuit of a canonistic logic comprised of dualized proof rules, we introduce a sequent calculus system, 2Intx, that is inspired by Wansing's bi-intuitionistic propositional logic 2Int. Though 2Int has canonicity and duality, it defines only natural deduction proof rules and employs an unintuitive Kripke semantics that allows atomic formulas to be both true and false. In addition to defining the sequent calculus rules of 2Intx, we also define a Kripke semantics that only admits models in which atomic formulas are either true or false but not both. Finally, we prove soundness of 2Intx.

ABSTRACT. Herbrand's Theorem, a fundamental result of classical logic, states that for every valid existential formula $ \exists x F(x) $ there is a finite set of terms $ T $ such that the quantifier-free disjunction $ \bigvee_{t\in T} F(t) $ is a tautology. Herbrand disjunctions can be computed in a number of ways, such as via cut-elimination, re-interpretations of classical logic in intuitionistic logic and term calculi for classical natural deduction.

In this talk I will outline a language-theoretic representation of Herbrand's Theorem. Specifically, I will introduce a class of higher order recursion schemes (HORS) for computing Herbrand disjunctions from classical sequent calculus proofs. HORS are a generalisation of regular tree grammars to finite types which equate to the simply-typed $\lambda Y$-calculus with non-deterministic reductions. The representation interprets inference rules of proofs as non-terminals whose production rules operate compositionally to extract the term instantiations that result from reductive cut-elimination. Current limitations of the approach, as well as future directions, will be discussed.

ABSTRACT. The logic of constant domains is intuitionistic logic extended with the so-called forall-shift axiom, a classically valid statement which implies the excluded middle over decidable formulas. Surprisingly, this logic is constructive and so far this has been proved by cut-elimination for ad-hoc sequent calculi. Here we use the methods of natural deduction and Curry-Howard correspondence to provide a simple computational interpretation of the logic.

ABSTRACT. The usual reading of logical implication φ → ψ as “if φ then ψ” fails in intuitionistic logic: there are formulas φ and ψ such that φ → ψ is not provable, even though ψ is provable whenever φ is provable. Intuitionistic rules apparently cannot derive interesting meta-properties of the logic and, from a computational perspective, the programs corresponding to intuitionistic proofs are not powerful enough. We propose a term assignment corresponding to the admissible rules of intuitionistic propositional logic, and employ it to study the admissible principles. We provide as an example a study of Kreisel-Putnam logic KP: we give a Curry-Howard correspondence for this system, proving the disjunction property and all the good constructive properties. This is a first step in understanding how to the programs of admissible rules look like.

ABSTRACT. Cyclic pre-proofs can be represented as sets of finite tree derivations with back-links. In the frame of the first-order logic with inductive definitions (FOL$_{\mbox{\scriptsize ID}}$), the nodes of the tree derivations are labelled by sequents and the back-links connect particular terminal nodes, referred to as \emph{buds}, to other nodes labelled by a same sequent. However, only some back-links can constitute sound pre-proofs. Previously, it has been shown that special ordering and derivability conditions, defined along the minimal cycles of the digraphs representing particular normal forms of cyclic pre-proofs, are sufficient for validating the back-links. In that approach, a same constraint could be checked several times when processing different minimal cycles, hence one may require additional recording mechanisms to avoid redundant computation in order to downgrade the time complexity to polynomial.

We present a new approach that does not need to process minimal cycles. It based on a normal form that allows to define the validation conditions by taking into account only the root-bud paths from the non-singleton strongly connected components existing in the digraphs.

ABSTRACT. Cyclic arithmetic, proposed by Simpson '17, is a deduction system based in the language of arithmetic where proofs may be non-wellfounded, as opposed to usual approaches to infinitary proof theory via an omega-rule. Naturally, some form of correctness condition must be imposed to ensure sound reasoning, and this is implemented by a 'trace' condition at the level of the 'flow graph' of the proof (cf. Buss '91). 'Cyclic arithmetic' (CA) itself consists of such proofs that are regular, i.e. that have only finitely many distinct subtrees, and so may be expressed as a finite directed graph (with cycles). It was independently shown by Simpson '17 and Berardi & Tatsuta '17 that CA and PA are equivalent, and recently that logical complexity in the two theories is similar (Das '18).

We consider the issue of cut-elimination for CA. Such a procedure cannot preserve regularity of proofs, so the issue is to show that cut-elimination is 'productive'. To this end, 'continuous' cut-elimination procedures have long been studied in the proof theory of arithmetic, originating from Mints '78. However the difficulties arising from the 'repetition' rule, ensuring continuity, and the need to preserve trace conditions seems to suggest that an alternative approach is pertinent.

In this work-in-progress, we show how cut-elimination can be similarly achieved by a certain reduction to finitary cut-elimination. We compute certain 'runs' through a non-wellfounded proof which must be finite thanks to the trace condition, and show that these are preserved in the image of cut-elimination. Productivity follows since cut-free runs must be non-empty, and validity follows by the finiteness of runs.

The computation of runs, naively, makes use of a semantic oracle, though we believe that this can be replaced by purely syntactic concepts via a 'geometry of interaction' approach to cut-elimination, cf. Girard '89. This would yield a novel proof of the consistency of PA indirectly via CA.

REFERENCES

Berardi & Tatsuta '17. Equivalence of inductive definitions and cyclic proofs under arithmetic. Proceedings of LICS ’17.

Buss '91. The undecidability of k-provability. Annals of Pure and Applied Logic.

Das '18. On the logical complexity of cyclic arithmetic. Preprint.

Girard '89. Towards a geometry of interaction. Proceedings of Categories in Computer Science and Logic.

Mints '78. Finite investigations of transfinite derivations. Journal of Soviet Mathematics.

Simpson '17. Cyclic Arithmetic is Equivalent to Peano Arithmetic. Proceedings of FoSSaCS ’17.