Search

A finitely alternative normal tense logic $$T_{n,m}$$ is a normal tense logic characterized by frames in which every point has at most n future alternatives and m past alternatives. The structure of the lattice $$\Lambda (T_{1,1})$$ is described. There are $$\aleph _0$$ logics in $$\Lambda (T_{1,1})$$ without the finite model property (FMP), and only one pretabular logic in $$\Lambda (T_{1,1})$$ . There are $$2^{\aleph _0}$$ logics in $$\Lambda (T_{1,1})$$ which are not finitely axiomatizable. For $$nm\ge 2$$ , there are $$2^{\aleph _0}$$ logics in $$\Lambda (T_{n,m})$$ without the FMP, and infinitely many pretabular extensions of $$T_{n,m}$$ .

The language of Belnap–Dunn modal logic $${\mathscr {L}}_0$$ expands the language of Belnap–Dunn four-valued logic (having constant symbols for the values 0 and 1) with the modal operator $$\Box $$ . We introduce the polarity semantics for $${\mathscr {L}}_0$$ and its two expansions $${\mathscr {L}}_1$$ and $${\mathscr {L}}_2$$ with value operators. The local finitary consequence relation $$\models _4^k$$ in the language $${\mathscr {L}}_k$$ with respect to the class of all frames is axiomatized by a sequent system $$\mathsf {S}_k$$ where $$k=0, 1, 2$$ . We prove by using translations between sequents and formulas that these languages under the polarity semantics have the same expressive power on the level of frames with the language $${\mathscr {L}}_0$$ under the relational semantics for classical modal logic.

The minimal weakening $${{\textsf {N}}}_0$$ of Belnap-Dunn logic under the polarity semantics for negation as a modal operator is formulated as a sequent system which is characterized by the class of all birelational frames. Some extensions of $${{\textsf {N}}}_0$$ with additional sequents as axioms are introduced. In particular, all three modal negation logics characterized by a frame with a single state are formalized as extensions of $${{\textsf {N}}}_0$$ . These logics have the finite model property and they are decidable.

Every Berman’s variety $$\mathbb {K}_p^q$$ which is the subvariety of Ockham algebras defined by the equation $${\sim ^{2p+q}}a = {\sim ^q}a$$ ($$p\ge 1$$ and $$q\ge 0$$) determines a finitary substitution invariant consequence relation $$\vdash _p^q$$. A sequent system $$\mathsf {S}_p^q$$ is introduced as an axiomatization of the consequence relation $$\vdash _p^q$$. The system $$\mathsf {S}_p^q$$ is characterized by a single finite frame $$\mathfrak {F}_p^q$$ under the frame semantics given for the formal language. By the duality between frames and algebras, $$\mathsf {S}_p^q$$ can be viewed as a $$4^{2p+q}$$-valued logic as it is characterized by a distributive lattice of $$4^{2p+q}$$ elements with a unary operator. Moreover, a structural-rule-free, cut-free and terminating sequent system $$\mathsf {G}_p^q$$ is established for $$\vdash _p^q$$. The Craig interpolation property of $$\vdash _p^q$$ is shown proof-theoretically utilizing $$\mathsf {G}_p^q$$.

The global consequence relation of a normal modal logic $$\Lambda $$ is formulated as a global sequent calculus which extends the local sequent theory of $$\Lambda $$ with global sequent rules. All global sequent calculi of normal modal logics admits global cut elimination. This property is utilized to show that decidability is preserved from the local to global sequent theories of any normal modal logic over $$\mathsf {K4}$$ . The preservation of Craig interpolation property from local to global sequent theories of any normal modal logic is shown by proof-theoretic method.

A deterministic weakening $$\mathsf {DW}$$ of the Belnap–Dunn four-valued logic $$\mathsf {BD}$$ is introduced to formalize the acceptance and rejection of a proposition at a state in a linearly ordered informational frame with persistent valuations. The logic $$\mathsf {DW}$$ is formalized as a sequent calculus. The completeness and decidability of $$\mathsf {DW}$$ with respect to relational semantics are shown in terms of normal forms. From an algebraic perspective, the class of all algebras for $$\mathsf {DW}$$ is described, and found to be a subvariety of Berman’s variety $$\mathcal {K}_{1,2}$$ . Every linearly ordered frame is logically equivalent to its dual algebra. It is proved that $$\mathsf {DW}$$ is the logic of a nine-element distributive lattice with a negation. Moreover, $$\mathsf {BD}$$ is embedded into $$\mathsf {DW}$$ by Glivenko’s double-negation translation.

Charles Peirce's alpha system $$\mathfrak {S}_\alpha $$S? is reformulated into a deep inference system where the rules are given in terms of deep graphical structures and each rule has its symmetrical rule in the system. The proof analysis of $$\mathfrak {S}_\alpha $$S? is given in terms of two embedding theorems: the system $$\mathfrak {S}_\alpha $$S? and Brunnler's deep inference system for classical propositional logic can be embedded into each other; and the system $$\mathfrak {S}_\alpha $$S? and Gentzen sequent calculus $$\mathbf {G3c}^*$$G3c? can be embedded into each other.