scholarly journals On semantics of a term calculus for classical logic

2012 ◽  
Vol 92 (106) ◽  
pp. 79-95
Author(s):  
Silvia Likavec ◽  
Pierre Lescanne
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Denotational Semantics ◽  
Proof System ◽  
Cut Elimination ◽  
Kleisli Category

The calculus of Curien and Herbelin was introduced to provide the Curry-Howard correspondence for classical logic. The terms of this calculus represent derivations in the sequent calculus proof system and reduction reflects the process of cut-elimination. We investigate some properties of two well-behaved subcalculi of untyped calculus of Curien and Herbelin, closed under the call-by-name and the call-by-value reduction, respectively. Continuation semantics is given using the category of negated domains and Moggi?s Kleisli category over predomains for the continuation monad. Soundness theorems are given for both versions thus relating operational and denotational semantics. A thorough overview of the work on continuation semantics is given.

On categorical models of classical logic and the Geometry of Interaction

2007 ◽  
Vol 17 (5) ◽  
pp. 957-1027 ◽  
Author(s):  
CARSTEN FÜHRMANN ◽  
DAVID PYM
Keyword(s):  
Classical Logic ◽  
Disjoint Union ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Structural Theory ◽  
Cut Elimination ◽  
Categorical Models ◽  
Boolean Lattices ◽  
Deep Exploration ◽  
Straightforward Proof

It is well known that weakening and contraction cause naive categorical models of the classical sequent calculus to collapse to Boolean lattices. In previous work, summarised briefly herein, we have provided a class of models calledclassical categoriesthat is sound and complete and avoids this collapse by interpreting cut reduction by a poset enrichment. Examples of classical categories include boolean lattices and the category of sets and relations, where both conjunction and disjunction are modelled by the set-theoretic product. In this article, which is self-contained, we present an improved axiomatisation of classical categories, together with a deep exploration of their structural theory. Observing that the collapse already happens in the absence of negation, we start with negation-free models calledDummett categories. Examples of these include, besides the classical categories mentioned above, the category of sets and relations, where both conjunction and disjunction are modelled by the disjoint union. We prove that Dummett categories are MIX, and that the partial order can be derived from hom-semilattices, which have a straightforward proof-theoretic definition. Moreover, we show that the Geometry-of-Interaction construction can be extended from multiplicative linear logic to classical logic by applying it to obtain a classical category from a Dummett category.Along the way, we gain detailed insights into the changes that proofs undergo during cut elimination in the presence of weakening and contraction.

scholarly journals A Binary Quantifier for Definite Descriptions for Cut Free Free Logics

Studia Logica ◽  
2021 ◽  
Author(s):  
Nils Kürbis
Keyword(s):  
Classical Logic ◽  
Final Section ◽  
Sequent Calculus ◽  
Definite Descriptions ◽  
Present Approach ◽  
Cut Elimination ◽  
Free Logic

AbstractThis paper presents rules in sequent calculus for a binary quantifier I to formalise definite descriptions: Ix[F, G] means ‘The F is G’. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of I. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a term forming operator. In the final section rules for I for negative free and classical logic are also mentioned.

On the unification of classical, intuitionistic and affine logics

2018 ◽  
Vol 29 (8) ◽  
pp. 1177-1216
Author(s):  
CHUCK LIANG
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Kripke Semantics ◽  
Cut Elimination ◽  
Structural Rules ◽  
Phase Semantics ◽  
Intuitionistic Logics

This article presents a unified logic that combines classical logic, intuitionistic logic and affine linear logic (restricting contraction but not weakening). We show that this unification can be achieved semantically, syntactically and in the computational interpretation of proofs. It extends our previous work in combining classical and intuitionistic logics. Compared to linear logic, classical fragments of proofs are better isolated from non-classical fragments. We define a phase semantics for this logic that naturally extends the Kripke semantics of intuitionistic logic. We present a sequent calculus with novel structural rules, which entail a more elaborate procedure for cut elimination. Computationally, this system allows affine-linear interpretations of proofs to be combined with classical interpretations, such as the λμ calculus. We show how cut elimination must respect the boundaries between classical and non-classical modes of proof that correspond to delimited control effects.

scholarly journals The geometry of non-distributive logics

2005 ◽  
Vol 70 (4) ◽  
pp. 1108-1126 ◽  
Author(s):  
Greg Restall ◽  
Francesco Paoli
Keyword(s):  
Classical Logic ◽  
Natural Deduction ◽  
Sequent Calculus ◽  
Linear Logic ◽  
Cut Elimination ◽  
Deduction System ◽  
Inductive Definition ◽  
Theoretical Criterion ◽  
Natural Deduction System

AbstractIn this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems for classical logic and Girard's proofnets for linear logic.

scholarly journals On Correspondence between Selective CPS Transformation and Selective Double Negation Translation

Mathematics ◽  
2021 ◽  
Vol 9 (4) ◽  
pp. 385
Author(s):  
Hyeonseung Im
Keyword(s):  
Programming Languages ◽  
Intuitionistic Logic ◽  
Reference Point ◽  
Classical Logic ◽  
Proof System ◽  
Double Negation

A double negation translation (DNT) embeds classical logic into intuitionistic logic. Such translations correspond to continuation passing style (CPS) transformations in programming languages via the Curry-Howard isomorphism. A selective CPS transformation uses a type and effect system to selectively translate only nontrivial expressions possibly with computational effects into CPS functions. In this paper, we review the conventional call-by-value (CBV) CPS transformation and its corresponding DNT, and provide a logical account of a CBV selective CPS transformation by defining a selective DNT via the Curry-Howard isomorphism. By using an annotated proof system derived from the corresponding type and effect system, our selective DNT translates classical proofs into equivalent intuitionistic proofs, which are smaller than those obtained by the usual DNTs. We believe that our work can serve as a reference point for further study on the Curry-Howard isomorphism between CPS transformations and DNTs.

Sign in / Sign up

Export Citation Format

Share Document