Strong Normalisation of Cut-Elimination in Classical Logic

1999 ◽  
pp. 365-380 ◽  
Author(s):  
C. Urban ◽  
G. M. Bierman
Keyword(s):  
Classical Logic ◽  
Cut Elimination

scholarly journals Call-by-name reduction and cut-elimination in classical logic

2008 ◽  
Vol 153 (1-3) ◽  
pp. 38-65 ◽  
Author(s):  
Kentaro Kikuchi
Keyword(s):  
Classical Logic ◽  
Cut Elimination

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.

Embedding theorems for LTL and its variants

2014 ◽  
Vol 25 (1) ◽  
pp. 83-134 ◽  
Author(s):  
NORIHIRO KAMIDE
Keyword(s):  
Intuitionistic Logic ◽  
Classical Logic ◽  
Linear Time ◽  
Cut Elimination ◽  
Embedding Theorems ◽  
Infinitary Logic ◽  
Spatial Logic ◽  
Linear Time Temporal Logic ◽  
Np Complete ◽  
Dynamic Topological Logic

In this paper, we prove some embedding theorems for LTL (linear-time temporal logic) and its variants:viz. some generalisations, extensions and fragments of LTL. Using these embedding theorems, we give uniform proofs of the completeness, cut-elimination and/or decidability theorems for LTL and its variants. The proposed embedding theorems clarify the relationships between some LTL-variations (for example, LTL, a dynamic topological logic, a fixpoint logic, a spatial logic, Prior's logic, Davies' logic and an NP-complete LTL) and some traditional logics (for example, classical logic, intuitionistic logic and infinitary logic).

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 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.

On the non-confluence of cut-elimination

2011 ◽  
Vol 76 (1) ◽  
pp. 313-340 ◽  
Author(s):  
Matthias Baaz ◽  
Stefan Hetzl
Keyword(s):  
Classical Logic ◽  
Normal Forms ◽  
Strong Sense ◽  
Cut Elimination ◽  
First Order ◽  
Elementary Number

AbstractWe study cut-elimination in first-order classical logic. We construct a sequence of polynomial-length proofs having a non-elementary number of different cut-free normal forms. These normal forms are different in a strong sense: they not only represent different Herbrand-disjunctions but also differ in their prepositional structure.This result illustrates that the constructive content of a proof in classical logic is not uniquely determined but rather depends on the chosen method for extracting it.

Cut-elimination for simple type theory with an axiom of choice

1999 ◽  
Vol 64 (2) ◽  
pp. 479-485 ◽  
Author(s):  
G. Mints
Keyword(s):  
Classical Logic ◽  
Type Theory ◽  
Axiom Of Choice ◽  
Second Order ◽  
Cut Elimination ◽  
Simple Type ◽  
Simple Type Theory

AbstractWe present a cut-elimination proof for simple type theory with an axiom of choice formulated in the language with an epsilon-symbol. The proof is modeled after Takahashi's proof of cut-elimination for simple type theory with extensionality. The same proof works when types are restricted, for example for second-order classical logic with an axiom of choice.

Sign in / Sign up

Export Citation Format

Share Document