Search results

1

Admissibility of Cut in Congruent Modal Logics

100%

Indrzejczak A.

Logic and Logical Philosophy

|

2011

|

vol. 20

|

issue 3

189-203

EN

We present a detailed proof of the admissibility of cut in sequent calculus for some congruent modal logics. The result was announced much earlier during the Trends in Logic Conference, Toruń 2006 and the proof for monotonic modal logics was provided already in Indrzejczak [5]. Also some tableau and natural deduction formalizations presented in Indrzejczak [6] and Indrzejczak [7] were based on this result but the proof itself was not published so far. In this paper we are going to fill this gap. The delay was partly due to the fact that the author from time to time was trying to improve the result and extend it to some additional logics by testing other methods of proving cut elimination. Unfortunately all these attempts failed and cut elimination holds only for these logics which were proved to satisfy this property already in 2005.

2

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

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

Hypersequent Calculi for S5: The Methods of Cut Elimination

100%

Bednarska K., Indrzejczak A.

Logic and Logical Philosophy

|

2015

|

vol. 24

|

issue 3

277–311

EN

S5 is one of the most important modal logic with nice syntactic, semantic and algebraic properties. In spite of that, a successful (i.e. cut-free) formalization of S5 on the ground of standard sequent calculus (SC) was problematic and led to the invention of numerous nonstandard, generalized forms of SC. One of the most interesting framework which was very often used for this aim is that of hypersequent calculi (HC). The paper is a survey of HC for S5 proposed by Pottinger, Avron, Restall, Poggiolesi, Lahav and Kurokawa. We are particularly interested in examining different methods which were used for proving the eliminability/admissibility of cut in these systems and present our own variant of a system which admits relatively simple proof of cut elimination.

Refine search results

4 Logic and Logical Philosophy

1 2019

1 2017

1 2015

1 2011

4 Indrzejczak A.

1 Bednarska K.

Admissibility of Cut in Congruent Modal Logics

Tautology Elimination, Cut Elimination, and S5

Fregean Description Theory in Proof-Theoretical Setting

Hypersequent Calculi for S5: The Methods of Cut Elimination