ABSTRACT. Reasoning involving notions of dependence and independence occurs in a variety of situations, and it is of interest to study dependence and independence as basic logical concepts in their own right. Indeed, this desideratum has been one motivation for the development of the "independence friendly logic" of Hintikka, and for the "dependence logic" programme of Väänänen. In the talk I will show that certain sheaf models naturally support an extension of classical logic with independence relations, leading to logical principles for reasoning about independence. No prior knowledge of sheaf theory will be assumed.

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. 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. 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. 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. 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 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. We revisit the symmetric mu-mutilde-framework introduced by Curien and Herbelin (later baptised System L by Munch-Maccagnoni) from the perspective of fibred category theory, i.e. using fibred spans and cospans and their relation to (CAT-valued) distributors. The mu-mutilde-framework provides direct computational interpretations for proofs in variants of Gentzen’s classical (multi-conclusioned) sequent calculus LK, exhibiting a duality between call-by-name and call-by-value evaluation. Not globally fixing an evaluation strategy however gives rise to a non-confluent critical pair. This problem has been further analyzed by Munch-Maccagnoni via polarized linear logic and the notion of duploid, where the critical pair is exposed as a failure of associativity of composition. One important motivation to revisit duploids and the mu-mutilde-framework from the perspective of fibred category theory is to understand these in a setting where usually dependent type theories are interpreted and to consider what kind of dependencies might be appropriate for such a symmetric system beyond a mere combination with ”usual” asymmetric intuitionistic dependent types. This question leads in a natural way to consider co- and contravariant reindexing, thereby providing for example a fresh perspective on the mu-mutilde-critical pair as choice between the two notions of reindexing, left and right sequent calculus rules as left and right actions (like for module structures in algebra) and polarity shifts as related to (op)cartesian liftings. It also suggests a refinement of the notions of “call-by-name” and “call-by-value”. This is still work in progress, and feedback will be appreciated.

ABSTRACT. This paper gives a denotational model to the typed lambda-mu calculus. In this model, absurdy type $\bot$ is interpreted as the type of truth values, and each type is divided into infinitely many ranks, each of which forms a Boolean algebra. The double-negation elimination, the signature deduction rule of classical logic, is interpreted as a move from a member of domain $D$ of type $\neg \neg A (= (A \to \bot) \to \bot)$, rank $\leq n$ to a member of domain $D'$ of type $A$, rank $\leq n+1$. $\mu$-variables are interpreted as variables ranging over a certain restricted domain.

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.