LE^{t}_{ \to } , LR^{ \circ }_{{\widehat{ \sim }}}, LK and Cutfree Proofs

Two consecution calculi are introduced: one for the implicational fragment of the logic of entailment with truth and another one for the disjunction free logic of nondistributive relevant implication. The proof technique—attributable to Gentzen—that uses a double induction on the degree and on the rank of the cut formula is shown to be insufficient to prove admissible various forms of cut and mix in these calculi. The elimination theorem is proven, however, by augmenting the earlier double inductive proof with additional inductions. We also give a new purely inductive proof of the cut theorem for the original single cut rule in Gentzen’s sequent calculus $ LK $ without any use of mix.     

Quasivarieties of Modules Over Path Algebras of Quivers

Let FΛ be a finite dimensional path algebra of a quiver Λ over a field F. Let L and R denote the varieties of all left and right FΛ-modules respectively. We prove the equivalence of the following statements.

• The subvariety lattice of L is a sublattice of the subquasivariety lattice of L.
• The subquasivariety lattice of R is distributive.
• Λ is an ordered forest.

     

Algebraic study of Sette's maximal paraconsistent logic

The aim of this paper is to study the paraconsistent deductive systemP ¹ within the context of Algebraic Logic. It is well known due to Lewin, Mikenberg and Schwarse thatP ¹ is algebraizable in the sense of Blok and Pigozzi, the quasivariety generated by Sette's three-element algebraS being the unique quasivariety semantics forP ¹. In the present paper we prove that the mentioned quasivariety is not a variety by showing that the variety generated byS is not equivalent to any algebraizable deductive system. We also show thatP ¹ has no algebraic semantics in the sense of Czelakowski. Among other results, we study the variety generated by the algebraS. This enables us to prove in a purely algebraic way that the only proper non-trivial axiomatic extension ofP ¹ is the classical deductive systemPC. Throughout the paper we also study those abstract logics which are in a way similar toP ¹, and are called hereabstract Sette logics. We obtain for them results similar to those obtained for distributive abstract logics by Font, Verdú and the author.     

Gentzen-Style Sequent Calculus for Semi-intuitionistic Logic

The variety \({\mathcal{SH}}\) of semi-Heyting algebras was introduced by H. P. Sankappanavar (in: Proceedings of the 9th “Dr. Antonio A. R. Monteiro” Congress, Universidad Nacional del Sur, Bahía Blanca, 2008) [13] as an abstraction of the variety of Heyting algebras. Semi-Heyting algebras are the algebraic models for a logic HsH, known as semi-intuitionistic logic, which is equivalent to the one defined by a Hilbert style calculus in Cornejo (Studia Logica 98(1–2):9–25, 2011) [6]. In this article we introduce a Gentzen style sequent calculus GsH for the semi-intuitionistic logic whose associated logic GsH is the same as HsH. The advantage of this presentation of the logic is that we can prove a cut-elimination theorem for GsH that allows us to prove the decidability of the logic. As a direct consequence, we also obtain the decidability of the equational theory of semi-Heyting algebras.     

BK-lattices. Algebraic Semantics for Belnapian Modal Logics

Earlier algebraic semantics for Belnapian modal logics were defined in terms of twist-structures over modal algebras. In this paper we introduce the class of BK-lattices, show that this class coincides with the abstract closure of the class of twist-structures, and it forms a variety. We prove that the lattice of subvarieties of the variety of BK-lattices is dually isomorphic to the lattice of extensions of Belnapian modal logic BK. Finally, we describe invariants determining a twist-structure over a modal algebra.     

A Gentzen Calculus for Nothing but the Truth

In their paper Nothing but the Truth Andreas Pietz and Umberto Rivieccio present Exactly True Logic (ETL), an interesting variation upon the four-valued logic for first-degree entailment FDE that was given by Belnap and Dunn in the 1970s. Pietz & Rivieccio provide this logic with a Hilbert-style axiomatisation and write that finding a nice sequent calculus for the logic will presumably not be easy. But a sequent calculus can be given and in this paper we will show that a calculus for the Belnap-Dunn logic we have defined earlier can in fact be reused for the purpose of characterising ETL, provided a small alteration is made—initial assignments of signs to the sentences of a sequent to be proved must be different from those used for characterising FDE. While Pietz & Rivieccio define ETL on the language of classical propositional logic we also study its consequence relation on an extension of this language that is functionally complete for the underlying four truth values. On this extension the calculus gets a multiple-tree character—two proof trees may be needed to establish one proof.     

On Endomorphisms of Ockham Algebras with Pseudocomplementation

A pO-algebra ${(L; f, \, ^{\star})}$ is an algebra in which (L; f) is an Ockham algebra, ${(L; \, ^{\star})}$ is a p-algebra, and the unary operations f and ${^{\star}}$ commute. Here we consider the endomorphism monoid of such an algebra. If ${(L; f, \, ^{\star})}$ is a subdirectly irreducible pK _1,1- algebra then every endomorphism ${\vartheta}$ is a monomorphism or ${\vartheta^3 = \vartheta}$ . When L is finite the endomorphism monoid of L is regular, and we determine precisely when it is a Clifford monoid.     

Fatal Heyting Algebras and Forcing Persistent Sentences

Hamkins and L?we proved that the modal logic of forcing is S4.2. In this paper, we consider its modal companion, the intermediate logic KC and relate it to the fatal Heyting algebra H _ZFC of forcing persistent sentences. This Heyting algebra is equationally generic for the class of fatal Heyting algebras. Motivated by these results, we further analyse the class of fatal Heyting algebras.     

Sequent Calculi for Semi-De Morgan and De Morgan Algebras

A contraction-free and cut-free sequent calculus \(\mathsf {G3SDM}\) for semi-De Morgan algebras, and a structural-rule-free and single-succedent sequent calculus \(\mathsf {G3DM}\) for De Morgan algebras are developed. The cut rule is admissible in both sequent calculi. Both calculi enjoy the decidability and Craig interpolation. The sequent calculi are applied to prove some embedding theorems: \(\mathsf {G3DM}\) is embedded into \(\mathsf {G3SDM}\) via Gödel–Gentzen translation. \(\mathsf {G3DM}\) is embedded into a sequent calculus for classical propositional logic. \(\mathsf {G3SDM}\) is embedded into the sequent calculus \(\mathsf {G3ip}\) for intuitionistic propositional logic.     

On All Strong Kleene Generalizations of Classical Logic

By using the notions of exact truth (‘true and not false’) and exact falsity (‘false and not true’), one can give 16 distinct definitions of classical consequence. This paper studies the class of relations that results from these definitions in settings that are paracomplete, paraconsistent or both and that are governed by the (extended) Strong Kleene schema. Besides familiar logics such as Strong Kleene logic (K3), the Logic of Paradox (LP) and First Degree Entailment (FDE), the resulting class of all Strong Kleene generalizations of classical logic also contains a host of unfamiliar logics. We first study the members of our class semantically, after which we present a uniform sequent calculus (the SK calculus) that is sound and complete with respect to all of them. Two further sequent calculi (the \({{\bf SK}^\mathcal{P}}\) and \({\bf SK}^{\mathcal{N}}\) calculus) will be considered, which serve the same purpose and which are obtained by applying general methods (due to Baaz et al.) to construct sequent calculi for many-valued logics. Rules and proofs in the SK calculus are much simpler and shorter than those of the \({\bf SK}^{\mathcal{P}}\) and the \({\bf SK}^{\mathcal{N}}\) calculus, which is one of the reasons to prefer the SK calculus over the latter two. Besides favourably comparing the SK calculus to both the \({\bf SK}^{\mathcal{P}}\) and the \({\bf SK}^{\mathcal{N}}\) calculus, we also hint at its philosophical significance.     

An Inconsistency-Adaptive Deontic Logic for Normative Conflicts

We present the inconsistency-adaptive deontic logic DP ^r , a nonmonotonic logic for dealing with conflicts between normative statements. On the one hand, this logic does not lead to explosion in view of normative conflicts such as O A?∧?O ～A, O A?∧?P ～A or even O A?∧?～O A. On the other hand, DP ^r still verifies all intuitively reliable inferences valid in Standard Deontic Logic (SDL). DP ^r interprets a given premise set ‘as normally as possible’ with respect to SDL. Whereas some SDL-rules are verified unconditionally by DP ^r , others are verified conditionally. The latter are applicable unless they rely on formulas that turn out to behave inconsistently in view of the premises. This dynamic process is mirrored by the proof theory of DP ^r .     

Algebraic Functions

Let A be an algebra. We say that the functions f ₁, . . . , f _m : A ⁿ ?? A are algebraic on A provided there is a finite system of term-equalities ${{\bigwedge t_{k}(\overline{x}, \overline{z}) = s_{k}(\overline{x}, \overline{z})}}$ satisfying that for each ${{\overline{a} \in A^{n}}}$ , the m-tuple ${{(f_{1}(\overline{a}), \ldots , f_{m}(\overline{a}))}}$ is the unique solution in A ^m to the system ${{\bigwedge t_{k}(\overline{a}, \overline{z}) = s_{k}(\overline{a}, \overline{z})}}$ . In this work we present a collection of general tools for the study of algebraic functions, and apply them to obtain characterizations for algebraic functions on distributive lattices, Stone algebras, finite abelian groups and vector spaces, among other well known algebraic structures.     

Analytic Tableaux for all of <Emphasis Type="Italic">SIXTEEN</Emphasis><Subscript>3</Subscript>

In this paper we give an analytic tableau calculus P L _{1 6} for a functionally complete extension of Shramko and Wansing’s logic. The calculus is based on signed formulas and a single set of tableau rules is involved in axiomatising each of the four entailment relations ? _t , ? _f , ? _i , and ? under consideration—the differences only residing in initial assignments of signs to formulas. Proving that two sets of formulas are in one of the first three entailment relations will in general require developing four tableaux, while proving that they are in the ? relation may require six.     

The Church–Fitch knowability paradox in the light of structural proof theory

Anti-realist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$ , by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$ (KP). The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$ (OP). A Gentzen-style reconstruction of the Church–Fitch paradox is presented following a labelled approach to sequent calculi. First, a cut-free system for classical (resp. intuitionistic) bimodal logic is introduced as the logical basis for the Church–Fitch paradox and the relationships between ${\mathcal {K}}$ and ${\diamondsuit}$ are taken into account. Afterwards, by exploiting the structural properties of the system, in particular cut elimination, the semantic frame conditions that correspond to KP are determined and added in the form of a block of nonlogical inference rules. Within this new system for classical and intuitionistic “knowability logic”, it is possible to give a satisfactory cut-free reconstruction of the Church–Fitch derivation and to confirm that OP is only classically derivable, but neither intuitionistically derivable nor intuitionistically admissible. Finally, it is shown that in classical knowability logic, the Church–Fitch derivation is nothing else but a fallacy and does not represent a real threat for anti-realism.     

Kripke Sheaf Completeness of some Superintuitionistic Predicate Logics with a Weakened Constant Domains Principle

The completeness w.r.t. Kripke frames with equality (or, equivalently, w.r.t. Kripke sheaves, [8] or [4, Sect. 3.6]) is established for three superintuitionistic predicate logics: (Q-H + D*), (Q-H + D*&K), (Q-H + D*&K&J). Here Q-H is intuitionistic predicate logic, J is the principle of the weak excluded middle, K is Kuroda’s axiom, and D* (cf. [12]) is a weakened version of the well-known constant domains principle D. Namely, the formula D states that any individual has ancestors in earlier worlds, and D* states that any individual has ${\neg\neg}$ -ancestors (i.e., ancestors up to ${\neg\neg}$ -equality) in earlier worlds. In particular, the logic (Q-H + D*&K&J) is the Kripke sheaf completion of (Q-H + E&K&J), where E is a version of Markov’s principle (cf. [12]). On the other hand, we show that the logic (Q-H + D*&J) is incomplete w.r.t. Kripke sheaves.