Analytic Tableaux for all of SIXTEEN ₃

Abstract

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.

1 Introduction

In [14] Yaroslav Shramko and Heinrich Wansing define an attractive generalisation of Belnap’s well-known four-valued logic (see [3, 4]). Where Belnap generalises classical two-valued propositional logic and moves from the set of truth values 2={1,0} to the set $\mathbf {4}=\mathcal {P}(\mathbf {2})$ of combinations of truth values, Shramko & Wansing repeat the move and consider logics based on $\mathbf {16}=\mathcal {P}(\mathbf {4})$—combinations of combinations of classical truth values. Belnap’s original motivation for the move from 2 to 4—a logic based on this set can model how a computer should deal with the incomplete and/or inconsistent information that may be fed to it—is extended as well, as the logic based on 1 6 arguably models how a network should reason on the basis of input it gets from computers reasoning on the basis of 4.

These moves from 2 to 4 and from 4 to 1 6 come with an increasing number of lattice orderings. There is of course the usual ordering on 2, but Belnap considers two orders on 4. The first of these is that of the logical lattice L4, in which the values $\mathbf {T}=\{1\}, ~\mathbf {F}=\{0\},~\mathbf {N}=\varnothing$, and B={1,0} are ordered in a way that corresponds to an extension of the Strong Kleene evaluation scheme (see Fig. 1 for a Hasse diagram). The second is the ordering of the approximation of information lattice A4, in which the same values are ordered according to their degree of information. Together these two orderings form what is called a bilattice. On 1 6 Shramko & Wansing consider three orderings, denoted with ≤ _t , ≤ _f , and ≤ _i , together forming the so-called trilattice SIXTEEN ₃. Of these three, ≤ _t can be interpreted as a truth order, ≤ _f as a falsity order, and ≤ _i again as an approximation of information order. The lattice L4, which in fact acts as a truth and falsity order, is thus replaced by two independent orderings, not each other’s inverses, as will become apparent below.

Fig. 1

Belnap’s lattices L4 and A4

Meet and join operations on these lattices can naturally be associated with conjunction and disjunction operators, but there are unary functions that can interpret negation too. Belnap [4] already considers a negation operation on 4 that swaps T and F, but leaves N and B untouched, but it has a natural dual in the operation that swaps N and B but leaves T and F as is. On S I X T E E N ₃ there are three involutions − _t , ‒ _f , and − _i that are natural candidates to provide the semantics for negation connectives in a logical language.

We thus see that S I X T E E N ₃ is well-understood (more precise definitions are to follow after this introduction). But the proof theory of logics based on this trilattice is another matter (see also Odintsov & Wansing’s [10] section 1.2 on ‘the axiomatization problem’). We are aware of several approaches. Odintsov [9], for example, gives Hilbert style axiomatisations of the truth entailment relation ⊧ _t naturally based on ≤ _t and the falsity entailment relation ⊧ _f based on ≤ _f . Another way of dealing with this problem is exemplified in Wansing [16], where cut-free sequent calculi for ⊧ _t and ⊧ _f are presented. And a third way can be found in Odintsov & Wansing’s [10], where a so-called ‘bi-calculus’ for the t and f consequence relations is given. More sequent and tableau systems for S I X T E E N ₃ related logics are presented in Kamide & Wansing [5] and in Wansing & Kamide [18].

But something is still to be wished for, as the logical languages that have been considered do not provide a set of connectives that is functionally complete for 1 6. In particular, we are not aware of an existing system in which a connective ∧ _i corresponding to meet in the ≤ _i order is definable. (Odintsov’s and Wansing’s logics are based on connectives corresponding to meet and join in the ≤ _t and ≤ _f orderings, plus, in the case of some logics, certain implications → _t and → _f that are residua with respect to these orderings. But ∧ _i cannot be defined in any of the resulting languages, as will become clear below). Since ∧ _i can be thought of as formalising a sceptical information merging strategy that one may reasonably want a computer network to follow, there is some interest in clarifying its proof theory and characterising its interactions with other connectives.

The purpose of this paper therefore is to give a calculus that characterises a propositional logic that expresses all of S I X T E E N ₃, i.e. deals with all truth functions on 1 6. We will provide such a logic with the help of a generalisation of the approach in Wintein & Muskens [19], where a calculus for a functionally complete first-order logic based on Belnap’s two lattices was given. That paper was based on two ideas that are relevant here. The first of these—taken over from Muskens [8] and ultimately from Langholm [6]—was to use a four-sided sequent calculus,¹ the second idea was to let each proof correspond to two proof trees in the usual sense (see also Wintein & Muskens [20]). We will generalise this approach by giving a signed analytic tableau calculus based on eight signs and by letting proofs correspond to four or even six tableaux (an eight-sided Gentzen sequent variant could easily be given). From a semantic point of view, each of the eight signs (for which we use t, f, n, b, t̸, f̸, n̸, and b̸) signals whether an element from 4={T, F, N, B} is present or absent in the value of the sentence that is signed and each tableau checks whether one of these four values is transmitted from premises to conclusions or vice versa. While the description just given may seem to point to a rather complicated system, the calculus is in fact simple and can be used to provide syntactic characterisations of the semantic entailment relations ⊧ _t , ⊧ _f , and ⊧ _i (information entailment²) based on the three lattice orderings, and a relation ⊧ which is the intersection of ⊧ _t and ⊧ _f . A single set of rules can be used for all four consequence relations (a feature our logic shares with the sequent calculus framework of Wansing [16]), but testing for different consequence relations involves different ways of initially assigning signs to formulas.

The presentation in this paper is meant to be technically self-contained, but is not self-contained in terms of providing general background and motivation. For these, the reader is invited to consult the papers cited above, or the somewhat more philosophical Wansing [17], or the full monograph Shramko & Wansing [15].

2 The Trilattice S I X T E E N ₃

The general theory of trilattices is subtle, but a description of S I X T E E N ₃ in particular is easy to give. As explained in the introduction, the domain of this trilattice is $\mathbf {16}=\mathcal {P}(\mathbf {4})$, where $\mathbf {4}=\mathcal {P}(\{1,0\})=\{\mathbf {T},\mathbf {F},\mathbf {N},\mathbf {B}\}$. In order to obtain the three lattice orderings, the following auxiliary definition from [14] is useful.

Definition 1

For any S∈1 6, let

$$\begin{array}{@{}rcl@{}} S^{t}& := \{x\in S\mid 1\in x\} \quad(= S\cap\{\mathbf{T},\mathbf{B}\})\\ S^{-t}& := \{x\in S\mid 1\notin x\} \quad(=S\cap\{\mathbf{F},\mathbf{N}\})\\ S^{f}& := \{x\in S\mid 0\in x\} \quad(= S\cap\{\mathbf{F},\mathbf{B}\})\\ S^{-f}& := \{x\in S\mid 0\notin x\} \quad(= S\cap\{\mathbf{T},\mathbf{N}\}) \end{array} $$

The idea here is that S ^t consists of all values in S that code for truth, S ^−t for all values in S that do not, S ^f for all values that code for falsity, and S ^−f for those that do not code for falsity. The trilattice orderings are now obtained as follows with the help of these operations.

Definition 2

Define ≤ _t , ≤ _f , and ≤ _i by letting, for any S ₁,S ₂∈1 6:

$$\begin{array}{@{}rcl@{}} S_{1}\leq_{t} S_{2} &\Longleftrightarrow& {S_{1}^{t}}\subseteq {S_{2}^{t}}\mathrm{ ~and ~} S_{2}^{-t}\subseteq S_{1}^{-t}\\ S_{1}\leq_{f} S_{2} &\Longleftrightarrow& {S_{2}^{f}}\subseteq {S_{1}^{f}}\mathrm{ ~and~ } S_{1}^{-f}\subseteq S_{2}^{-f}\\ S_{1}\leq_{i} S_{2} &\Longleftrightarrow& S_{1}\subseteq S_{2} \end{array} $$

Note that ≤ _t is defined in terms of truth only, ≤ _f in terms of falsity only. We have followed Odintsov [9] and Odintsov & Wansing [10] in letting ≤ _f be the inverse of the ≤ _f relation originally defined in [14]. An increase in the falsity order will make statements less false, not more so (and the falsity order could equally well be called a nonfalsity order).

For our purposes it will be worthwile to also characterise ≤ _t and ≤ _f in the following more concrete way. That these equivalences hold is verified by an easy inspection.

Proposition 1

For any S ₁, S₂ in SIXTEEN ₃ :

$$\begin{array}{@{}rcl@{}} S_{1}\leq_{t} S_{2} \Longleftrightarrow & \left\{\begin{array}{ll} \mathbf{T}\in S_{1} & \Rightarrow \mathbf{T} \in S_{2}\text{ ~and ~} \mathbf{B} \in S_{1}\Rightarrow \mathbf{B}\in S_{2}\text{ ~and~}\\ \mathbf{F}\in S_{2} & \Rightarrow \mathbf{F}\in S_{1}\text{~ and ~} \mathbf{N}\in S_{2}\Rightarrow \mathbf{N}\in S_{1} \end{array}\right.\\ S_{1}\leq_{f} S_{2} \Longleftrightarrow & \left\{ \begin{array}{ll}\mathbf{F} \in S_{2} & \Rightarrow \mathbf{F}\in S_{1}\text{ ~and~ } \mathbf{B} \in S_{2}\Rightarrow \mathbf{B}\in S_{1}\text{ ~and~}\\ \mathbf{T}\in S_{1} & \Rightarrow \mathbf{T}\in S_{2}\text{ ~and ~} \mathbf{N}\in S_{1}\Rightarrow \mathbf{N}\in S_{2} \end{array}\right. \end{array} $$

In fact the four implications characterising ≤ _t will lead to four auxiliary semantic entailment relations in Section 4, which will, in their turn, correspond to four syntactic consequence relations.

Each of the lattice orderings on 1 6 comes with meet and join operations, We will write ⊓ _x for the meet and ⊔ _x for the join of ≤ _x (x ∈ {t, f, i}). Clearly, ⊓ _i is $\cap$ and ⊔ _i is ∪. For the other four operations the following proposition provides a handy reference (see also [15], but note that the inverse of our ≤ _f is employed there).

Proposition 2

For any $S,~S^{\prime }$ in SIXTEEN ₃ :

$$\begin{array}{llllll} \mathbf{T}\in S \sqcap_{t} S^{\prime} &\Leftrightarrow \mathbf{T}\in S \text{ ~and ~} \mathbf{T}\in S^{\prime};\qquad \mathbf{T}\in S \sqcup_{t} S^{\prime}&\Leftrightarrow \mathbf{T}\in S \text{ ~or ~}\mathbf{T} \in S^{\prime};\\ \mathbf{B} \in S \sqcap_{t} S^{\prime} &\Leftrightarrow \mathbf{B}\in S \text{ ~and ~}\mathbf{B}\in S^{\prime};\qquad \mathbf{B} \in S \sqcup_{t} S^{\prime} &\Leftrightarrow \mathbf{B} \in S \text{ ~or ~} \mathbf{B} \in S^{\prime};\\ \mathbf{F} \in S \sqcap_{t} S^{\prime} &\Leftrightarrow \mathbf{F} \in S \text{ ~or ~}\mathbf{F}\in S^{\prime};\qquad \mathbf{F}\in S \sqcup_{t} S^{\prime} &\Leftrightarrow \mathbf{F} \in S\text{~ and ~} \mathbf{F}\in S^{\prime};\\ \mathbf{N} \in S \sqcap_{t} S^{\prime} &\Leftrightarrow \mathbf{N} \in S\text{ ~or ~}\mathbf{N}\in S^{\prime};\qquad \mathbf{N}\in S \sqcup_{t} S^{\prime} &\Leftrightarrow \mathbf{N} \in S\text{ ~and ~}\mathbf{N}\in S^{\prime};\\\\ \mathbf{T} \in S \sqcap_{f} S^{\prime} &\Leftrightarrow \mathbf{T} \in S\text{ ~and ~}\mathbf{T}\in S^{\prime};\qquad \mathbf{T}\in S \sqcup_{f} S^{\prime} &\Leftrightarrow \mathbf{T}\in S\text{ ~or ~}\mathbf{T}\in S^{\prime};\\ \mathbf{B}\in S \sqcap_{f} S^{\prime} &\Leftrightarrow \mathbf{B}\in S\text{ ~or ~}\mathbf{B}\in S^{\prime};\qquad \mathbf{B}\in S \sqcup_{f} S^{\prime} &\Leftrightarrow \mathbf{B}\in S\text{ ~and~ }\mathbf{B}\in S^{\prime};\\ \mathbf{F}\in S \sqcap_{f} S^{\prime} &\Leftrightarrow \mathbf{F} \in S\text{ ~or ~}\mathbf{F}\in S^{\prime};\qquad \mathbf{F}\in S \sqcup_{f} S^{\prime}&\Leftrightarrow \mathbf{F}\in S\text{ ~and ~}\mathbf{F}\in S^{\prime};\\ \mathbf{N} \in S \sqcap_{f} S^{\prime} &\Leftrightarrow \mathbf{N} \in S\text{ ~and ~} \mathbf{N} \in S^{\prime};\qquad \mathbf{N} \in S \sqcup_{f} S^{\prime} &\Leftrightarrow \mathbf{N} \in S\text{ ~or ~} \mathbf{N} \in S^{\prime}. \end{array} $$

S I X T E E N ₃ can now be defined as 〈1 6,⊓ _t ,⊔ _t ,⊓ _f ,⊔ _f ,⊓ _i ,⊔ _i 〉 and the reader may wish to verify that, for any ’,∘ ∈ {⊓ _t ,⊔ _t ,⊓ _f ,⊔ _f ,⊓ _i ,⊔ _i }, we have that a∘(b∙c)=(a∘b)∙(a c) (see also Rivieccio [11]). This makes S I X T E E N ₃ into a distributive trilattice, from which it can be shown to follow that the structure is interlaced, in the sense that all six lattice operations are monotone with respect to the three lattice orders.

It is useful to also have available three unary operations that can be taken to be the semantic correlates of negation connectives. The following definition provides them.

Definition 3

Define the unary operations − _t , − _f , and − _i by letting, for any S∈1 6:

$$\begin{array}{@{}rcl@{}} \begin{aligned} \mathbf{T}\in {-}_{t} S &\Leftrightarrow \mathbf{N} \in S;\qquad \mathbf{T}\in {-}_{f} S &\Leftrightarrow \mathbf{B} \in S;\qquad \mathbf{T} \in {-}_{i} S &\Leftrightarrow \mathbf{F}\notin S;\\ \mathbf{B}\in {-}_{t} S &\Leftrightarrow \mathbf{F} \in S;\qquad \mathbf{B} \in {-}_{f} S &\Leftrightarrow \mathbf{T} \in S;\qquad \mathbf{B} \in {-}_{i} S &\Leftrightarrow \mathbf{N} \notin S;\\ \mathbf{F} \in {-}_{t} S &\Leftrightarrow \mathbf{B} \in S;\qquad \mathbf{F} \in {-}_{f} S &\Leftrightarrow \mathbf{N} \in S;\qquad \mathbf{F} \in {-}_{i} S &\Leftrightarrow \mathbf{T} \notin S;\\ \mathbf{N} \in {-}_{t} S &\Leftrightarrow \mathbf{T} \in S;\qquad \mathbf{N} \in {-}_{f} S &\Leftrightarrow \mathbf{F} \in S;\qquad \mathbf{N} \in {-}_{i} S &\Leftrightarrow \mathbf{B} \notin S; \end{aligned} \end{array} $$

Inspection will show that, for each pairwise distinct x,y∈{t,f,i},

$$\begin{array}{@{}rcl@{}} &&\text{if ~}a\leq_{x} b,\text{ ~then ~}{-}_{x} b\leq_{x} {-}_{x} a~ ;\\ &&\text{if ~}a\leq_{y} b,\text{ ~then ~}{-}_{x} a\leq_{y} {-}_{x} b~ ;\\ &&a = {-}_{x}{-}_{x} a . \end{array} $$

(Again see Rivieccio [11].)

This ends the description of S I X T E E N ₃ proper, but before we end this section we would like to introduce three operators defined by Odintsov in [9], as they will play a role in the next section. The first two can be defined as follows.

Definition 4

Define the binary operations $\sqsupset _{t}$, and $\sqsupset _{f}$ by letting, for any $S,S^{\prime }\in \mathbf {16}$:

$$\begin{array}{@{}rcl@{}} \begin{array}{lllll} \mathbf{T}\in S \sqsupset_{t} S^{\prime}&\Leftrightarrow \mathbf{T} \notin S\text{ ~or ~}\mathbf{T} \in S^{\prime};\qquad \mathbf{T}\in S \sqsupset_{f} S^{\prime} &\Leftrightarrow \mathbf{T} \notin S\text{ ~or ~}\mathbf{T}\in S^{\prime};\\ \mathbf{B} \in S \sqsupset_{t} S^{\prime}&\Leftrightarrow \mathbf{B} \notin S\text{ ~or ~} \mathbf{B} \in S^{\prime}; \qquad \mathbf{B} \in S \sqsupset_{f} S^{\prime} &\Leftrightarrow \mathbf{B} \notin S\text{ ~and ~}\mathbf{B}\in S^{\prime};\\ \mathbf{F} \in S \sqsupset_{t} S^{\prime} &\Leftrightarrow \mathbf{F} \notin S\text{ ~and ~} \mathbf{F} \in S^{\prime};\qquad \mathbf{F}\in S \sqsupset_{f} S^{\prime} &\Leftrightarrow \mathbf{F} \notin S\text{ ~and ~}\mathbf{F}\in S^{\prime};\\ \mathbf{N}\in S \sqsupset_{t} S^{\prime} &\Leftrightarrow \mathbf{N} \notin S\text{~ and ~} \mathbf{N} \in S^{\prime};\qquad \mathbf{N} \in S \sqsupset_{f} S^{\prime} &\Leftrightarrow \mathbf{N} \notin S\text{ ~or ~}\mathbf{N} \in S^{\prime}. \end{array} \end{array} $$

Odintsov’s unary operator $\rightharpoondown$, which completes the three, is defined by letting $\rightharpoondown S=\{\mathbf {T},\mathbf {F},\mathbf {N},\mathbf {B}\}-S$, for any S∈1 6.

The reader may note that $\rightharpoondown$ in fact equals the composition of − _t , − _f , and − _i (in any order) and that $S \,{\sqsupset _{t}} S^{\prime }=\,\rightharpoondown {}S\,{\sqcup _{t}} S^{\prime }$, while $S\,{\sqsupset _{f}} S^{\prime }=\,\rightharpoondown {}S\,{\sqcup _{f}} S^{\prime }$, for any $S,S^{\prime }\in \mathbf {16}$.

3 Syntax, Semantics, and Expressivity

The logical language we shall use in this paper will be $\mathcal {L}_{\mathit {tfi}}$, given by the following BNF form (where p comes from some countably infinite set of propositional constants).

$$\varphi ::= p\mid{\sim_{t}}\varphi\mid{\sim_{f}}\varphi\mid{ \sim_{i}}\varphi\mid \varphi\land_{t}\,\varphi\mid\varphi\land_{f}\, \varphi\mid\varphi\land_{i}\, \varphi $$

This set-up may be somewhat spartan, but other connectives can be defined and the set {∼ _t ,∼ _f ∼ _i ,∧ _t ,∧ _f ,∧ _i } is in fact functionally complete, as we shall see shortly.

Let us provide the language $\mathcal {L}_{\mathit {tfi}}$ with a semantics. The following definition will not come as a surprise.

Definition 5

A valuation function is a function V from the sentences of $\mathcal {L}_{\mathit {tfi}}$ to 1 6 such that

$$\begin{array}{lllll} V(\varphi \land_{t} \psi) &= V(\varphi) \sqcap_{t} V(\psi);\qquad V(\sim_{t}{}\varphi) &= {-}_{t} V(\varphi);\\ V(\varphi \land_{f} \psi) &= V(\varphi) \sqcap_{f} V(\psi);\qquad V(\sim_{f}{}\varphi) &= -_{f} V(\varphi);\\ V(\varphi \land_{i} \psi) &= V(\varphi) \sqcap_{i} V(\psi);\qquad V(\sim_{i}{}\varphi) &= {-}_{i} V(\varphi). \end{array} $$

Given this interpretation of the language, we clearly can also define connectives denoting the operations $\sqcup _{t}, ~\sqcup _{f},~\sqcup _{i},~\rightharpoondown ,~\sqsupset _{t}$, and $\sqsupset _{f}$ via the obvious De Morgan rules and the equivalences discussed in the previous section.

Definition 6

The following abbreviations will be in force.

$$\begin{array}{@{}rcl@{}} \varphi \lor_{t} \psi & :=& \sim_{t}(\sim_{t}{}\varphi\,\land_{t} \sim_{t}{}\psi);\\ \varphi \lor_{f}\psi & := & \sim_{f} (\sim_{f}{}\varphi\,\land_{f} \sim_{f}{}\psi);\\ \varphi \lor_{i} \psi & :=& \sim_{i}(\sim_{i}{}\varphi\,\land_{i}\sim_{i}{}\psi);\\ \lnot\varphi & :=& \sim_{t} \sim_{f} \sim_{i}{}\varphi;\\ \varphi \to_{t} \psi & :=& \lnot\varphi \lor_{t}\psi;\\ \varphi \to_{f}\psi & :=& \lnot\varphi \lor_{f}\psi. \end{array} $$

It is easily verified that $V(\lnot \varphi ) =\, \rightharpoondown {}V(\varphi )$ etc.

It will also be possible to define sentences that constantly denote a given element of 1 6, regardless of the valuation. This can be done for each element of 1 6. In the following definition we have chosen names for these sentences that serve as a mnemonic for the element denoted (e.g. V(n f b)={N,F,B}, for any V).

Definition 7

Let p ₀ be some fixed propositional constant. The following abbreviations will be used.

ᅟ ᅟ

Let us call a sentence φ bivalent if V(φ) = {T, B} or V(φ) = {N, F} for any valuation V (note that {T, B} is the top element of the ≤ _t order, while {N, F} is its bottom element). It is useful to have connectives at our disposal that always give a result that is bivalent. For arbitrary φ, consider the sentence T φ defined as

$$\varphi\,\,\land_{t} \sim_{i}{}\varphi\,\,\land_{t} \sim_{f}{}\varphi\,\,\land_{t} \sim_{f} \sim_{i}{}\varphi . $$

We find by inspection, using Proposition 2 and Definition 3, that, for any V,

$$\begin{array}{@{}rcl@{}} \mathbf{T}\in V(\mathsf{T}\varphi)&\Longleftrightarrow& \mathbf{T}\in V(\varphi)\text{~ and ~}\mathbf{F}\notin V(\varphi)\text{ ~and ~} \mathbf{B}\in V(\varphi)\text{ ~and ~}\mathbf{N}\notin V(\varphi)\\ & \Longleftrightarrow & \mathbf{B} \in V(\mathsf{T}\varphi)\\ \mathbf{F}\in V(\mathsf{T} \varphi)& \Longleftrightarrow & \mathbf{F} \in V(\varphi)\text{ ~or ~} \mathbf{T} \notin V(\varphi)\text{ ~or ~} \mathbf{N} \in V(\varphi)\text{ ~or ~}\mathbf{B} \notin V(\varphi)\\ & \Longleftrightarrow & \mathbf{N} \in V(\mathsf{T}\varphi) \end{array} $$

From this it follows that V(T φ)={T,B} iff V(φ)={T,B} and that V(T φ)={N,F} iff V(φ)≠{T,B}. This can be used to define other connectives giving bivalent results.

Definition 8

We define the following connectives.

$$\begin{array}{@{}rcl@{}} \varphi \twoheadrightarrow_{t} \psi &:=& \mathsf{T}(\varphi \to_{t} \psi)\\ \varphi\equiv\psi &:= &(\varphi \twoheadrightarrow_{t} \psi)\land_{t} (\psi \twoheadrightarrow_{t}\varphi) \end{array} $$

In [9] Odintsov shows that, for every $S, ~S^{\prime }\in \mathbf {16}, ~S\leq _{t} S^{\prime }$ iff $S \sqsupset _{t} S^{\prime }=\{ \mathbf {T},\mathbf {B}\}$. From this and the definition of $\varphi \twoheadrightarrow _{t} \psi$ it follows that, for all $V, ~V(\varphi \twoheadrightarrow _{t} \psi )=\{\mathbf {T},\mathbf {B1}\}$ iff V(φ) ≤ _t V(ψ) and $V(\varphi \twoheadrightarrow _{t} \psi )=\{\mathbf {N},\mathbf {F}\}$ iff V(φ)≦̸ _t V(ψ). The ≡ connective expresses identity, as V(φ≡ψ)={T,B} iff V(φ)=V(ψ), and V(φ≡ψ)={N,F} otherwise.

We now turn to the functional completeness theorem, for which we will assume that p ₀,p ₁,p ₂,…,p _n ,… is some fixed enumeration of the set of propositional constants (p ₀ was already used in Definition 7). If g is an n-ary truth function g:1 6 ⁿ→1 6 and φ is an $\mathcal {L}_{\mathit {tfi}}$ formula such that exactly p ₀,p ₁,…,p _n occur in φ, we say that φ expresses g if V(φ)=g(V(p ₁),…,V(p _n )), for each valuation V.

Proposition 3

Every truth function g: 1 6 ⁿ→1 6 is expressed by an $\mathcal {L}_{\mathit {tfi}}$ formula.

Proof

The proof generalises that of Muskens [7] for the four-valued case and proceeds by induction on n. Zero-place truth functions can be identified with the elements of 1 6 and inspection of Definition 7 shows that each element of that set is denoted by a constant defined there. For S∈1 6 we will use the notation $\overline {S}$ to refer to the term given in Definition 7 that denotes S. For the induction step, let g:1 6 ⁿ⁺¹→1 6 be an n+1-ary function. For each S∈1 6 define the n-ary truth function $g_{S}:\mathbf {16}^{n}\to \mathbf {16}$ by letting g _S (S ₁,…,S _n )=g(S ₁,…,S _n ,S). Using induction we find that each g _S (S∈1 6) is expressed by some formula φ _S . Let φ be the formula

$$\underset{U\in\mathbf{16}}{{\bigwedge}_{t}} \sim_{t}{}(p_{n+1}\equiv\overline{U})\lor_{t}\varphi_{U}~ , $$

where $\bigwedge _{t}$ is used to denote a finite ∧ _t -conjunction of formulas. Let V be an arbitrary valuation. Then V(p _n+1)=S, for some S∈1 6 and, for any $S^{\prime }\neq S$, it holds that $V(\sim _{t}{}(p_{n+1}\equiv \overline {S^{\prime }})\lor _{t}\varphi _{S^{\prime }})=\{ \mathbf {T},{\mathbf {B}}\}$, while $V(\sim _{t}{}(p_{n+1}\equiv \overline {S})\lor _{t}\varphi _{S})=V(\varphi _{S})$. It follows that V(φ)=V(φ _S )=g _S (V(p ₁),…,V(p _n ))=g(V(p ₁),…,V(p _n ),S), so that V(φ)=g(V(p ₁),…,V(p _n ),V(p _n+1)), and, since V was arbitrary, that φ expresses g. □

It is also instructive to see that {∼ _t ,∼ _f ,∼ _i ,∧ _t ,∧ _f ,∧ _i } is a minimal set that is functionally complete.

Proposition 4

No proper subset of {∼ _t ,∼ _f ,∼ _i ,∧ _t ,∧ _f ,∧ _i } can express every truth function g: 1 6 ⁿ→1 6.

Proof

In order to see that ∼ _t is essential, consider a unary g such that g({T,B})={N,F}. Each operator underlying one of the connectives ∼ _f , ∼ _i , ∧ _t , ∧ _f , and ∧ _i will return the value {T,B} when its argument(s) all take that value, so no formula in {∼ _f ,∼ _i ,∧ _t ,∧ _f ,∧ _i } can express g.

That ∧ _i cannot be left out can be seen by considering the set

$$\mathcal{O} := \{\{\mathbf{T},\mathbf{B}\}, \{\mathbf{N},\mathbf{F}\}, \{\mathbf{N},\mathbf{T}\}, \{\mathbf{F},\mathbf{B}\}\}~. $$

Each connective in {∼ _t ,∼ _f ,∼ _i ,∧ _t ,∧ _f } will return a value from $\mathcal {O}$ when fed arguments from $\mathcal {O}$. It follows that no formula built up from these connectives can take the value $\varnothing$ when all its propositional constants are assigned elements of $\mathcal {O}$. So no formula in {∼ _t ,∼ _f ,∼ _i ,∧ _t ,∧ _f } can express ⊓ _i .

For the other four cases proceed similarly. □

The last proposition of this section shows that some logics considered in the literature (see Odintsov [9] and Wansing’s [16]) are equally expressive.

Proposition 5

The languages

$$\begin{array}{@{}rcl@{}} \mathcal{L}_{\mathit{tf}}^{\to_{t}}:\quad &\varphi & ::= p\,\,\mid\,\,\sim_{t}{}\varphi\mid\,\, \sim_{f}{}\varphi\mid \varphi \land_{t} \varphi\mid\varphi \land_{f} \varphi\mid\varphi \to_{t} \varphi\\ \mathcal{L}_{\mathit{tf}}^{\to_{f}}:\quad & \varphi & ::= p\,\,\mid\,\,\sim_{t}{}\varphi\mid\,\,\sim_{f}{}\varphi\mid \varphi \land_{t} \varphi\mid\varphi \land_{f} \varphi\mid\varphi \to_{f} \varphi\\ \mathcal{L}_{\mathit{tf}}^{\ast}:\quad & \varphi & ::= p\,\,\mid\,\,\sim_{t}{}\varphi\mid\,\,\sim_{f}{}\varphi\mid \varphi \land_{t} \varphi\mid\varphi \land_{f} \varphi\mid\varphi \to_{t} \varphi \mid\varphi \to_{f} \varphi\\ \mathcal{L}_{\mathit{tf}}^{\sim_{i}}:\quad & \varphi & ::= p\,\,\mid\,\,\sim_{t}{}\varphi\mid\,\,\sim_{f}{}\varphi\mid\,\,\sim_{i}{}\varphi\mid \varphi \land_{t} \varphi\mid\varphi \land_{f} \varphi \end{array} $$

are all equally expressive.

Proof

Observe that Definition 6 did not make use of ∧ _i to obtain → _t and → _f , so $\mathcal {L}_{\mathit {tf}}^{\sim _{i}}$ is at least as expressive as any of $\mathcal {L}_{\mathit {tf}}^{\to _{t}}, ~\mathcal {L}_{\mathit {tf}}^{\to _{f}}$, or $\mathcal {L}_{\mathit {tf}}^{\ast }$. To see that, conversely, any of $\mathcal {L}_{\mathit {tf}}^{\to _{t}}, ~\mathcal {L}_{\mathit {tf}}^{\to _{f}}$, and $\mathcal {L}_{\mathit {tf}}^{\ast }$ are at least as expressive as $\mathcal {L}_{\mathit {tf}}^{\sim _{i}}$, use Odintsov’s [9] sand Wansing’s [16] observations that $\lnot \varphi$ can be defined as $\varphi \to _{t}\,\,\sim _{t}{}(p_{0} \to _{t}p_{0})$ or as $\varphi \to _{f}\sim _{f}{}(p_{0} \to _{f} p_{0})$, together with the fact that $\sim _{i}{}\varphi$ is equivalent with $\sim _{t} \sim _{f}{} \lnot \varphi$. □

4 Semantic and Syntactic Consequence

We now come to the characterisation of consequence relations. Let us first give semantic definitions.

Definition 9

Using for greatest lower bound in the ≤ _x order (x∈{t,f,i}) and $\bigsqcup _{x}$ for least upper bound, let the relations ⊧ _t , ⊧ _f , ⊧ _i , and ⊧ between sets of sentences be defined in the following way.

We have thrown the relation ⊧ into the mix because it models a constraint on reasoning that not only rejects loss of truth but also rejects increase in falsity when going from premises to conclusions. Requiring a computer network to preserve both truth and nonfalsity while drawing conclusions seems a reasonable demand.

The definition of ⊧ _i is just a fancy way of expressing that Γ⊧ _i Δ if and only if $\bigcap _{\gamma \in {\Gamma }}V(\gamma )\subseteq \bigcup _{\delta \in {\Delta }}V(\delta )$, for all V, but we have put it in the form above in order to stress the uniformity of the three definitions. It is worthwile, however, to decompose the ⊧ _t and ⊧ _f entailment relations a bit further.

Proposition 6

Γ⊧ _t Δ holds iff the conjunction of the following four statements holds for all valuations V.

$$\begin{array}{@{}rcl@{}} \mathbf{T}\in V(\gamma)\text{ ~for all ~}\gamma\in{\Gamma} &&\Longrightarrow \mathbf{T}\in V(\delta)\text{ ~for some ~}\delta\in{\Delta}\\ \mathbf{B}\in V(\gamma)\text{ ~for all ~}\gamma\in{\Gamma} &&\Longrightarrow \mathbf{B}\in V(\delta)\text{ ~for some ~}\delta\in{\Delta}\\ \mathbf{F} \in V(\delta)\text{ ~for all ~}\delta\in{\Delta} &&\Longrightarrow \mathbf{F} \in V(\gamma)\text{ ~for some ~}\gamma\in{\Gamma}\\ {\mathbf{N}}\in V(\delta)\text{ for all }\delta\in{\Delta} &&\Longrightarrow \mathbf{N}\in V(\gamma)\text{ ~for some ~}\gamma\in{\Gamma} \end{array} $$

Γ⊧ _f Δ, on the other hand, is true iff the conjunction of the following four statements holds for all V.

$$\begin{array}{@{}rcl@{}} \mathbf{T}\in V(\gamma)\text{ ~for all ~}\gamma\in{\Gamma} & \Longrightarrow & \mathbf{T}\in V(\delta)\text{ ~for some ~}\delta\in{\Delta}\\ \mathbf{B}\in V(\delta)\text{ ~for all ~}\delta\in{\Delta} & \Longrightarrow & \mathbf{B}\in V(\gamma)\text{ ~for some ~}\gamma\in{\Gamma}\\ \mathbf{F}\in V(\delta)\text{ ~for all ~}\delta\in{\Delta} & \Longrightarrow & \mathbf{F}\in V(\gamma)\text{~ for some ~}\gamma\in{\Gamma}\\ \mathbf{N}\in V(\gamma)\text{ ~for all ~}\gamma\in{\Gamma} & \Longrightarrow & \mathbf{N}\in V(\delta)\text{ ~for some ~}\delta\in{\Delta} \end{array} $$

Proof

By inspection, using Propositions 1 and 2. □

These decompositions inspire us to define four auxiliary entailment relations.

Definition 10

For each x∈{T,B,F,N}, define the auxiliary entailment relation ⊧ _x by

$${\Gamma}\models_{x}{\Delta} \Longleftrightarrow x\in\bigcap_{\gamma\in{\Gamma}}V(\gamma)\Rightarrow x\in\bigcup_{\delta\in{\Delta}}V(\delta), \text{~ for all valuations ~}V $$

Note that no pair of these relations or their inverses are equivalent on sets of premises and conclusions from $\mathcal {L}_{\mathit {tfi}}$.

Proposition 7

The relations ⊧ _T , ⊧ _F ,⊧ _N ,⊧ _B , and their inverses are pairwise distinct on $\mathcal {L}_{\mathit {tfi}}$.

Proof

None of these relations is equivalent with any of their inverses, for $\varnothing \models _{x}\mathsf {n}\mathsf {f}\mathsf {t}\mathsf {b}$ for all x ∈ {T, B, F, N} while $\mathsf {n}\mathsf {f}\mathsf {t}\mathsf {b}\models _{x}\varnothing$ holds for none. Note further that n f t b⊧ _x n holds for x=N, but not for any other of the three values for x, so that ⊧ _N is different from ⊧ _T ,⊧ _F , and ⊧ _B . Showing that other relations ⊧ _x and ⊧ _y are distinct goes in an entirely similar way. □

Proposition 7 is in stark contrast with what is the case in less expressive logics, in which not all elements of 1 6 can be named. See Shramko & Wansing [14, Lemma 4.2]. A similar situation obtains with respect to Belnap’s original four-valued logic versus a functionally complete extension (see Muskens [8]).

Given our definitions thus far the following equivalences between our main consequence relations and certain combinations of the auxiliary ones obviously hold.

$$\begin{array}{ll} {\Gamma}\models_{t}{\Delta} &\Longleftrightarrow {\Gamma}\models_{\mathbf{T}}{\Delta}\text{ ~and~} {\Gamma}\models_{\mathbf{B}}{\Delta}\text{~ and ~} {\Delta}\models_{\mathbf{F}}{\Gamma}\text{~ and ~} {\Delta}\models_{\mathbf{N}}{\Gamma}\\ {\Gamma}\models_{f}{\Delta} &\Longleftrightarrow {\Gamma}\models_{\mathbf{T}}{\Delta}\text{~ and ~} {\Delta}\models_{\mathbf{B}}{\Gamma}\text{~ and ~} {\Delta}\models_{\mathbf{F}}{\Gamma}\text{~ and ~} {\Gamma}\models_{\mathbf{N}}{\Delta}\\ {\Gamma}\models_{i}{\Delta} &\Longleftrightarrow {\Gamma}\models_{\mathbf{T}}{\Delta}\text{~ and ~} {\Gamma}\models_{\mathbf{B}}{\Delta}\text{~ and ~} {\Gamma}\models_{\mathbf{F}}{\Delta}\text{~ and ~} {\Gamma}\models_{\mathbf{N}}{\Delta} \end{array} $$

The idea now is to define four syntactic entailment relations $\vdash _{x} (x\in \{{\mathbf {T}},{\mathbf {B}},{\mathbf {F}},{\mathbf {N}}\})$, each one characterising its semantic counterpart ⊧ _x . In this way the relations ⊧ _t , ⊧ _f , ⊧ _i , and ⊧ will also be provided with syntactic characterisations. We will do this with the help of the signed tableau calculus P L _{1 6} (the name stands for ‘ 1 6-valued propositional logic’). This calculus will make use of eight signs t, f, n, b, t̸, f̸, n̸, and b̸, whose informal interpretations will become clear shortly. A $signed ~~\mathcal {L}_{\mathit {tfi}} ~~sentence$ will be a pair x:φ, where x is one of these signs and φ is an $\mathcal {L}_{\mathit {tfi}}$ sentence. In Table 1 nine rule schemes are given which form the heart of our calculus. Note that each of the three conjunctions comes with two rule schemes, each allowing four instantiations of a variable x ranging over signs, while negations come with one rule scheme each and can each be instantiated in eight different ways. The rule schemes thus sum up eight rules for each connective. Conjunction rules do not change the signs of formulas, but negation rules always do.

Table 1 Tableau expansion rules for P L _{1 6}

For formal considerations it will be useful to have a general form for rules, for which we choose 𝜗/B ₁,…,B _n , where 𝜗 is a signed sentence called the top formula of the rule and each B _i is a set of signed sentences called a set of bottom formulas of the rule. For example, one instantiation of $({\land _{f}^{2}})$ could formally be written as n̸: φ∧ _f ψ / {n̸:φ},{n̸:ψ} and one instantiation of the $(\land _{i}^{1})$ rule could be expressed as f:φ∧ _i ψ / {f:φ, f:ψ}. This general form is useful, even though neither the number of sets of bottom formulas nor their cardinality ever exceeds 2.

Tableaux will be certain sets of branches. Let us study the latter and some of the syntactic and semantic properties of notions connected with them before we define the tableaux themselves.

Definition 11

A (tableau) branch is a set of signed sentences. A branch is closed if it contains signed sentences x:φ and x̸:φ for x∈{n,f,t,b}. A branch that is not closed is called open.

If $\mathcal {B}$ is a branch and $\mathsf {x}:\varphi \in \mathcal {B}$ is a signed sentence, then x:φ is fulfilled in $\mathcal {B}$ if (a) φ is atomic, or (b) φ is complex and $B_{i}\subseteq \mathcal {B}$ for one set of bottom formulas of the unique rule x:φ/B ₁,…,B _n . A branch $\mathcal {B}$ is completed if $\mathcal {B}$ is closed or 𝜗 is fulfilled in $\mathcal {B}$ for every $\vartheta \in \mathcal {B}$.

Satisfiability of branches will be a central notion. We define it as follows.

Definition 12

Let Θ be a set of signed $\mathcal {L}_{\mathit {tfi}}$ sentences and let V be an $\mathcal {L}_{\mathit {tfi}}$ valuation. We say that V satisfies Θ iff the following statements hold.

$$\begin{array}{cc} {\mathsf{t}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{T}}\in V(\varphi) & \quad \mathsf{\not{t}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{T}}\notin V(\varphi)\\ {\mathsf{f}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{F}}\in V(\varphi) &\quad \mathsf{\not{f}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{F}}\notin V(\varphi)\\ {\mathsf{n}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{N}}\in V(\varphi) &\quad \mathsf{\not{n}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{N}}\notin V(\varphi)\\ {\mathsf{b}}:\varphi\in{\Theta}~\Rightarrow {\mathbf{B}}\in V(\varphi) &\quad \mathsf{\not{b}}:\varphi\in{\Theta}~ \Rightarrow {\mathbf{B}}\notin V(\varphi) \end{array} $$

So the signs wear their interpretations on their sleeves. We also say that V satisfies 𝜗 if V satisfies {𝜗} and that a signed sentence or a set of signed sentences is satisfiable if some V satisfies it.

Satisfaction is preserved from the top formula in a rule to one of its sets of bottom formulas and vice versa, as the following proposition attests.

Proposition 8

For any instantiation of a rule scheme in Table 1 , a valuation satisfies the top formula of the rule if and only if it satisfies a set of bottom formulas of the rule.

Proof

By inspection, using Proposition 2 and Definition 3. □

It is immediate from the definitions that a branch that is satisfiable cannot be closed. The following also holds.

Lemma 1

A branch that is completed and open is satisfiable.

Proof

Let $\mathcal {B}$ be completed and open and, for all propositional constants p, let

$$\begin{array}{@{}rcl@{}} V(p)=\{x\mid(x={\mathbf{T}}\text{~ and ~}{\mathsf{t}}:p\in\mathcal{B})\text{~ or ~} (x={\mathbf{F}}\text{~ and ~}{\mathsf{f}}:p\in\mathcal{B})\text{~ or ~}\\ (x={\mathbf{N}}\text{~ and ~}{\mathsf{n}}:p\in\mathcal{B})\text{~ or ~} (x={\mathbf{B}}\text{~ and ~}{\mathsf{b}}:p\in\mathcal{B})\} \end{array} $$

We prove by induction on formula complexity that V satisfies all signed sentences $\mathsf {x}:\varphi \in \mathcal {B}$. If φ is a propositional constant, then V satisfies x:φ by the definition just given and the fact that $\mathcal {B}$ is open. So, let $\mathsf {x}:\varphi \in \mathcal {B}$ for some sign x and complex formula φ. Since $\mathcal {B}$ is completed, a set of bottom formulas B of the unique rule of which x:φ is the top formula is a subset of $\mathcal {B}$. But, for all signed sentences y:ψ∈B, ψ is a subformula of φ, so that, by induction, V satisfies y:ψ. So V satisfies B, and by Proposition 8, V satisfies x:φ. □

Let us now define tableaux.

Definition 13

Let $\mathcal {T}$ and $\mathcal {T}^{\prime }$ be sets of branches. We say that $\mathcal {T}^{\prime }$ is a one-step expansion of $\mathcal {T}$ if, for some $\mathcal {B}\in \mathcal {T}, ~\vartheta \in \mathcal {B}$, and rule $\vartheta /B_{1},\ldots ,B_{n}, ~\mathcal {T}^{\prime }=(\mathcal {T}\backslash \{\mathcal {B}\})\cup \{\mathcal {B}\cup B_{1},\ldots ,\mathcal {B}\cup B_{n}\}$.

Let $\mathcal {B}$ be a finite branch. A set of branches $\mathcal {T}$ is a tableau with initial branch $\mathcal {B}$ if there is a sequence $\mathcal {T}_{0},\mathcal {T}_{1},\ldots ,\mathcal {T}_{n}$ such that $\mathcal {T}_{0}=\{\mathcal {B}\},~\mathcal {T}_{n}=\mathcal {T}$, and each $\mathcal {T}_{i+1}$ is a one-step expansion of $\mathcal {T}_{i}~~(0\leq i < n)$. We also say that a finite $\mathcal {B}$ has tableau $\mathcal {T}$ if $\mathcal {T}$ is a tableau with initial branch $\mathcal {B}$. A tableau $\mathcal {T}$ is open if some $\mathcal {B}\in \mathcal {T}$ is open, otherwise $\mathcal {T}$ is closed. A tableau is completed if each of its branches is completed.

Proposition 9

(a) Every finite branch has a tableau that is completed. (b) Let $\mathcal {T}$ be a tableau with initial branch $\mathcal {B}$ . If $\mathcal {B}$ is satisfiable then there is a satisfiable branch $\mathcal {B}^{\prime }$ such that $\mathcal {B}\subseteq \mathcal {B}^{\prime }\in \mathcal {T}$.

Proof

The (a) part is proved just as in classical propositional logic. For the (b) part, consider the sequence $\{\mathcal {B}\}=\mathcal {T}_{0},\mathcal {T}_{1},\ldots ,\mathcal {T}_{n}=\mathcal {T}$ that must exist according to the previous definition and do an induction on n, using Proposition 8. □

With the help of this Proposition and Lemma 1 the following lemma now follows immediately.

Lemma 2

A finite set of signed sentences is unsatisfiable iff it has a closed tableau.

Proof

Suppose the finite set of signed sentences $\mathcal {B}$ is unsatisfiable. By the previous proposition $\mathcal {B}$ has a completed tableau $\mathcal {T}$. Since $\mathcal {B}$ is included in every branch of $\mathcal {T}$, no such branch can be satisfiable. By Lemma 1 it follows that $\mathcal {T}$ must be closed. Conversely, assume that $\mathcal {B}$ is satisfiable. Then $\mathcal {B}$ has a completed tableau $\mathcal {T}$ with at least one satisfiable branch, so that $\mathcal {T}$ cannot be closed. □

With the help of our tableaux we define four auxiliary syntactic consequence relations.

Definition 14

Let Γ and Δ be finite sets of $\mathcal {L}_{\mathit {tfi}}$ sentences and define

$$\begin{array}{@{}rcl@{}} {\Gamma}\vdash_{{\mathbf{T}}}{\Delta} & :=& \{{\mathsf{t}}:\varphi\mid\varphi\in{\Gamma}\}\cup \{\mathsf{\not{t}}:\varphi\mid\varphi\in{\Delta}\} \text{~ has a closed tableau;~}\\ {\Gamma}\vdash_{{\mathbf{F}}}{\Delta} & :=& \{{\mathsf{f}}:\varphi\mid\varphi\in{\Gamma}\}\cup \{\mathsf{\not{f}}:\varphi\mid\varphi\in{\Delta}\} \text{~ has a closed tableau;~}\\ {\Gamma}\vdash_{{\mathbf{N}}}{\Delta} & :=& \{{\mathsf{n}}:\varphi\mid\varphi\in{\Gamma}\}\cup \{\mathsf{\not{n}}:\varphi\mid\varphi\in{\Delta}\} \text{~ has a closed tableau;~}\\ {\Gamma}\vdash_{{\mathbf{B}}}{\Delta} & :=& \{{\mathsf{b}}:\varphi\mid\varphi\in{\Gamma}\}\cup \{\mathsf{\not{b}}:\varphi\mid\varphi\in{\Delta}\} \text{~ has a closed tableau.~} \end{array} $$

Using Lemma 2 it immediately follows that these provide sound and complete characterisations of the auxiliary semantic entailment relations defined earlier.

Lemma 3

${\Gamma }\models _{x}{\Delta }\Longleftrightarrow {\Gamma }\vdash _{x}{\Delta }$ , for each x ∈ { T, B, F, N }.

Proof

Let $\mathcal {B}_{{\mathbf {T}}}=\{{\mathsf {t}}:\varphi \mid \varphi \in {\Gamma }\}\cup \{\mathsf {\not {t}}:\varphi \mid \varphi \in {\Delta }\}$. Then ${\Gamma }\models _{{\mathbf {T}}}{\Delta } \Longleftrightarrow \mathcal {B}_{{\mathbf {T}}}$ is unsatisfiable $\Longleftrightarrow \mathcal {B}_{{\mathbf {T}}}$ has a closed tableau $\Longleftrightarrow {\Gamma }\vdash _{{\mathbf {T}}}{\Delta }$. The other cases are quite similar. □

Definition 15

Let Γ and Δ be finite sets of $\mathcal {L}_{\mathit {tfi}}$ sentences. Define

$$\begin{array}{@{}rcl@{}} {\Gamma}\vdash_{t}{\Delta} &\quad\Longleftrightarrow\quad& {\Gamma}\vdash_{{\mathbf{T}}}{\Delta}\text{~ and ~} {\Gamma}\vdash_{{\mathbf{B}}}{\Delta}\text{~ and ~} {\Delta}\vdash_{{\mathbf{F}}}{\Gamma}\text{~ and ~} {\Delta}\vdash_{{\mathbf{N}}}{\Gamma}\\ {\Gamma}\vdash_{f}{\Delta} &\quad\Longleftrightarrow\quad& {\Gamma}\vdash_{{\mathbf{T}}}{\Delta}\text{~ and ~} {\Delta}\vdash_{{\mathbf{B}}}{\Gamma}\text{~ and ~} {\Delta}\vdash_{{\mathbf{F}}}{\Gamma}\text{~ and ~} {\Gamma}\vdash_{{\mathbf{N}}}{\Delta}\\ {\Gamma}\vdash_{i}{\Delta} &\quad\Longleftrightarrow\quad& {\Gamma}\vdash_{{\mathbf{T}}}{\Delta}\text{~ and ~} {\Gamma}\vdash_{{\mathbf{B}}}{\Delta}\text{ and ~} {\Gamma}\vdash_{{\mathbf{F}}}{\Delta}\text{~ and ~} {\Gamma}\vdash_{{\mathbf{N}}}{\Delta}\\ {\Gamma}\vdash{\Delta} &\quad\Longleftrightarrow\quad& {\Gamma}\vdash_{t}{\Delta}\text{~ and ~} {\Gamma}\vdash_{f}{\Delta} \end{array} $$

From Lemma 3 and our definitions the next theorem now immediately follows.

Theorem 1

If Γ and Δ are finite sets of $\mathcal {L}_{\mathit {tfi}}$ sentences the following hold.

$$\begin{array}{ll} {\Gamma}\models_{t}{\Delta}~\Longleftrightarrow{\Gamma}\vdash_{t}{\Delta}\quad & \quad{\Gamma}\models_{f}{\Delta}~\Longleftrightarrow{\Gamma}\vdash_{f}{\Delta}\\ {\Gamma}\models_{i}{\Delta}~\Longleftrightarrow{\Gamma}\vdash_{i}{\Delta}\quad & \quad{\Gamma}\models{\Delta}~\Longleftrightarrow{\Gamma}\vdash_{t}{\Delta}\text{~ and ~} {\Gamma}\vdash_{f}{\Delta} \end{array} $$

This solves the characterisation problem of the logics connected with $\mathcal {L}_{\mathit {tfi}}$. Finite sequents can now be decided with the help of developing several tableaus. In general four tableaus are needed to decide ⊧ _t , ⊧ _f , or ⊧ _i sequents and six are needed to decide sequents on the basis of ⊧. It may of course happen that fewer tableaux are needed if sequents have a special form. For ⊧ _t sequents from $\mathcal {L}_{t}$, the language based on {∧ _t ,∼ _t }, only one tableau needs to be developed, for example, as the others will be isomorphic. This is already clear from Shramko & Wansing’s [14, Lemma 4.2 ], but can also be glossed from our tableau rules.

5 Conclusion

We have given an analytic tableau calculus P L _{1 6} for the whole of S I X T E E N ₃, with connectives for all its truth functions. While each connective comes with eight rules and in general several tableaux must be developed in order to check entailments (six tableaux, for instance, in the case of ⊧ entailments), the calculus is still essentially simple, as the many rules can be brought under much fewer rule schemes and the system that results has a remarkable family resemblance to the usual signed tableau calculus for classical propositional logic.³