Proof Systems Combining Classical and Paraconsistent Negations

New propositional and first-order paraconsistent logics (called L _ω and FL _ω , respectively) are introduced as Gentzen-type sequent calculi with classical and paraconsistent negations. The embedding theorems of L _ω and FL _ω into propositional (first-order, respectively) classical logic are shown, and the completeness theorems with respect to simple semantics for L _ω and FL _ω are proved. The cut-elimination theorems for L _ω and FL _ω are shown using both syntactical ways via the embedding theorems and semantical ways via the completeness theorems. Presented by Yaroslav Shramko and Heinrich Wansing     

Towards a Semantic Characterization of Cut-Elimination

We introduce necessary and sufficient conditions for a (single-conclusion) sequent calculus to admit (reductive) cut-elimination. Our conditions are formulated both syntactically and semantically.     

A sequent calculus for a logic of contingencies

We introduce a sequent calculus that is sound and complete with respect to propositional contingencies, i.e., formulas which are neither provable nor refutable. Like many other sequent and natural deduction proof systems, this calculus possesses cut elimination and the subformula property and has a simple proof search mechanism.     

Sequent Calculi for Some Strict Implication Logics

We introduce various sequent systems for propositional logicshaving strict implication, and prove the completeness theoremsand the finite model properties of these systems.The cut-eliminationtheorems or the (modified) subformula properties are provedsemantically.     

Gentzen-Type Methods for Bilattice Negation

A general Gentzen-style framework for handling both bilattice (or strong) negation and usual negation is introduced based on the characterization of negation by a modal-like operator. This framework is regarded as an extension, generalization or re- finement of not only bilattice logics and logics with strong negation, but also traditional logics including classical logic LK, classical modal logic S4 and classical linear logic CL. Cut-elimination theorems are proved for a variety of proposed sequent calculi including CLS (a conservative extension of CL) and CLS_cw (a conservative extension of some bilattice logics, LK and S4). Completeness theorems are given for these calculi with respect to phase semantics, for SLK (a conservative extension and fragment of LK and CLS_cw, respectively) with respect to a classical-like semantics, and for SS4 (a conservative extension and fragment of S4 and CLScw, respectively) with respect to a Kripke-type semantics. The proposed framework allows for an embedding of the proposed calculi into LK, S4 and CL.     

Marginalia on Sequent Calculi

The paper discusses the relationship between normal natural deductions and cutfree proofs in Gentzen (sequent) calculi in the absence of term labeling. For Gentzen calculi this is the usual version; for natural deduction this is the version under the complete discharge convention, where open assumptions are always discharged as soon as possible. The paper supplements work by Mints, Pinto, Dyckhoff, and Schwichtenberg on the labeled calculi.     

Gentzen Calculi for the Existence Predicate

We introduce Gentzen calculi for intuitionistic logic extended with an existence predicate. Such a logic was first introduced by Dana Scott, who provided a proof system for it in Hilbert style. We prove that the Gentzen calculus has cut elimination in so far that all cuts can be restricted to very simple ones. Applications of this logic to Skolemization, truth value logics and linear frames are also discussed.     

Sequent Calculi and Decision Procedures for Weak Modal Systems

We investigate sequent calculi for the weak modal (propositional) system reduced to the equivalence rule and extensions of it up to the full Kripke system containing monotonicity, conjunction and necessitation rules. The calculi have cut elimination and we concentrate on the inversion of rules to give in each case an effective procedure which for every sequent either furnishes a proof or a finite countermodel of it. Applications to the cardinality of countermodels, the inversion of rules and the derivability of Löb rules are given.