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

scholarly journals Two Treatments of Definite Descriptions in Intuitionist Negative Free Logic

2019 ◽  
Vol 48 (4) ◽  
Author(s):  
Nils Kürbis
Keyword(s):  
Definite Descriptions ◽  
Present Approach ◽  
Predicate Abstraction ◽  
Free Logic ◽  
Axiomatic Treatment ◽  
Two Systems

Sentences containing definite descriptions, expressions of the form `The F', can be formalised using a binary quantier that forms a formula out of two predicates, where ℩x[F;G] is read as `The F is G'. This is an innovation over the usual formalisation of definite descriptions with a term forming operator. The present paper compares the two approaches. After a brief overview of the system INF℩ of intuitionist negative free logic extended by such a quantier, which was presented in [4], INF℩ is first compared to a system of Tennant's and an axiomatic treatment of a term forming ℩ operator within intuitionist negative free logic. Both systems are shown to be equivalent to the subsystem of INF℩ in which the G of ℩x[F;G] is restricted to identity. INF℩ is then compared to an intuitionist version of a system of Lambert's which in addition to the term forming operator has an operator for predicate abstraction for indicating scope distinctions. The two systems will be shown to be equivalent through a translation between their respective languages. Advantages of the present approach over the alternatives are indicated in the discussion.

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.

GENERALITY AND EXISTENCE 1: QUANTIFICATION AND FREE LOGIC

2018 ◽  
Vol 12 (1) ◽  
pp. 1-29
Author(s):  
GREG RESTALL
Keyword(s):  
Classical Logic ◽  
Sequent Calculus ◽  
Free Logic ◽  
Singular Terms ◽  
First Order ◽  
Existential Import ◽  
The Way

AbstractIn this paper, I motivate a cut free sequent calculus for classical logic with first order quantification, allowing for singular terms free of existential import. Along the way, I motivate a criterion for rules designed to answer Prior’s question about what distinguishes rules for logical concepts, like conjunction from apparently similar rules for putative concepts like Prior’s tonk, and I show that the rules for the quantifiers—and the existence predicate—satisfy that condition.

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 Free Logics are Cut-Free

Studia Logica ◽  
2021 ◽  
Author(s):  
Andrzej Indrzejczak
Keyword(s):  
Computer Science ◽  
Sequent Calculus ◽  
Cut Elimination ◽  
Constructive Mathematics ◽  
Free Logic ◽  
Sequent Calculi ◽  
Special Rule ◽  
First Time

AbstractThe paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is proved in a constructive way for sequent calculi adequate for all logics under consideration.

Sign in / Sign up

Export Citation Format

Share Document