scholarly journals Metasequents and Tetravaluations

2021 ◽  
Author(s):  
Rohan French
Keyword(s):  
Sequent Calculus

AbstractIn this paper we treat metasequents—objects which stand to sequents as sequents stand to formulas—as first class logical citizens. To this end we provide a metasequent calculus, a sequent calculus which allows us to directly manipulate metasequents. We show that the various metasequent calculi we consider are sound and complete w.r.t. appropriate classes of tetravaluations where validity is understood locally. Finally we use our metasequent calculus to give direct syntactic proofs of various collapse results, closing a problem left open in French (Ergo, 3(5), 113–131 2016).

scholarly journals Sequent calculus as a compiler intermediate language

2016 ◽  
Vol 51 (9) ◽  
pp. 74-88 ◽  
Author(s):  
Paul Downen ◽  
Luke Maurer ◽  
Zena M. Ariola ◽  
Simon Peyton Jones
Keyword(s):  
Sequent Calculus ◽  
Intermediate Language

scholarly journals Deduction in Non-Fregean Propositional Logic SCI

Axioms ◽  
2019 ◽  
Vol 8 (4) ◽  
pp. 115 ◽  
Author(s):  
Joanna Golińska-Pilarek ◽  
Magdalena Welle
Keyword(s):  
Propositional Logic ◽  
Sequent Calculus ◽  
Classical Propositional Logic ◽  
Tableau System ◽  
Soundness And Completeness

We study deduction systems for the weakest, extensional and two-valued non-Fregean propositional logic SCI . The language of SCI is obtained by expanding the language of classical propositional logic with a new binary connective ≡ that expresses the identity of two statements; that is, it connects two statements and forms a new one, which is true whenever the semantic correlates of the arguments are the same. On the formal side, SCI is an extension of classical propositional logic with axioms characterizing the identity connective, postulating that identity must be an equivalence and obey an extensionality principle. First, we present and discuss two types of systems for SCI known from the literature, namely sequent calculus and a dual tableau-like system. Then, we present a new dual tableau system for SCI and prove its soundness and completeness. Finally, we discuss and compare the systems presented in the paper.

scholarly journals On Polymorphic Sessions and Functions

2021 ◽  
Vol 43 (2) ◽  
pp. 1-55
Author(s):  
Bernardo Toninho ◽  
Nobuko Yoshida
Keyword(s):  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Linear Formulation ◽  
Session Types ◽  
Logical Foundation ◽  
Π Calculus ◽  
Soundness And Completeness ◽  
System F ◽  
Algebraic Representations

This work exploits the logical foundation of session types to determine what kind of type discipline for the Λ-calculus can exactly capture, and is captured by, Λ-calculus behaviours. Leveraging the proof theoretic content of the soundness and completeness of sequent calculus and natural deduction presentations of linear logic, we develop the first mutually inverse and fully abstract processes-as-functions and functions-as-processes encodings between a polymorphic session π-calculus and a linear formulation of System F. We are then able to derive results of the session calculus from the theory of the Λ-calculus: (1) we obtain a characterisation of inductive and coinductive session types via their algebraic representations in System F; and (2) we extend our results to account for value and process passing, entailing strong normalisation.

scholarly journals A Sequent Calculus for Subtyping Polymorphic Types

2001 ◽  
Vol 164 (2) ◽  
pp. 345-369 ◽  
Author(s):  
Jerzy Tiuryn
Keyword(s):  
Sequent Calculus

A Sequent Calculus

1994 ◽  
pp. 59-74 ◽  
Author(s):  
H.-D. Ebbinghaus ◽  
J. Flum ◽  
W. Thomas
Keyword(s):  
Sequent Calculus

scholarly journals Mīmāṃsā deontic reasoning using specificity: a proof theoretic approach

2020 ◽  
Author(s):  
Björn Lellmann ◽  
Francesca Gulisano ◽  
Agata Ciabattoni
Keyword(s):  
Deontic Logic ◽  
Sequent Calculus ◽  
Prima Facie ◽  
Theoretic Approach ◽  
Deontic Reasoning ◽  
Complexity Results ◽  
Restricted Form ◽  
Philosophical School ◽  
Decidability And Complexity ◽  
Potential Use

Abstract Over the course of more than two millennia the philosophical school of Mīmāṃsā has thoroughly analyzed normative statements. In this paper we approach a formalization of the deontic system which is applied but never explicitly discussed in Mīmāṃsā to resolve conflicts between deontic statements by giving preference to the more specific ones. We first extend with prohibitions and recommendations the non-normal deontic logic extracted in Ciabattoni et al. (in: TABLEAUX 2015, volume 9323 of LNCS, Springer, 2015) from Mīmāṃsā texts, obtaining a multimodal dyadic version of the deontic logic $$\mathsf {MD}$$ MD . Sequent calculus is then used to close a set of prima-facie injunctions under a restricted form of monotonicity, using specificity to avoid conflicts. We establish decidability and complexity results, and investigate the potential use of the resulting system for Mīmāṃsā philosophy and, more generally, for the formal interpretation of normative statements.

Sign in / Sign up

Export Citation Format

Share Document