215 research outputs found
On the relationship between hypersequent calculi and labelled sequent calculi for intermediate logics with geometric Kripke semantics
No full textIn this thesis we examine the relationship between hypersequent and some types of labelled sequent calculi for a subset of intermediate logics—logics between intuitionistic (Int), and classical logics—that have geometric Kripke semantics, which we call Int∗/Geo.
We introduce a novel calculus for a fragment of first-order classical logic, which
we call partially-shielded formulae (or PSF for short), that is adequate for expressing
the semantic validity of formulae in Int∗/Geo, and apply techniques from correspondence theory to provide translations of hypersequents, simply labelled sequents and relational sequents (simply labelled sequents with relational formulae) into PSF. Using these translations, we show that hypersequents and simply labelled sequents for calculi in
Int∗/Geo share the same models. We also use these translations to justify various techniques that we introduce for translating simply labelled sequents into relational sequents and vice versa. In particular, we introduce a technique called "transitive unfolding" for translating relational sequents into simply labelled sequents (and by extension, hypersequents) which preserves linear models in Int∗/Geo.
We introduce syntactic translations between hypersequent calculi and simply labelled
sequent calculi. We apply these translations to a novel hypersequent framework HG3ipm∗
for some logics in Int∗/Geo to obtain a corresponding simply labelled sequent framework LG3ipm∗, and to an existing simply labelled calculus for Int from the literature to obtain a novel hypersequent calculus for Int.
We introduce methods for translating a simply labelled sequent calculus into a cor-
responding relational calculus, and apply these methods to LG3ipm∗ to obtain a novel
relational framework RG3ipm∗ that bears similarities to existing calculi from the literature. We use transitive unfolding to translate proofs in RG3ipm∗ into proofs in LG3ipm∗ and HG3ipm∗ with the communication rule, which corresponds to the semantic restriction to linear models
A Cut-Free Simple Sequent Calculus for Modal Logic S5
No full textInternational audienceIn this paper, we present a simple sequent calculus for the modal propositional logic S5. We prove that this sequent calculus is theoremwise equivalent to the Hilbert-style system S5, that it is contraction-free and cut-free, and finally that it is decidable. All results are proved in a purely syntactic way
Lambda Terms for Natural Deduction, Sequent Calculus and Cut Elimination
No full textIt is well-known that there is a good correspondence between natural deduction derivations and typed lambda terms. Moreover normalizing these terms is equivalent to eliminating cuts in the corresponding sequent calculus derivations. Several papers have been written on this topic. The correspondence between sequent calculus derivations and natural deduction derivations is, however, not a one-to-one map. This causes some syntactic technicalities. The correspondence is best explained by two extensionally equivalent type assignment systems for untyped lambda terms, one corresponding to natural deduction (N) and the other to sequent calculus (L). These two systems constitute different grammars for generating the same (type assignment relation for untyped) lambda terms. The second grammar is ambiguous, but the first one is not. This fact explains the many-one correspondence mentioned above. Moreover, the second type assignment system has a `cut--free' fragment (L cf ). This fragment genera..
A Sequent Calculus for Compact Closed Categories
No full textIn this paper, we introduce the system CMLL of sequent calculus and establish its correspondence with compact closed categories. CMLL is equivalent in provability to the system MLL of classical linear logic with the tensor and par connectives identified. We show that the system allows a fairly simple cut-elimination, and the proofs in the system have a natural interpretation in compact closed categories. However, the soundness of the cut-elimination procedure in terms of the categorical interpretation is by no means evident. We answer to this question affirmatively and establish the soundness by using the coherence result on compact closed categories by Kelly and Laplaza. 1 Introduction In this paper, we introduce the system CMLL of sequent calculus and establish its correspondence with compact closed categories. CMLL is equivalent in provability to the system MLL of classical linear logic with the tensor ffl and par O connectives identified. Compact closed categories are abundant in ..
Non-commutative logic II: sequent calculus and phase semantics
No full textNon-commutative logic, which is an unification of commutative linear logic and cyclic linear logic, is extended to all linear connectives: additives, exponentials and constants. We give two equivalent versions of the sequent calculus --- directly with the structure of series-parallel order varieties, and with their presentations as partial orders ---, phase semantics and a cut elimination theorem. Contents 1 Introduction 2 2 Sequent calculus : first version 5 2.1 Language . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.2 Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3 Order varieties 12 3.1 Order varieties and orders . . . . . . . . . . . . . . . . . . . . 12 3.2 Series-parallel order varieties . . . . . . . . . . . . . . . . . . 14 3.3 Characterization of series-parallel order varieties . . . . . . . 16 Post-doctoral fellowship from the INRIA. This research was pa..
A Contraction-free and Cut-free Sequent Calculus for Propositional Dynamic Logic
No full textInternational audienceIn this paper we present a sequent calculus for propositional dynamic logic built using an enriched version of the tree-hypersequent method and including an infinitary rule for the iteration operator. We prove that this sequent calculus is theoremwise equivalent to the corresponding Hilbert-style system, and that it is contraction-free and cut-free. All results are proved in a purely syntactic way
Multi Lingual Sequent Calculus and Coherent Spaces
No full textWe study a Gentzen style sequent calculus where the formulas on the left and right of the turnstile need not necessarily come from the same logical system. Such a sequent can be seen as a consequence between different domains of reasoning. We discuss the ingredients needed to set up the logic generalized in this fashion. The usual cut rule does not make sense for sequents which connect different logical systems because it mixes formulas from antecedent and succedent. We propose a different cut rule which addresses this problem. The new cut rule can be used as a basis for composition in a suitable category of logical systems. As it turns out, this category is equivalent to coherent spaces with certain relations between them. Finally, cut elimination in this set-up can be employed to provide a new explanation of the domain constructions in Samson Abramsky's Domain Theory in Logical Form. Key words: Sequent calculus, coherent spaces 1 Introduction This paper attempts to provide a new ana..
A sequent calculus for type theory
No full textBased on natural deduction, Pure Type Systems (PTS) can express a wide range of type theories. In order to express proof-search in such theories, we introduce the Pure Type Sequent Calculi (PTSC) by enriching a sequent calculus due to Herbelin, adapted to proof-search and strongly related to natural deduction. PTSC are equipped with a normalisation procedure, adapted from Herbelin’s and defined by local rewrite rules as in Cut-elimination, using explicit substitutions. It satisfies Subject Reduction and it is confluent. A PTSC is logically equivalent to its corresponding PTS, andtheformer is strongly normalising if and only if the latter is. We show how the conversion rules can be incorporated inside logical rules (as in syntax-directed rules for type checking), so that basic proofsearch tactics in type theory are merely the root-first application of our inference rules
A cut-free sequent calculus for the bi-intuitionistic logic 2Int
No full textThe purpose of this paper is to introduce a bi-intuitionistic sequent calculus and to give proofs of admissibility for its structural rules. The calculus I will present, called SC2Int, is a sequent calculus for the bi-intuitionistic logic 2Int, which Wansing presents in [2016a]. There he also gives a natural deduction system for this logic, N2Int, to which SC2Int is equivalent in terms of what is derivable. What is important is that these calculi represent a kind of bilateralist reasoning, since they do not only internalize processes of verifcation or provability but also the dual processes in terms of falsifcation or what is called dual provability. In [Wansing, 2017] a normal form theorem for N2Int is stated, here, I want to prove a cut-elimination theorem for SC2Int, i.e., if successful, this would extend the results existing so far
Non-commutative logic II: sequent calculus and phase semantics
No full textNon-commutative logic, which is a unification of commutative linear logic and cyclic linear
logic, is extended to all linear connectives: additives, exponentials and constants. We give two
equivalent versions of the sequent calculus (directly with the structure of order varieties, and
with their presentations as partial orders), phase semantics and a cut-elimination theorem.
This involves, in particular, the study of the entropy relation between partial orders, and the
introduction of a special class of order varieties: the series–parallel order varieties.</jats:p
- …
