Full-text resources of CEJSH and other databases are now available in the new Library of Science.
Visit https://bibliotekanauki.pl

Results found: 7

first rewind previous Page / 1 next fast forward last

Search results

Search:
in the keywords:  sequent calculus
help Sort By:

help Limit search:
first rewind previous Page / 1 next fast forward last
1
Content available remote

An Epistemic Interpretation of Paraconsistent Weak Kleene Logic

100%
Szmuc D. E.
Logic and Logical Philosophy
|
2019
|
vol. 28
|
issue 2
277-330
EN
This paper extends Fitting’s epistemic interpretation of some Kleene logics to also account for Paraconsistent Weak Kleene logic. To achieve this goal, a dualization of Fitting’s “cut-down” operator is discussed, leading to the definition of a “track-down” operator later used to represent the idea that no consistent opinion can arise from a set including an inconsistent opinion. It is shown that, if some reasonable assumptions are made, the truth-functions of Paraconsistent Weak Kleene coincide with certain operations defined in this track-down fashion. Finally, further reflections on conjunction and disjunction in the weak Kleene logics accompany this paper, particularly concerning their relation with containment logics. These considerations motivate a special approach to defining sound and complete Gentzen-style sequent calculi for some of their four-valued generalizations.
2
Content available remote

Tautology Elimination, Cut Elimination, and S5

100%
Indrzejczak A.
Logic and Logical Philosophy
|
2017
|
vol. 26
|
issue 4
461–471
EN
Tautology elimination rule was successfully applied in automated deduction and recently considered in the framework of sequent calculi where it is provably equivalent to cut rule. In this paper we focus on the advantages of proving admissibility of tautology elimination rule instead of cut for sequent calculi. It seems that one may find simpler proofs of admissibility for tautology elimination than for cut admissibility. Moreover, one may prove its admissibility for some calculi where constructive proofs of cut admissibility fail. As an illustration we present a cut-free sequent calculus for S5 based on tableau system of Fitting and prove admissibility of tautology elimination rule for it.
3
Content available remote

Fregean Description Theory in Proof-Theoretical Setting

100%
Indrzejczak A.
Logic and Logical Philosophy
|
2019
|
vol. 28
|
issue 1
137-155
EN
We present a proof-theoretical analysis of the theory of definite descriptions which emerges from Frege’s approach and was formally developed by Kalish and Montague. This theory of definite descriptions is based on the assumption that all descriptions are treated as genuine terms. In particular, a special object is chosen as a designatum for all descriptions which fail to designate a unique object. Kalish and Montague provided a semantical treatment of such theory as well as complete axiomatic and natural deduction formalization. In the paper we provide a sequent calculus formalization of this logic and prove cut elimination theorem in the constructive manner.
4

Symmetric and dual paraconsistent logics

88%
Kamide N., Wansing H.
Logic and Logical Philosophy
|
2010
|
vol. 19
|
issue 1-2
7–30
EN
Two new first-order paraconsistent logics with De Morgan-type negations and co-implication, called symmetric paraconsistent logic (SPL) and dual paraconsistent logic (DPL), are introduced as Gentzen-type sequent calculi. The logic SPL is symmetric in the sense that the rule of contraposition is admissible in cut-free SPL. By using this symmetry property, a simpler cut-free sequent calculus for SPL is obtained. The logic DPL is not symmetric, but it has the duality principle. Simple semantics for SPL and DPL are introduced, and the completeness theorems with respect to these semantics are proved. The cut-elimination theorems for SPL and DPL are proved in two ways: One is a syntactical way which is based on the embedding theorems of SPL and DPL into Gentzen’s LK, and the other is a semantical way which is based on the completeness theorems.
5
Content available remote

Partial and paraconsistent three-valued logics

63%
Degauquier V.
Logic and Logical Philosophy
|
2016
|
vol. 25
|
issue 2
143–171
EN
On the sidelines of classical logic, many partial and paraconsistent three-valued logics have been developed. Most of them differ in the notion of logical consequence or in the definition of logical connectives. This article aims, firstly, to provide both a model-theoretic and a proof-theoretic unified framework for these logics and, secondly, to apply these general frameworks to several well-known three-valued logics. The proof-theoretic approach to which we give preference is sequent calculus. In this perspective, several results concerning the properties of functional completeness, cut redundancy, and proof-search procedure are shown. We also provide a general proof for the soundness and the completeness of the three sequent calculi discussed.
6

On the proof-theory of a first-order extension of GL

51%
Schwartz Y., Tourlakis G.
Logic and Logical Philosophy
|
2014
|
vol. 23
|
issue 3
329–363
EN
We introduce a first order extension of GL, called ML3, and develop its proof theory via a proxy cut-free sequent calculus GLTS. We prove the highly nontrivial result that cut is a derived rule in GLTS, a result that is unavailable in other known first-order extensions of GL. This leads to proofs of weak reflection and the related conservation result for ML3, as well as proofs for Craig’s interpolation theorem for GLTS. Turning to semantics we prove that ML3 is sound with respect to arithmetical interpretations and that it is also sound and complete with respect to converse well-founded and transitive finite Kripke models. This leads us to expect that a Solovay-like proof of arithmetical completeness of ML3 is possible.
7
Content available remote

Znaczenie pojęcia odrzucania we współczesnej logice

45%
Rożko K.
Diametros
|
2014
|
issue 41
115-126
PL
Głównym celem artykułu jest pokazanie, jak pojęcie odrzucania zmieniało się na gruncie logiki w ciągu ostatnich kilkunastu lat. Idea odrzucania była znana już Arystotelesowi, ale do logi-ki formalnej zastała wprowadzona przez Jana Łukasiewicza. Następnie pojęcie to było wnikliwie analizowane przez polskich logików skoncentrowanych wokół Jerzego Słupeckiego. W ostatnim czasie ukazało się kilka interesujących artykułów, które rzucają nowe światło na tę problematykę. W tym artykule zarysowana zostanie historia pojęcia odrzucania oraz pokazane zostaną nowe zastosowania systemów odrzucania zarówno na gruncie teoretycznym, jak i praktycznym.
EN
The main aim of this article is to show how the notion of refutation has been changing in logic for the last few years. The idea of refutation was known to Aristotle, but the formal concept was introduced by Jan Łukasiewicz. Afterwards this notion was investigated by the Polish group of logicians headed by Jerzy Słupecki. Several interesting articles about refutation have appeared in the last years. In this article, I present in outline the history of the notion of refutation and I discuss recent applications of refutation systems both in the theoretical and practical approach.
first rewind previous Page / 1 next fast forward last
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.