A General Relational Semantics of Propositional Logic: Axiomatization

Abstract

In the chapter on quantum logic in Volume 6 of Handbook of Philosophical Logic, Dalla Chiara and Giuntini make an interesting observation that there is a unified relational semantics underlying both the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic and ortho-logic. In this paper, we contribute to a systematic investigation of this relational semantics by providing an axiomatization of its logic.

Supported by NSSFC (No. 20CZX048).

1 Introduction

Intuitionistic logic [7] and quantum logic [2] are two important kinds of non-classical logic. They were inspired by the observation that some laws in classical propositional logic are untenable under some considerations from philosophy of mathematics or quantum physics. At the beginning, they were studied as formal proof calculi in which some laws in classical logic are absent. To be precise, we do not have in propositional intuitionistic logic the law of double negation and a part of De Morgan Laws, while in quantum logic the distributive laws between conjunction and disjunction are missing.

Around 1970, after the genesis of relational semantics in modal logic, relational semantics of intuitionistic logic [1, 8] and that of quantum logic [6] were also proposed. These formal semantics prove to be fruitful in the study of these two logics and in addition reveal some interesting technical similarities of the logics. (Please refer to the textbook [4] for intuitionistic logic and the handbook chapter [5] for quantum logic.) The main idea is to use a Kripke frame, i.e. a non-empty set W equipped with a binary relation $\rightarrow$, to interpret these two propositional logics. The intuition behind W is in intuitionistic logic the set of stages of mental construction of mathematical objects and in quantum logic the set of pure states of a quantum system, respectively. The intuition behind ${\rightarrow }$ is in intuitionistic logic the progress from one stage of mental construction to another and in quantum logic the non-orthogonality relation between pure states, respectively.

There are two key features of this interpretation. One of them is that the fundamental level of interpretation, i.e. the notion of truth, is local and bivalent. To be precise, the formal notion of truth is among a Kripke frame $(W,{\rightarrow })$, an element $s \in W$ and a formula $\varphi$, instead of being between a Kripke frame and a formula. Moreover, either $\varphi$ is true at s in $(W,{\rightarrow })$ or $\varphi$ is false at s in $(W,{\rightarrow })$ (Page 26 in [4] for intuitionistic logic and Definition 2.2 in [6] for quantum logic). Under such an interpretation the proposition expressed by a formula $\varphi$ is the set of elements of W at which $\varphi$ is true. The other feature of this interpretation is that not every subset of W is a proposition. A proposition satisfies in intuitionistic logic a property called ‘persistent’¹ and in quantum logic a property called ‘bi-orthogonally closed’² . If every subset of W is a proposition, we get classical logic; by restricting our attention to special subsets of W, from an algebraic point of view, we get sublattices of the power set algebra on W which are not Boolean.

This interpretation provides a unified framework for both intuitionistic logic and quantum logic which reflects some intuitions behind these two logics and thus is not as purely technical as algebraic semantics. However, the logics still seem very different. In intuitionistic logic we study the persistent subsets of W in a Kripke frame $(W,{\rightarrow })$ where ${\rightarrow }$ satisfies at least Reflexivity and Transitivity (Page 25 in [4]), while in quantum logic we study the bi-orthogonally closed subsets of W in a Kripke frame $(W,{\rightarrow })$ where ${\rightarrow }$ satisfies at least Reflexivity and Symmetry (Definition 2.1 in [6]³ ).

In [5] (pp. 139–140) Dalla Chiara and Giuntini make an interesting observation that, despite the difference on the involved classes of Kripke frames, intuitionistic logic and quantum logic care about the same kind of special subsets of W. In other words, there is a unified property of subsets of W such that, when ${\rightarrow }$ satisfies Reflexivity and Transitivity, it is equivalent to being persistent and, when ${\rightarrow }$ satisfies Reflexivity and Symmetry, it is equivalent to being bi-orthogonally closed. Technically this points to a unified notion of propositions in a relational semantics for both intuitionistic logic and quantum logic. We acknowledge that the motivations behind intuitionistic logic and quantum logic are completely different, and that at present there is no meaningful interpretation of this unified notion of propositions, as far as we know. However, we still hope that a study of the technical aspect of this unified notion of propositions in relational semantics of propositional logic may eventually lead to something common and interesting about the notion of propositions in intensional logics.

In this paper we contribute to a systematic investigation of this formal semantics by providing an axiomatization of its logic. The formal language we use only has two connectives $\lnot$ and $\wedge$. We leave out disjunction and implication, because both of them are defined differently in intuitionistic logic and quantum logic. (Please refer to Page 26 in [4] for intuitionistic logic and Page 137 and Sect. 3 in [5] for quantum logic). The axiomatization is essentially in the style of natural deduction, but we adopt an abstract, rigorous and concise treatment and define it as the smallest relation between a set of formulas and a formula that satisfies some syntactic properties. Finally, since the logic is weak, we write the proofs in greater details than normal so that it is convenient for the readers to check what is used in which step and whether we take some unwarranted things for granted.

The remaining part of this paper is organized as follows: In Sect. 2 we present the logic, including the formal language and the definitions of semantic consequence and syntactic consequence. We also prove the soundness and completeness theorem. In Sect. 3 we briefly discuss how the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic and quantum logic can be considered as extensions of our logic, which is the observation in [5]. We add nothing new here but just flesh out this observation by proving some claims without proofs in [5]. Our techniques are useful in proving soundness and completeness of the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic and ortho-logic, the smallest logic in quantum logic; and this will be presented in the appendices. In Sect. 4 we discuss some interesting topics for future work.

2 The Logic $\mathbf {PL}$

2.1 Formal Language

Definition 1

$\mathsf {PV}$ is a countably infinite set of propositional variables.

Formulas are defined as follows:

$$ \varphi \,::\,= p \mid ( \lnot \varphi ) \mid ( \varphi \wedge \varphi ) \text{, } \text{ where } p \in \mathsf {PV} $$

Denote by $\mathsf {Form}$ the set of formulas. Moreover, we may omit the parentheses with the assumption that $\lnot$ has priority over $\wedge$.

2.2 Semantic Consequence

Definition 2

A frame is an ordered pair $\mathfrak {F} = (W, {\rightarrow })$ such that W is a non-empty set and ${\rightarrow } \subseteq W \times W$ satisfies Reflexivity, i.e. $s \rightarrow s$ for each $s \in W$.

A proposition⁴ in a frame $\mathfrak {F} = (W, {\rightarrow })$ is a set $X \subseteq W$ such that, for each $s \in W$, the following are equivalent:

• (i) $s \in X$;

• (ii) for each $t \in W$, $s \rightarrow t$ implies that there is a $u \in X$ satisfying $u \rightarrow t$.

Denote by $\mathcal {P} (\mathfrak {F})$ the set of propositions of $\mathfrak {F}$.

Remark 1

Note that, for each $X \subseteq W$ in a frame $\mathfrak {F} = (W, {\rightarrow })$, for each $s \in W$, the direction from (i) to (ii) is trivial and only the direction from (ii) to (i) is substantial in the definition of propositions. Hence in the following we only show the proof of the latter direction when proving that a set is a proposition.

Definition 3

A model is an ordered pair $\mathfrak {M} = (\mathfrak {F}, V)$, where $\mathfrak {F} = (W, {\rightarrow })$ is a frame and V is a function from $\mathsf {PV}$ to $\mathcal {P} (\mathfrak {F})$.

Remark 2

Note that V maps each $p \in \mathsf {PV}$ to an element of $\mathcal {P} (\mathfrak {F})$, instead of an element of $\wp (W)$.⁵

Definition 4

Define a satisfaction relation  ${\models }$  between a model $\mathfrak {M} = (W, {\rightarrow }, V)$, $s \in W$ and $\varphi \in \mathsf {Form}$ recursively as follows:

• $\mathfrak {M}, s \,\models \, p$, if $s \in V (p)$;

• $\mathfrak {M}, s \,\models \, (\varphi \wedge \psi )$, if $\mathfrak {M}, s \,\models \, \varphi$ and $\mathfrak {M}, s \,\models \, \psi$;

• $\mathfrak {M}, s \,\models \, (\lnot \varphi )$, if, for each $t \in W$, $s \rightarrow t$ implies that $\mathfrak {M}, t \,\not \models \, \varphi$.

For each $\varGamma \subseteq \mathsf {Form}$, $\mathfrak {M}, s \,\models \, \varGamma$ means that, for each $\gamma \in \varGamma$, $\mathfrak {M}, s \,\models \, \gamma$.

We write $\Vert \varphi \Vert$ for $\{ s \in W \mid \mathfrak {M}, s \,\models \, \varphi \}$.

Remark 3

Note that in a model $\mathfrak {M} = (W, {\rightarrow }, V)$ by definition, for any $p \in \mathsf {PV}$ and $\varphi , \psi \in \mathsf {Form}$,

• 1. $\Vert p \Vert = V (p)$;

• 2. $\Vert (\varphi \wedge \psi ) \Vert = \Vert \varphi \Vert \cap \Vert \psi \Vert$;

• 3. $\Vert (\lnot \varphi ) \Vert = - \Vert \varphi \Vert$, where, for an $X \subseteq W$, $-X$, called the strong complement of X, is defined to be $\{ s \in W \mid \text{ for } \text{ each } t \in W \text{, } \text{ if } s \rightarrow t \text{, } \text{ then } t \not \in X \}$.

Lemma 1

Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model. For each $\varphi \in \mathsf {Form}$, $\Vert \varphi \Vert$ is a proposition.

Proof

Use induction on the structure of formula.

In the base step, $\varphi$ is a $p \in \mathsf {PV}$. By definition $\Vert p \Vert = V (p)$ is a proposition.

In the induction step, consider two cases.

In the first case, $\varphi$ is $\lnot \psi$. Assume that, for each t, if $s \rightarrow t$, then there is a u such that $u \in \Vert \lnot \psi \Vert$ and $u \rightarrow t$. For each t satisfying $s \rightarrow t$, by the assumption there is a u such that $u \in - \Vert \psi \Vert$ and $u \rightarrow t$, so $t \not \in \Vert \psi \Vert$. Thus $s \in - \Vert \psi \Vert = \Vert \lnot \psi \Vert$.

In the second case, $\varphi$ is $\psi \wedge \theta$. Assume that, for each t, if $s \rightarrow t$, then there is a u such that $u \in \Vert \psi \wedge \theta \Vert$ and $u \rightarrow t$. For each t satisfying $s \rightarrow t$, by the assumption there is a u such that $u \in \Vert \psi \Vert \cap \Vert \theta \Vert$ and $u \rightarrow t$, so this u is such that $u \in \Vert \psi \Vert$ and $u \rightarrow t$. By IH $\Vert \psi \Vert$ is a proposition, so $s \in \Vert \psi \Vert$. Similarly we can show that $s \in \Vert \theta \Vert$. Therefore, $s \in \Vert \psi \Vert \cap \Vert \theta \Vert = \Vert \psi \wedge \theta \Vert$.    $\square$

Definition 5

For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varphi$ is a semantic consequence of $\varGamma$, denoted by $\varGamma \,\models \, \varphi$, if, for any model $\mathfrak {M} = (W, {\rightarrow }, V)$ and $s \in W$, $\mathfrak {M}, s \,\models \, \varGamma$ implies that $\mathfrak {M}, s \,\models \, \varphi$.

2.3 Syntactic Consequence

Definition 6

Let ${\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form}$.

• 1. For any $\varGamma \in \wp (\mathsf {Form})$ and $\varphi \in \mathsf {Form}$, $\varphi$ is an $\mathbf {L}$-syntactic consequence of $\varGamma$, if $(\varGamma , \varphi ) \in {\vdash _\mathbf {L}}$. In this case, for convenience, we write $\varGamma \vdash _\mathbf {L} \varphi$. Moreover, we write $\psi \vdash _\mathbf {L} \varphi$ for $\{ \psi \} \vdash _\mathbf {L} \varphi$ and $\vdash _\mathbf {L} \varphi$ for $\emptyset \vdash _\mathbf {L} \varphi$.

• 2. $\varGamma \in \wp (\mathsf {Form})$ is $\mathbf {L}$-consistent, if there is no $\varphi \in \mathsf {Form}$ such that $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \lnot \varphi$.

• 3. $\varGamma \in \wp (\mathsf {Form})$ is $\mathbf {L}$-closed, if, for each $\varphi \in \mathsf {Form}$, $\varGamma \vdash _\mathbf {L} \varphi$ implies that $\varphi \in \varGamma$.

The following are some syntactic properties of a relation ${\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form}$ (to make them easier to read, we omit the universal quantifiers for $\varGamma , \varDelta \in \wp (\mathsf {Form})$ and $\varphi , \psi \in \mathsf {Form}$ at the beginning of each of the properties):

(A):

$\varGamma \cup \{ \varphi \} \vdash _\mathbf {L} \varphi$;

($\wedge$I):

if $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \psi$, then $\varGamma \vdash _\mathbf {L} \varphi \wedge \psi$;

($\wedge$E):

if $\varGamma \vdash _\mathbf {L} \varphi \wedge \psi$, then $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \psi$;

(Exp):

if $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \lnot \varphi$, then $\varGamma \vdash _\mathbf {L} \psi$;

(Mon):

if $\varGamma \subseteq \varDelta$ and $\varGamma \vdash _\mathbf {L} \varphi$, then $\varDelta \vdash _\mathbf {L} \varphi$;

(Cut):

if $\varGamma \cup \{ \psi \} \vdash _\mathbf {L} \varphi$ and $\varDelta \vdash _\mathbf {L} \psi$, then $\varGamma \cup \varDelta \vdash _\mathbf {L} \varphi$;

($\lnot$Iw):

if $\varphi \vdash _\mathbf {L} \psi$ and $\varphi \vdash _\mathbf {L} \lnot \psi$, then $\vdash _\mathbf {L} \lnot \varphi$;

(Ctr):

if $\varphi \vdash _\mathbf {L} \psi$, then $\lnot \psi \vdash _\mathbf {L} \lnot \varphi$;

($\lnot$I):

if $\varGamma \cup \{ \varphi \} \vdash _\mathbf {L} \psi$ and $\varGamma \cup \{ \varphi \} \vdash _\mathbf {L} \lnot \psi$, then $\varGamma \vdash _\mathbf {L} \lnot \varphi$;

($\lnot ^2$I):

$\varGamma \cup \{ \varphi \} \vdash _\mathbf {L} \lnot \lnot \varphi$;

($\lnot ^2$E):

$\varGamma \cup \{ \lnot \lnot \varphi \} \vdash _\mathbf {L} \varphi$;

(Com):

if $\varGamma \vdash _\mathbf {L} \varphi$, there is a finite set $\varGamma ' \subseteq \varGamma$ such that $\varGamma ' \vdash _\mathbf {L} \varphi$.

Definition 7

We define three special syntactic consequence relations and mark them by special subscripts $\mathbf {PL}$, $\mathbf {IL}$ and $\mathbf {OL}$, respectively. $\mathbf {IL}$ stands for intuitionistic logic and $\mathbf {OL}$ stands for ortho-logic.

$$\begin{aligned} {\vdash _{\mathbf {PL}}} = \bigcap \Big \{&{\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form} \mid \\&\ {\vdash _\mathbf {L}} \text{ satisfies } \text{(A),( }\wedge \text{ I),( }\wedge \text{ E),(Exp),(Mon),(Cut),( }\lnot \text{ Iw),(Ctr) } \Big \} \\ {\vdash _{\mathbf {IL}}} = \bigcap \Big \{&{\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form} \mid \\&\ {\vdash _\mathbf {L}} \text{ satisfies } \text{(A),( }\wedge \text{ I),( }\wedge \text{ E),(Exp),(Mon),(Cut),( }\lnot \text{ I) } \Big \} \\ {\vdash _{\mathbf {OL}}} = \bigcap \Big \{&{\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form} \mid \\&{\vdash _\mathbf {L}} \text{ satisfies } \text{(A),( }\wedge \text{ I),( }\wedge \text{ E),(Exp),(Mon),(Cut),( }\lnot \text{ Iw),(Ctr),( }\lnot ^2\text{ I),( }\lnot ^2\text{ E) } \Big \} \end{aligned}$$

Lemma 2

• 1. ${\vdash _{\mathbf {PL}}}$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw) and (Ctr).

• 2. ${\vdash _{\mathbf {IL}}}$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut) and ($\lnot$I).

• 3. ${\vdash _{\mathbf {OL}}}$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw), (Ctr), ($\lnot ^2$I) and ($\lnot ^2$E).

Proof

The proof is an easy verification, because each syntactic property under consideration is expressed by a universal statement.    $\square$

Next we prove three important lemmas of syntactic consequence relations.

Lemma 3

(Extension Lemma). Let ${\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form}$ satisfies (A), (Exp), (Mon), (Cut) and (Com). For any $\varGamma \subseteq \mathsf {Form}$ and $\theta \in \mathsf {Form}$, if $\varGamma \not \vdash _\mathbf {L} \theta$, there is a $\varDelta \! \subseteq \! Form$ such that $\varDelta$ is $\mathbf {L}$-closed and $\mathbf {L}$-consistent, $\varGamma \! \subseteq \! \varDelta$ and $\theta \not \in \varDelta$.

Proof

Enumerate $\mathsf {Form}$ without repetition as $(\varphi _i : i \in \mathbb {N})$.

Define a sequence of sets of formulas $(\varGamma _i : i \in \mathbb {N})$ recursively as follows:

$$\begin{aligned} \varGamma _0&= \varGamma \\ \varGamma _{i+1}&= \left\{ \begin{array}{ll} \varGamma _{i} \cup \{ \varphi _i \}, &{} \text{ if } \varGamma _{i} \cup \{ \varphi _i \} \not \vdash _\mathbf {L} \theta \\ \varGamma _{i}, &{} \text{ otherwise } \end{array} \right. \end{aligned}$$

By induction it can be shown that (a) $\varGamma _i \subseteq \varGamma _j$, for any $i, j \in \mathbb {N}$ satisfying $i \le j$ and (b) $\varGamma _i \not \vdash _\mathbf {L} \theta$, for each $i \in \mathbb {N}$.

Let $\varDelta = \bigcup _{i \in \mathbb {N}} \varGamma _i$. Obviously $\varGamma = \varGamma _0 \subseteq \bigcup _{i \in \mathbb {N}} \varGamma _i = \varDelta$.

Note that $\varDelta \not \vdash _\mathbf {L} \theta$: Otherwise, by (Com) there is a finite subset $\varDelta ' \subseteq \varDelta$ such that $\varDelta ' \vdash _\mathbf {L} \theta$; since $\varDelta '$ is finite, there is an $n \in \mathbb {N}$ such that $\varDelta ' \subseteq \varGamma _n$, so by (Mon) $\varGamma _n \vdash _\mathbf {L} \theta$, contradicting that $\varGamma _n \not \vdash _\mathbf {L} \theta$.

Then it follows from (A) that $\theta \not \in \varDelta$ and by (Exp) $\varDelta$ is $\mathbf {L}$-consistent.

Note that $\varDelta$ is $\mathbf {L}$-closed: Assume that $\varDelta \vdash _\mathbf {L} \varphi$. Then there is an $n \in \mathbb {N}$ such that $\varphi _n = \varphi$. Hence $\varGamma _n \cup \{ \varphi _n \} \not \vdash _\mathbf {L} \theta$; otherwise, by the assumption and (Cut) $\varGamma _n \cup \varDelta \vdash _\mathbf {L} \theta$, i.e. $\varDelta \vdash _\mathbf {L} \theta$, contradicting what has just been proved. Therefore, $\varphi \in \varGamma _n \cup \{ \varphi _n \} = \varGamma _{n+1} \subseteq \bigcup _{i \in \mathbb {N}} \varGamma _i = \varDelta$.    $\square$

Lemma 4

(Conjunction Lemma). Let ${\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form}$ satisfies (A), ($\wedge$I) and ($\wedge$E). For any $\mathbf {L}$-closed and $\mathbf {L}$-consistent $\varGamma \subseteq \mathsf {Form}$ and $\varphi , \psi \in \mathsf {Form}$, $\varphi \wedge \psi \in \varGamma$, if and only if $\varphi \in \varGamma$ and $\psi \in \varGamma$.

Proof

For the ‘only if’ part, by (A) $\varGamma \vdash _\mathbf {L} \varphi \wedge \psi$. By ($\wedge$E) $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \psi$. Since $\varGamma$ is $\mathbf {L}$-closed, $\varphi \in \varGamma$ and $\psi \in \varGamma$.

For the ‘if’ part, by (A) $\varGamma \vdash _\mathbf {L} \varphi$ and $\varGamma \vdash _\mathbf {L} \psi$. By ($\wedge$I) $\varGamma \vdash _\mathbf {L} \varphi \wedge \psi$. Since $\varGamma$ is $\mathbf {L}$-closed, $\varphi \wedge \psi \in \varGamma$.    $\square$

Lemma 5

(Negation Lemma). Let ${\vdash _\mathbf {L}} \subseteq \wp (\mathsf {Form}) \times \mathsf {Form}$ satisfies (A), ($\lnot$Iw), (Ctr), (Mon), (Cut) and (Com). For any $\mathbf {L}$-closed and $\mathbf {L}$-consistent $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, the following are equivalent:

• (i) $\lnot \varphi \not \in \varGamma$;

• (ii) there is a $\varDelta \subseteq \mathsf {Form}$ such that $\varDelta$ is $\mathbf {L}$-closed and $\mathbf {L}$-consistent, $\varphi \in \varDelta$ and there is no formula $\theta$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varDelta$.

Proof

For the direction from (ii) to (i), since $\varphi \in \varDelta$, $\lnot \varphi \not \in \varGamma$.

For the direction from (i) to (ii), following the idea in the proof of Theorem 1.4 in [6], we let $\varDelta = \{ \psi \in \mathsf {Form} \mid \varphi \vdash _\mathbf {L} \psi \}$.

• 1. Show that $\varphi \in \varDelta$.

  By (A) $\varphi \vdash _\mathbf {L} \varphi$, so $\varphi \in \varDelta$.

• 2. Show that there is no formula $\theta$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varDelta$.

  Suppose (towards a contradiction) that there is a formula $\theta$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varDelta$. Then $\varphi \vdash _\mathbf {L} \theta$. By (Ctr) $\lnot \theta \vdash _\mathbf {L} \lnot \varphi$. Since $\lnot \theta \in \varGamma$, by (Mon) $\varGamma \vdash _\mathbf {L} \lnot \varphi$. Since $\varGamma$ is $\mathbf {L}$-closed, $\lnot \varphi \in \varGamma$, contradicting (i).

• 3. Show that $\varDelta$ is $\mathbf {L}$-closed.

  Assume that $\varDelta \vdash _\mathbf {L} \psi$. By (Com) there is a finite set $\varDelta ' \subseteq \varDelta$ such that $\varDelta ' \vdash _\mathbf {L} \psi$. By the definition of $\varDelta$, for each $\delta \in \varDelta '$, $\varphi \vdash _\mathbf {L} \delta$. By (Cut) $\varphi \vdash _\mathbf {L} \psi$, so $\psi \in \varDelta$.

• 4. Show that $\varDelta$ is $\mathbf {L}$-consistent.

  Suppose (towards a contradiction) that there is a formula $\psi$ such that $\varDelta \vdash _\mathbf {L} \psi$ and $\varDelta \vdash _\mathbf {L} \lnot \psi$. By Item 3 $\psi \in \varDelta$ and $\lnot \psi \in \varDelta$. By definition $\varphi \vdash _\mathbf {L} \psi$ and $\varphi \vdash _\mathbf {L} \lnot \psi$. By ($\lnot$Iw) $\vdash _\mathbf {L} \lnot \varphi$. By (Mon) $\varGamma \vdash _\mathbf {L} \lnot \varphi$. Since $\varGamma$ is $\mathbf {L}$-closed, $\lnot \varphi \in \varGamma$, contradicting (i).   $\square$

We end this subsection by proving the compactness of $\mathbf {PL}$.

Theorem 1

(Compactness Theorem of $\mathbf {PL}$). ${\vdash _\mathbf {PL}}$ satisfies (Com).

Proof

Let

$$ {\vdash } = \{ (\varGamma , \varphi ) \in \wp (\mathsf {Form}) \times \mathsf {Form} \mid \text{ there } \text{ is } \text{ a } \text{ finite } \varGamma ' \subseteq \varGamma \text{ such } \text{ that } \varGamma ' \vdash _\mathbf {PL} \varphi \} $$

It suffices to show that ${\vdash }$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw) and (Ctr). After this is done, by definition ${\vdash _\mathbf {PL}} \subseteq {\vdash }$, so ${\vdash _\mathbf {PL}}$ satisfies (Com).

(A):

Since $\{ \varphi \}$ is a finite subset of $\varGamma \cup \{ \varphi \}$ and $\varphi \vdash _\mathbf {PL} \varphi$ by (A), $\varGamma \cup \{ \varphi \} \vdash \varphi$.

($\wedge$I):

Assume that $\varGamma \vdash \varphi$ and $\varGamma \vdash \psi$. By definition there is a finite set $\varGamma ' \subseteq \varGamma$ and a finite set $\varGamma '' \subseteq \varGamma$ such that $\varGamma ' \vdash _\mathbf {PL} \varphi$ and $\varGamma '' \vdash _\mathbf {PL} \psi$. By (Mon) $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \varphi$ and $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \psi$. By ($\wedge$I) $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \varphi \wedge \psi$. Since $\varGamma ' \cup \varGamma ''$ is a finite subset of $\varGamma$, $\varGamma \vdash \varphi \wedge \psi$.

($\wedge$E):

Assume that $\varGamma \vdash \varphi \wedge \psi$. By definition there is a finite set $\varGamma ' \subseteq \varGamma$ such that $\varGamma ' \vdash _\mathbf {PL} \varphi \wedge \psi$. By ($\wedge$E) $\varGamma ' \vdash _\mathbf {PL} \varphi$ and $\varGamma ' \vdash _\mathbf {PL} \psi$. Hence $\varGamma \vdash \varphi$ and $\varGamma \vdash \psi$.

(Exp):

Assume that $\varGamma \vdash \varphi$ and $\varGamma \vdash \lnot \varphi$. By definition there is a finite set $\varGamma ' \subseteq \varGamma$ and a finite set $\varGamma '' \subseteq \varGamma$ such that $\varGamma ' \vdash _\mathbf {PL} \varphi$ and $\varGamma '' \vdash _\mathbf {PL} \lnot \varphi$. By (Mon) $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \varphi$ and $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \lnot \varphi$. By (Exp) $\varGamma ' \cup \varGamma '' \vdash _\mathbf {PL} \psi$. Since $\varGamma ' \cup \varGamma ''$ is a finite subset of $\varGamma$, $\varGamma \vdash \psi$.

(Mon):

Assume that $\varGamma \subseteq \varDelta$ and $\varGamma \vdash \varphi$. By definition there is a finite $\varGamma ' \subseteq \varGamma$ such that $\varGamma ' \vdash _\mathbf {PL} \varphi$. By the assumption $\varGamma '$ is a finite subset of $\varDelta$. Hence $\varDelta \vdash \varphi$.

(Cut):

Assume that $\varGamma \cup \{ \psi \} \vdash \varphi$ and $\varDelta \vdash \psi$. By (Mon) and definition there are two finite sets $\varGamma ' \subseteq \varGamma$ and $\varDelta ' \subseteq \varDelta$ such that $\varGamma ' \cup \{ \psi \} \vdash _\mathbf {PL} \varphi$ and $\varDelta ' \vdash _\mathbf {PL} \psi$. By (Cut) $\varGamma ' \cup \varDelta ' \vdash _\mathbf {PL} \varphi$. Since $\varGamma ' \cup \varDelta '$ is a finite subset of $\varGamma \cup \varDelta$, $\varGamma \cup \varDelta \vdash \varphi$.

($\lnot$Iw):

Assume that $\varphi \vdash \psi$ and $\varphi \vdash \lnot \psi$. By (Mon) $\varphi \vdash _\mathbf {PL} \psi$ and $\varphi \vdash _\mathbf {PL} \lnot \psi$. By ($\lnot$Iw) $\vdash _\mathbf {PL} \lnot \varphi$. Since $\emptyset$ is finite, $\vdash \lnot \varphi$.

(Ctr):

Assume that $\varphi \vdash \psi$. By definition either $\varphi \vdash _\mathbf {PL} \psi$ or $\vdash _\mathbf {PL} \psi$. In both cases by (Mon) $\varphi \vdash _\mathbf {PL} \psi$. By (Ctr) $\lnot \psi \vdash _\mathbf {PL} \lnot \varphi$. Since $\{ \lnot \psi \}$ is finite, $\lnot \psi \vdash \lnot \varphi$.    $\square$

Remark 4

By Theorem 1 the conclusions of Lemmas 3, 4 and 5 apply to ${\vdash _\mathbf {PL}}$.

2.4 Soundness and Completeness

We start from proving the soundness theorem.

Theorem 2

(Soundness Theorem of $\mathbf {PL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \vdash _\mathbf {PL} \varphi$ implies that $\varGamma \,\models \, \varphi$.

Proof

Similar to the proof of Theorem 1, it suffices to show that ${\models }$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw) and (Ctr), from which ${\vdash _\mathbf {PL}} \subseteq \,{\models }$ follows.

(A):

Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Assume that $\mathfrak {M}, s \,\models \, \varGamma \cup \{ \varphi \}$. Then $\mathfrak {M}, s \,\models \, \varphi$.

($\wedge$I):

Assume that $\varGamma \,\models \, \varphi$ and $\varGamma \,\models \, \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose that $\mathfrak {M}, s \,\models \, \varGamma$. By the assumption $\mathfrak {M}, s \,\models \, \varphi$ and $\mathfrak {M}, s \,\models \, \psi$. Hence $\mathfrak {M}, s \,\models \, \varphi \wedge \psi$.

($\wedge$E):

Assume that $\varGamma \,\models \, \varphi \wedge \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose that $\mathfrak {M}, s \,\models \, \varGamma$. By the assumption $\mathfrak {M}, s \,\models \, \varphi \wedge \psi$. Then $\mathfrak {M}, s \,\models \, \varphi$ and $\mathfrak {M}, s \,\models \, \psi$.

(Exp):

Assume that $\varGamma \,\models \, \varphi$ and $\varGamma \,\models \, \lnot \varphi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Note that $\mathfrak {M}, s \,\not \models \, \varGamma$: Suppose (towards a contradiction) that $\mathfrak {M}, s \,\models \, \varGamma$. By the assumption $\mathfrak {M}, s \,\models \, \varphi$ and $\mathfrak {M}, s \,\models \, \lnot \varphi$. Since $\mathfrak {M}, s \,\models \, \lnot \varphi$ and $s \rightarrow s$ by Reflexivity, $\mathfrak {M}, s \,\not \models \, \varphi$, contradicting that $\mathfrak {M}, s \,\models \, \varphi$. Therefore, $\varGamma \,\models \, \psi$.

(Mon):

Assume that $\varGamma \,\models \, \varphi$ and $\varGamma \subseteq \varDelta$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose that $\mathfrak {M}, s \,\models \, \varDelta$. By the assumption $\mathfrak {M}, s \,\models \, \varGamma$ and thus $\mathfrak {M}, s \,\models \, \varphi$.

(Cut):

Assume that $\varGamma \cup \{ \psi \} \,\models \, \varphi$ and $\varDelta \,\models \, \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose that $\mathfrak {M}, s \,\models \, \varGamma \cup \varDelta$. By the assumption $\mathfrak {M}, s \,\models \, \varGamma \cup \{ \psi \}$, so $\mathfrak {M}, s \,\models \, \varphi$.

($\lnot$Iw):

Assume that $\varphi \,\models \, \psi$ and $\varphi \,\models \, \lnot \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose (towards a contradiction) that $\mathfrak {M}, s \,\not \models \, \lnot \varphi$. Then there is a $t \in W$ such that $s \rightarrow t$ and $\mathfrak {M}, t \,\models \, \varphi$. By the assumption $\mathfrak {M}, t \,\models \, \psi$ and $\mathfrak {M}, t \,\models \, \lnot \psi$. Since $\mathfrak {M}, t \,\models \, \lnot \psi$ and $t \rightarrow t$ by Reflexivity, $\mathfrak {M}, t \,\not \models \, \psi$, contradicting that $\mathfrak {M}, t \,\models \, \psi$. Hence $\mathfrak {M}, s \,\models \, \lnot \varphi$.

(Ctr):

Assume that $\varphi \,\models \, \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be a model and $s \in W$. Suppose that $\mathfrak {M}, s \,\models \, \lnot \psi$. Then, for each $t \in W$, if $s \rightarrow t$, then $\mathfrak {M}, t \,\not \models \, \psi$, so $\mathfrak {M}, t \,\not \models \, \varphi$ by the assumption. Hence $\mathfrak {M}, s \,\models \, \lnot \varphi$.   $\square$

For the completeness theorem, we need the notion of the canonical model. Our definition follows Definition 3.3 in [6] and the definition on Page 160 in [5].

Definition 8

$\mathfrak {F}^\mathbf {PL}= (W^\mathbf {PL}, {\rightarrow ^\mathbf {PL}})$ is called the canonical frame of $\mathbf {PL}$, where

• $W^\mathbf {PL} = \{ \varGamma \subseteq \mathsf {Form} \mid \varGamma \text{ is } \mathbf {PL} \text{-consistent } \text{ and } \mathbf {PL} \text{-closed } \}$ ;

• $\varGamma \rightarrow ^\mathbf {PL} \varDelta$, if there is no $\theta \in \mathsf {Form}$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varDelta$.

The canonical model of $\mathbf {PL}$ is an ordered pair $\mathfrak {M}^\mathbf {PL} = (\mathfrak {F}^\mathbf {PL}, V^\mathbf {PL})$ such that $\mathfrak {F}^\mathbf {PL}$ is the canonical frame of $\mathbf {PL}$ and $V^\mathbf {PL} : \mathsf {PV} \rightarrow \wp (W^\mathbf {PL})$ is a function satisfying, for each $p \in \mathsf {PV}$, $V^\mathbf {PL} (p) = \{ \varGamma \in W^\mathbf {PL} \mid p \in \varGamma \}$.

Lemma 6

(Canonical Model Lemma).

• 1. ${\rightarrow ^\mathbf {PL}}$ satisfies Reflexivity.

• 2. For any $\varGamma \in W^\mathbf {PL}$ and $\varphi \in \mathsf {Form}$, $\mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, \varphi$ if and only if $\varphi \in \varGamma$.

Proof

For Item 1, suppose (towards a contradiction) that $\varGamma \not \rightarrow ^\mathbf {PL} \varGamma$ for some $\varGamma \in W^\mathbf {PL}$. By definition there is a $\theta \in \mathsf {Form}$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varGamma$. By (A) $\varGamma \vdash _\mathbf {PL} \lnot \theta$ and $\varGamma \vdash _\mathbf {PL} \theta$, contradicting that $\varGamma$ is $\mathbf {PL}$-consistent.

For Item 2, use induction on the structure of formula.

In the base step, $\varphi$ is a $p \in \mathsf {PV}$. By definition $\mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, p \Leftrightarrow p \in \varGamma$.

In the induction step, consider two cases. In the first case, $\varphi$ is $\psi \wedge \theta$.

$$\begin{aligned}&\quad \qquad \qquad \qquad \qquad \quad \ \ \mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, \psi \wedge \theta \\&\quad \qquad \qquad \qquad \qquad \Leftrightarrow \mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, \psi \text{ and } \mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, \theta \\&\quad \qquad \qquad \qquad \qquad \Leftrightarrow \psi \in \varGamma \text{ and } \theta \in \varGamma \qquad \qquad \qquad \qquad \qquad \qquad \quad \ \text {(by IH)} \\&\quad \qquad \qquad \qquad \qquad \Leftrightarrow \psi \wedge \theta \in \varGamma \qquad \qquad \qquad \quad \ \qquad \qquad \qquad \,\text {(by Lemma 4)} \end{aligned}$$

In the second case, $\varphi$ is $\lnot \psi$.

$$\begin{aligned}&\qquad \quad \qquad \quad \ \ \mathfrak {M}^\mathbf {PL}, \varGamma \,\models \, \lnot \psi \\&\qquad \quad \qquad \Leftrightarrow \text{ for } \text{ each } \varDelta \in W^\mathbf {PL} \text{, } \text{ if } \varGamma \rightarrow ^\mathbf {PL} \varDelta \text{, } \text{ then } \mathfrak {M}^\mathbf {PL}, \varDelta \,\not \models \, \psi \\&\quad \qquad \qquad \Leftrightarrow \text{ for } \text{ each } \varDelta \in W^\mathbf {PL} \text{, } \text{ if } \varGamma \rightarrow ^\mathbf {PL} \varDelta \text{, } \text{ then } \psi \not \in \varDelta \qquad \qquad \quad \text {(by IH)} \\&\quad \qquad \qquad \Leftrightarrow \lnot \psi \in \varGamma \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \qquad \ \,\text {(by Lemma 5)} \end{aligned}$$

   $\square$

It is not obvious that the canonical model is a model in the sense of Definition 3. We can find a $\varGamma \in W^\mathbf {PL}$ and a $p \in \mathsf {PV}$ such that $p \not \in \varGamma$ and thus $\varGamma \not \in V^\mathbf {PL} (p)$. For $\mathfrak {M}^\mathbf {PL}$ to be a model, there must be a $\varDelta \in W^\mathbf {PL}$ such that $\varGamma \rightarrow ^\mathbf {PL} \varDelta$ and, for each $\varTheta \in W^\mathbf {PL}$, $\varTheta \rightarrow ^\mathbf {PL} \varDelta$ implies that $\varTheta \not \in V^\mathbf {PL} (p)$. There is little cue on what is this $\varDelta$. Our way of solving this problem is to add a ‘twin sister’ $\varGamma '$ of $\varGamma$ such that (a) only $\varGamma$ and $\varGamma '$ access to $\varGamma '$ via the binary relation and (b) the set of formulas true at $\varGamma '$ is the same as that at $\varGamma$. In this case, there are only two elements accessing to $\varGamma '$, namely $\varGamma$ and $\varGamma '$, both of which are not in $V^\mathbf {PL} (p)$; and thus $\varGamma '$ has the required property. The tricky point is that the set of formulas true at $\varGamma '$ must be the same as that at $\varGamma$. The idea is to let $\varGamma '$ ‘see the same panorama’ as $\varGamma$. To achieve this in a way that takes care of all points in a model, a well-known technique in modal logic called ‘unravelling’ is at our disposal (Proposition 2.15 in [3]). Finally, the model obtained by unravelling in [3] does not satisfy Reflexivity. This can be solved by taking the reflexive closure of the binary relation, and it does not affect truth in the model because ${\rightarrow }^\mathbf {PL}$ satisfies Reflexivity. The above consideration leads to the following definition:

Definition 9

Let $\varGamma \in W^\mathbf {PL}$. The $\varGamma$-model is $\mathfrak {M}^\varGamma = (W^\varGamma , {\rightarrow ^\varGamma }, V^\varGamma )$, where:

• 1. $W^\varGamma = \{ (\varTheta _0, \dots , \varTheta _n) \mid n \in \mathbb {N},\ \varTheta _0, \dots , \varTheta _n \in W^\mathbf {PL} \text{ satisfy } \text{ that } \varTheta _0 = \varGamma \text{ and }$ $\varTheta _i \rightarrow ^\mathbf {PL} \varTheta _{i+1} \text{ for } \text{ each } i = 0, \dots , n-1 \}$.

• 2. $(\varTheta _0, \dots , \varTheta _m) \rightarrow ^\varGamma (\varTheta '_0, \dots , \varTheta '_n)$, if and only if one of the following is true:

  • (a) $(\varTheta _0, \dots , \varTheta _m) = (\varTheta '_0, \dots , \varTheta '_n)$;

  • (b) $(\varTheta _0, \dots , \varTheta _m) = (\varTheta '_0, \dots , \varTheta '_{n-1})$ (in this case $m +1 = n$).

• 3. For each $p \in \mathsf {PV}$, $V^\varGamma (p) = \{ (\varTheta _0, \dots , \varTheta _n) \in W^\varGamma \mid \mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, p \}$.

Lemma 7

($\varGamma$-Model Lemma) Let $\varGamma \in W^\mathbf {PL}$.

• 1. ${\rightarrow ^\varGamma }$ satisfies Reflexivity;

• 2. for each $p \in \mathsf {PV}$, $V^\varGamma (p)$ is closed.

• 3. $\mathfrak {M}^\varGamma$ is a model.

Proof

Item 1 follows from Condition (a) in the definition of ${\rightarrow ^\varGamma }$.

For Item 2, assume that $(\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n) \not \in V^\varGamma (p)$. By definition $\mathfrak {M}^\mathbf {PL}, \varTheta _n \,\not \models \, p$. Consider $(\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n)$.

• 1. We show that $(\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n) \in W^\varGamma$.

  By the Canonical Model Lemma $\varTheta _n \rightarrow ^\mathbf {PL} \varTheta _n$. Since $(\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n) \in W^\varGamma$, $(\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n) \in W^\varGamma$.

• 2. We show that, for each $(\varTheta '_0, \dots , \varTheta '_m) \in W^\varGamma$, $(\varTheta '_0, \dots , \varTheta '_m) \not \in V^\varGamma (p)$, if $(\varTheta '_0, \dots , \varTheta '_m) \rightarrow ^\varGamma (\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n)$.

  Assume that $(\varTheta '_0, \dots , \varTheta '_m) \rightarrow ^\varGamma (\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n)$.

  By definition consider 2 cases.

  In the first case, $(\varTheta '_0, \dots , \varTheta '_m) = (\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n, \varTheta _n)$. Then $\varTheta '_m = \varTheta _n$. Since $\mathfrak {M}^\mathbf {PL}, \varTheta _n \,\not \models \, p$, $\mathfrak {M}^\mathbf {PL}, \varTheta '_m \,\not \models \, p$, so by definition $(\varTheta '_0, \dots , \varTheta '_m) \not \in V^\varGamma (p)$.

  In the second case, $(\varTheta '_0, \dots , \varTheta '_m) = (\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n)$. By the assumption at the very beginning $(\varTheta '_0, \dots , \varTheta '_m) = (\varTheta _0, \dots , \varTheta _{n-1}, \varTheta _n) \not \in V^\varGamma (p)$.

Therefore, $V^\varGamma (p)$ is closed.

Item 3 follows from Items 1 and 2 directly.    $\square$

Lemma 8

($\varGamma$-Model Truth Lemma). Let $\varGamma \in W^\mathbf {PL}$. For any $\varphi \in \mathsf {Form}$ and $(\varTheta _0, \dots , \varTheta _n) \in W^\varGamma$, $\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\models \, \varphi$ if and only if $\mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, \varphi$.

Proof

Use induction on the structure of formula.

In the base step, $\varphi$ is a $p \in \mathsf {PV}$. $\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\models \, p \Leftrightarrow (\varTheta _0, \dots , \varTheta _n) \in V^\varGamma (p) \Leftrightarrow \mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, p$.

In the induction step, consider two cases.

In the first case, $\varphi$ is $\psi \wedge \theta$.

$$\begin{aligned}&\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\models \, \psi \wedge \theta \\&\Leftrightarrow \mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\models \, \psi \text{ and } \mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\models \, \theta \\&\Leftrightarrow \mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, \psi \text{ and } \mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, \theta \qquad \qquad \qquad \qquad \qquad \text {(by IH)} \\&\Leftrightarrow \mathfrak {M}^\mathbf {PL}, \varTheta _n \,\models \, \psi \wedge \theta \end{aligned}$$

In the second case, $\varphi$ is $\lnot \psi$.

First assume that $\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\not \models \, \lnot \psi$. There is a $(\varTheta '_0, \dots , \varTheta '_m) \in W^\varGamma$ such that $(\varTheta _0 , \dots , \varTheta _n) \rightarrow ^\varGamma (\varTheta '_0, \dots , \varTheta '_m)$ and $\mathfrak {M}^\varGamma , (\varTheta '_0, \dots , \varTheta '_m) \,\models \, \psi$. By definition in both cases $\varTheta _n \rightarrow ^\mathbf {PL} \varTheta '_m$. By IH $\mathfrak {M}^\mathbf {PL}, \varTheta '_m \,\models \, \psi$. Hence $\mathfrak {M}^\mathbf {PL}, \varTheta _n \,\not \models \, \lnot \psi$.

Second assume that $\mathfrak {M}^\mathbf {PL}, \varTheta _n \,\not \models \, \lnot \psi$. There is a $\varDelta \in W^\mathbf {PL}$ such that $\varTheta _n \rightarrow ^\mathbf {PL} \varDelta$ and $\mathfrak {M}^\mathbf {PL}, \varDelta \,\models \, \psi$. Consider $(\varTheta _0, \dots , \varTheta _n, \varDelta )$. Since $(\varTheta _0, \dots , \varTheta _n) \in W^\varGamma$ and $\varTheta _n \rightarrow ^\mathbf {PL} \varDelta$, $(\varTheta _0, \dots , \varTheta _n, \varDelta ) \in W^\varGamma$ and $(\varTheta _0, \dots , \varTheta _n) \rightarrow ^\varGamma (\varTheta _0, \dots , \varTheta _n, \varDelta )$. Since $\mathfrak {M}^\mathbf {PL}, \varDelta \,\models \, \psi$, by IH $\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n, \varDelta ) \,\models \, \psi$. Hence $\mathfrak {M}^\varGamma , (\varTheta _0, \dots , \varTheta _n) \,\not \models \, \lnot \psi$.

   $\square$

Theorem 3

(Completeness Theorem of $\mathbf {PL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \,\models \, \varphi$ implies that $\varGamma \vdash _\mathbf {PL} \varphi$.

Proof

Assume that $\varGamma \not \vdash _\mathbf {PL} \varphi$. By Lemma 3 there is a $\varDelta \in W^\mathbf {PL}$ such that $\varGamma \subseteq \varDelta$ and $\varphi \not \in \varDelta$. By Lemma 6 $\mathfrak {M}^\mathbf {PL}, \varDelta \,\models \, \varGamma$ and $\mathfrak {M}^\mathbf {PL}, \varDelta \,\not \models \, \varphi$. By Lemma 8 $\mathfrak {M}^\varDelta , (\varDelta ) \,\models \, \varGamma$ and $\mathfrak {M}^\varDelta , (\varDelta ) \,\not \models \, \varphi$, where $(\varDelta )$ is a sequence of length 1. Since $\mathfrak {M}^\varDelta$ is a model, $\varGamma \,\not \models \, \varphi$.    $\square$

3 Extensions of $\mathbf {PL}$

In this section we briefly discuss how the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic and ortho-logic can be considered as extensions of our logic, which is the observation in [5]. Here we add nothing new but just flesh out this observation by proving some claims without proofs in [5].

3.1 Intuitionistic Logic

Definition 10

An I-frame is a frame $\mathfrak {F} = (W, {\rightarrow })$ such that ${\rightarrow }$ satisfies Transitivity, i.e., for any $s, t, u \in W$, $s \rightarrow t$ and $t \rightarrow u$ imply that $s \rightarrow u$.⁶

Lemma 9

In an I-frame $\mathfrak {F} = (W, {\rightarrow })$, for each $X \in \wp (W)$, the following are equivalent:

• (i) X is persistent, i.e., for any $s, t \in W$, if $s \in X$ and $s \rightarrow t$, then $t \in X$;

• (ii) $X \in \mathcal {P} (\mathfrak {F})$.

Proof

For the direction from (i) to (ii), let s be arbitrary. Assume that, for each $t \in W$, if $s \rightarrow t$, then there is a $u \in X$ such that $u \rightarrow t$. By Reflexivity $s \rightarrow s$. Hence there is a u such that $u \in X$ and $u \rightarrow s$. By (i) $s \in X$.

For the direction from (ii) to (i), let s and t be arbitrary such that $s \in X$ and $s \rightarrow t$. By (ii) there is a u such that $u \in X$ and $u \rightarrow t$.

Let v be arbitrary such that $t \rightarrow v$. Since $u \rightarrow t$ and $t \rightarrow v$, by Transitivity $u \rightarrow v$. So $u \in X$ is such that $u \rightarrow v$.

By the arbitrariness of v and (ii) $t \in X$.    $\square$

Definition 11

An I-model is an ordered pair $\mathfrak {M} = (\mathfrak {F}, V)$, where $\mathfrak {F}$ is an I-frame and V is a function from $\mathsf {PV}$ to $\mathcal {P} (\mathfrak {F})$.

For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varphi$ is an I-semantic consequence of $\varGamma$, denoted by $\varGamma \,\models _I\, \varphi$, if, for any I-model $\mathfrak {M} = (W, {\rightarrow }, V)$ and $s \in W$, $\mathfrak {M}, s \,\models \, \varGamma$ implies that $\mathfrak {M}, s \,\models \, \varphi$.

Remark 5

According to Lemma 9, the definition of an I-model is the same as the usual definition of a model in the relational semantics of propositional intuitionistic logic. (Please refer to Page 25 in [4]. There the binary relation is required to be anti-symmetric in addition, but in fact this does not affect the logic.) Lemma 9 is claimed without proof on pages 139–140 in [5].

Since every I-frame is a frame by definition, ${\models }\, \subseteq \,{\models _I}$, and thus the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic is an extension of our logic.

3.2 Ortho-Logic

Definition 12

An O-frame is a frame $\mathfrak {F} = (W, {\rightarrow })$ such that ${\rightarrow }$ satisfies Symmetry, i.e., for any $s, t \in W$, $s \rightarrow t$ implies $t \rightarrow s$.⁷

Lemma 10

In an O-frame $\mathfrak {F} = (W, {\rightarrow })$, for each $X \in \wp (W)$, the following are equivalent:

• (i) X is bi-orthogonally closed, i.e. $- (- X) = X$;

• (ii) $X \in \mathcal {P} (\mathfrak {F})$.

Proof

$$\begin{aligned}&X \in \mathcal {P} (\mathfrak {F}) \\ \Leftrightarrow&\text{ for } \text{ each } s \in W,\ s \in X \text{, } \text{ if } \text{ and } \text{ only } \text{ if, } \text{ for } \text{ each } t,\ s \rightarrow t \text{ implies } \text{ that } \\&\qquad \text{ there } \text{ is } \text{ a } u \text{ such } \text{ that } u \in X \text{ and } u \rightarrow t \\ \Leftrightarrow&\text{ for } \text{ each } s \in W,\ s \in X \text{, } \text{ if } \text{ and } \text{ only } \text{ if, } \text{ for } \text{ each } t,\ s \rightarrow t \text{ implies } \text{ that } \\&\qquad \text{ there } \text{ is } \text{ a } u \text{ such } \text{ that } u \in X \text{ and } t \rightarrow u \qquad \qquad \qquad \qquad \text {(by Symmetry)} \\ \Leftrightarrow&\text{ for } \text{ each } s \in W,\ s \in X \text{, } \text{ if } \text{ and } \text{ only } \text{ if, } \text{ for } \text{ each } t,\ s \rightarrow t \text{ implies } \text{ that } t \not \in - X \\ \Leftrightarrow&\text{ for } \text{ each } s \in W,\ s \in X \text{, } \text{ if } \text{ and } \text{ only } \text{ if } s \in - ( -X ) \\ \Leftrightarrow&- ( - X) = X \end{aligned}$$

   $\square$

Definition 13

An O-model is an ordered pair $\mathfrak {M} = (\mathfrak {F}, V)$, where $\mathfrak {F}$ is an O-frame and V is a function from $\mathsf {PV}$ to $\mathcal {P} (\mathfrak {F})$.

For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varphi$ is an O-semantic consequence of $\varGamma$, denoted by $\varGamma \,\models _O\, \varphi$, if, for any O-model $\mathfrak {M} = (W, {\rightarrow }, V)$ and $s \in W$, $\mathfrak {M}, s \,\models \, \varGamma$ implies that $\mathfrak {M}, s \,\models \, \varphi$.

Remark 6

According to Lemma 10, the definition of an O-model is the same as the usual definition of a model in the relational semantics of ortho-logic [6], despite the fact that in the literature usually ${\perp } {\mathop {=}\limits ^{\text {def}}} (W \times W) \setminus {\rightarrow }$ is the primitive binary relation. Lemma 10 is claimed without proof on page 140 in [5].

Since every O-frame is a frame by definition, ${\models }\, \subseteq \,{\models _O}$, and thus ortho-logic is an extension of our logic.

4 Future Work

The axiomatization result in this paper is only a part of a systematic study of this general relational semantics of propositional logic, and much more could and should be done.

First, it is interesting to pinpoint the expressive power of this relational semantics in describing Kripke frames by a van Benthem Characterization Theorem. We defer this study to an extension of this paper.

Second, we see that the present theory of this relational semantics is not as modular as that of the relational semantics of modal logic. Remember that the logics $\mathbf {IL}$ and $\mathbf {OL}$ are related to the modal logics $\mathbf {S4}$ and $\mathbf {KTB}$ via the Tarski-Mckinsey translation and Goldblatt’s translation, respectively, and there is a unified theory of relational semantics for $\mathbf {S4}$ and $\mathbf {KTB}$ and many other modal logics. However, it is not the present situation for $\mathbf {IL}$, $\mathbf {OL}$ and $\mathbf {PL}$. For an example, according to Lemma 11 in the appendix, in defining $\mathbf {IL}$, ($\lnot$Iw) and (Ctr) are no longer needed when ($\lnot$I) is present. For another example, in the completeness proofs in the appendices we see that the model for $\mathbf {IL}$ and that for $\mathbf {OL}$ are different and both are different from that for $\mathbf {PL}$, although they are related. It is interesting to see whether there is a logical theory of this relational semantics, which is as modular as the theory of relational semantics of modal logic. Conceptually, this will lead to interesting interplay between syntax and semantics. Technically, this may involve works on proof theory to find the appropriate formal system and improvement on the current completeness proofs.

Appendices

A Intuitionistic Logic

In this appendix, we apply our techniques to prove the soundness and completeness theorem for $\mathbf {IL}$, which is the $\{ {\lnot }, {\wedge } \}$-fragment of intuitionistic logic.

We start with a remark about the semantics.

Remark 7

Since every I-model is a model, by Lemmas 1 and 9 in an I-model $\Vert \varphi \Vert$ is persistent for each $\varphi \in \mathsf {Form}$.

Second, we prove some results about the syntactic consequence relation ${\vdash _\mathbf {IL}}$.

Lemma 11

${\vdash _\mathbf {IL}}$ satisfies ($\lnot$Iw) and (Ctr), and thus ${\vdash _\mathbf {PL}} \subseteq {\vdash _\mathbf {IL}}$

Proof

($\lnot$Iw) is a special case of ($\lnot$I) when $\varGamma = \emptyset$.

For (Ctr), assume that $\varphi \vdash _\mathbf {IL} \psi$. By (Mon) $\{ \varphi , \lnot \psi \} \vdash _\mathbf {IL} \psi$. By (A) $\{ \varphi , \lnot \psi \} \vdash _\mathbf {IL} \lnot \psi$. By ($\lnot$I) $\lnot \psi \vdash _\mathbf {IL} \lnot \varphi$.    $\square$

Theorem 4

(Compactness Theorem of $\mathbf {IL}$). ${\vdash _\mathbf {IL}}$ satisfies (Com).

Proof

Let

$$ {\vdash } = \{ (\varGamma , \varphi ) \in \wp (\mathsf {Form}) \times \mathsf {Form} \mid \text{ there } \text{ is } \text{ a } \text{ finite } \varGamma ' \subseteq \varGamma \text{ such } \text{ that } \varGamma ' \vdash _\mathbf {IL} \varphi \} $$

Similar to the proof of Theorem 1, it suffices to show that $\vdash$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut) and ($\lnot$I). The proofs for the first 6 properties are the same as that in Theorem 1. Here we only need to deal with ($\lnot$I).

Assume that $\varGamma \cup \{ \varphi \} \vdash \psi$ and $\varGamma \cup \{ \varphi \} \vdash \lnot \psi$. By definition and (Mon) there are two finite subsets $\varGamma '$ and $\varGamma ''$ of $\varGamma$ such that $\varGamma ' \cup \{ \varphi \} \vdash _\mathbf {IL} \psi$ and $\varGamma '' \cup \{ \varphi \} \vdash _\mathbf {IL} \lnot \psi$. By (Mon) $\varGamma ' \cup \varGamma '' \cup \{ \varphi \} \vdash _\mathbf {IL} \psi$ and $\varGamma ' \cup \varGamma '' \cup \{ \varphi \} \vdash _\mathbf {IL} \lnot \psi$. By ($\lnot$I) $\varGamma ' \cup \varGamma '' \vdash _\mathbf {IL} \lnot \varphi$. Since $\varGamma ' \cup \varGamma ''$ is a finite subset of $\varGamma$, $\varGamma \vdash \lnot \varphi$.    $\square$

Remark 8

By Lemma 11 and Theorem 4 the conclusions of Lemmas 3 and 4 apply to ${\vdash _\mathbf {IL}}$.

Lemma 12

(Negation Lemma of $\mathbf {IL}$). Let $\varGamma \subseteq \mathsf {Form}$ be $\mathbf {IL}$-closed and $\mathbf {IL}$-consistent and $\varphi \in \mathsf {Form}$. The following are equivalent:

• (i) $\lnot \varphi \not \in \varGamma$;

• (ii) there is an $\mathbf {IL}$-closed and $\mathbf {IL}$-consistent $\varDelta \subseteq \mathsf {Form}$ such that $\varGamma \cup \{ \varphi \} \subseteq \varDelta$.

Proof

For the direction from (ii) to (i), suppose (towards a contradiction) that $\lnot \varphi \in \varGamma$. Since $\varGamma \subseteq \varDelta$, $\lnot \varphi \in \varDelta$. By (A) $\varDelta \vdash _\mathbf {IL} \varphi$ and $\varDelta \vdash _\mathbf {IL} \lnot \varphi$, contradicting that $\varDelta$ is $\mathbf {IL}$-consistent.

For the direction from (i) to (ii), note that $\varGamma \cup \{ \varphi \} \not \vdash _\mathbf {IL} \lnot \varphi$: Suppose (towards a contradiction) that $\varGamma \cup \{ \varphi \} \vdash _\mathbf {IL} \lnot \varphi$. By (A) $\varGamma \cup \{ \varphi \} \vdash _\mathbf {IL} \varphi$. By ($\lnot$I) $\varGamma \vdash _\mathbf {IL} \lnot \varphi$. Since $\varGamma$ is $\mathbf {IL}$-closed, $\lnot \varphi \in \varGamma$, contradicting (i).

By Lemma 3 there is a $\varDelta \subseteq \mathsf {Form}$ such that $\varDelta$ is $\mathbf {IL}$-closed and $\mathbf {IL}$-consistent and $\varGamma \cup \{ \varphi \} \subseteq \varDelta$.    $\square$

Third, we prove the soundness theorem.

Theorem 5

(Soundness Theorem of $\mathbf {IL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \vdash _\mathbf {IL} \varphi$ implies that $\varGamma \,\models _I\, \varphi$.

Proof

It suffices to show that ${\models }$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut) and ($\lnot$I). Since every I-model is a model, the proofs for the first 6 properties are the same as in Theorem 2. Here we only need to show ($\lnot$I).

Assume that $\varGamma \cup \{ \varphi \} \,\models \, \psi$ and $\varGamma \cup \{ \varphi \} \,\models \, \lnot \psi$. Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be an I-model and $s \in W$ such that $\mathfrak {M}, s \,\models \, \varGamma$. Suppose (towards a contradiction) that $\mathfrak {M}, s \,\not \models \, \lnot \varphi$. Then there is a $t \in W$ such that $s \rightarrow t$ and $\mathfrak {M}, t \,\models \, \varphi$. Since $s \rightarrow t$ and $\mathfrak {M}, s \,\models \, \varGamma$, by Remark 7 $\mathfrak {M}, t \,\models \, \varGamma$, so $\mathfrak {M}, t \,\models \, \varGamma \cup \{ \varphi \}$. By the assumption $\mathfrak {M}, t \,\models \, \psi$ and $\mathfrak {M}, t \,\models \, \lnot \psi$. By Reflexivity $t \rightarrow t$, so $\mathfrak {M}, t \,\not \models \, \psi$, contradicting $\mathfrak {M}, t \,\models \, \psi$. Therefore, $\mathfrak {M}, s \,\models \, \lnot \varphi$.    $\square$

Finally, we define the canonical frame of $\mathbf {IL}$, which is standard in the literature (Pages 132–133 in [4]), and prove the completeness theorem.

Definition 14

$\mathfrak {F}^\mathbf {IL}= (W^\mathbf {IL}, {\rightarrow ^\mathbf {IL}})$ is the canonical frame of $\mathbf {IL}$, where:

• $W^\mathbf {IL} = \{ \varGamma \subseteq \mathsf {Form} \mid \varGamma \text{ is } \mathbf {IL} \text{-consistent } \text{ and } \mathbf {IL} \text{-closed } \}$;

• ${\rightarrow ^\mathbf {IL}} = \{ (\varGamma , \varDelta ) \in W^\mathbf {IL} \times W^\mathbf {IL} \mid \varGamma \subseteq \varDelta \}$.

The canonical model of $\mathbf {IL}$ is an ordered pair $\mathfrak {M}^\mathbf {IL} = (\mathfrak {F}^\mathbf {IL}, V^\mathbf {IL})$ such that $\mathfrak {F}^\mathbf {IL}$ is the canonical frame of $\mathbf {IL}$ and $V^\mathbf {IL} : \mathsf {PV} \rightarrow \wp (W^\mathbf {IL})$ is a function such that, for each $p \in \mathsf {PV}$, $V^\mathbf {IL} (p) = \{ \varGamma \in W^\mathbf {IL} \mid p \in \varGamma \}$.

Lemma 13

(Canonical Model Lemma of $\mathbf {IL}$ ).

• 1. ${\rightarrow ^\mathbf {IL}}$ satisfies Reflexivity and Transitivity.

• 2. $\mathfrak {M}^\mathbf {IL}$ is an I-model.

• 3. For any $\varGamma \in W^\mathbf {IL}$ and $\varphi \in \mathsf {Form}$, $\mathfrak {M}^\mathbf {IL}, \varGamma \,\models \, \varphi$ if and only if $\varphi \in \varGamma$.

Proof

For Item 1, ${\rightarrow ^\mathbf {IL}} = {\subseteq }$ satisfies Reflexivity and Transitivity.

For Item 2, for any $p \in \mathsf {PV}$ and $\varGamma , \varDelta \in W^\mathbf {IL}$ such that $\varGamma \subseteq \varDelta$ and $\varGamma \in V^\mathbf {IL} (p)$, $p \in \varGamma$, so $p \in \varDelta$, i.e. $\varDelta \in V^\mathbf {IL} (p)$.

For Item 3, the proof is the same as that of Item 2 in Lemma 6, besides that here we use Lemma 12 instead of Lemma 5.    $\square$

Theorem 6

(Completeness Theorem of $\mathbf {IL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \,\models _I\, \varphi$ implies that $\varGamma \vdash _\mathbf {IL} \varphi$.

Proof

Assume that $\varGamma \not \vdash _\mathbf {IL} \varphi$. By Lemma 3 there is a $\varDelta \in W^\mathbf {IL}$ such that $\varGamma \subseteq \varDelta$ and $\varphi \not \in \varDelta$. By Lemma 13 $\mathfrak {M}^\mathbf {IL}, \varDelta \,\models \, \varGamma$ and $\mathfrak {M}^\mathbf {IL}, \varDelta \,\not \models \, \varphi$. Since $\mathfrak {M}^\mathbf {IL}$ is an I-model, $\varGamma \,\not \models _I\, \varphi$.    $\square$

B Ortho-logic

In this appendix, we apply the techniques developed before to prove the soundness and completeness theorem for ortho-logic $\mathbf {OL}$.

Our axiomatization of ortho-logic is essentially the same as that on Pages 158–159 in [5], and the results in this appendix are all in [5] (with or without proofs). Here we give detailed proofs using the results in this paper.

We start with a remark about the semantics.

Remark 9

Since every O-model is a model, by Lemmas 1 and 10 in an O-model $\Vert \varphi \Vert$ is bi-orthogonally closed for each $\varphi \in \mathsf {Form}$.

Second, we prove some results about the syntactic consequence relation ${\vdash _\mathbf {OL}}$.

Remark 10

By definition ${\vdash _\mathbf {PL}} \subseteq {\vdash _\mathbf {OL}}$.

Theorem 7

(Compactness Theorem of $\mathbf {OL}$). ${\vdash _\mathbf {OL}}$ satisfies (Com).

Proof

Let

$$ {\vdash } = \{ (\varGamma , \varphi ) \in \wp (\mathsf {Form}) \times \mathsf {Form} \mid \text{ there } \text{ is } \text{ a } \text{ finite } \varGamma ' \subseteq \varGamma \text{ such } \text{ that } \varGamma ' \vdash _\mathbf {OL} \varphi \} $$

Similar to the proof of Theorem 1, it suffices to show that $\vdash$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw), (Ctr), ($\lnot ^2$I) and ($\lnot ^2$E). The proofs for the first 8 properties are the same as that in Theorem 1. Here we only need to deal with ($\lnot ^2$I) and ($\lnot ^2$E).

By ($\lnot ^2$I) $\{ \varphi \} \vdash _\mathbf {OL} \lnot \lnot \varphi$. Since $\{ \varphi \}$ is finite, $\varGamma \cup \{ \varphi \} \vdash \lnot \lnot \varphi$. Similarly we can show that $\varGamma \cup \{ \lnot \lnot \varphi \} \vdash \varphi$.    $\square$

Remark 11

By Theorem 7 the conclusions of Lemmas 3, 4 and 5 apply to ${\vdash _\mathbf {OL}}$.

Third, we prove the soundness theorem.

Theorem 8

(Soundness Theorem of $\mathbf {OL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \vdash _\mathbf {OL} \varphi$ implies that $\varGamma \,\models _O\, \varphi$.

Proof

Similar to the proof of Theorem 2, it suffices to show that ${\models }$ satisfies (A), ($\wedge$I), ($\wedge$E), (Exp), (Mon), (Cut), ($\lnot$Iw), (Ctr), ($\lnot ^2$I) and ($\lnot ^2$E). Since every O-model is a model, the proofs for the first 8 properties are the same as in Theorem 2. Here we only need to show ($\lnot ^2$I) and ($\lnot ^2$E).

Let $\mathfrak {M} = (W, {\rightarrow }, V)$ be an O-model and $s \in W$ such that $\mathfrak {M}, s \,\models \, \varGamma \cup \{ \varphi \}$. Then $s \in \Vert \varphi \Vert$. By Remark 9 $s \in - (- \Vert \varphi \Vert )$. By Remark 3 $- (- \Vert \varphi \Vert ) = \Vert \lnot \lnot \varphi \Vert$. Hence $s \in \Vert \lnot \lnot \varphi \Vert$, i.e. $\mathfrak {M}, s \,\models \, \lnot \lnot \varphi$. Therefore, $\varGamma \cup \{ \varphi \} \,\models _O\, \lnot \lnot \varphi$.

Similarly we can show that $\varGamma \cup \{ \lnot \lnot \varphi \} \,\models _O\, \varphi$.    $\square$

Next, we define the canonical model of $\mathbf {OL}$ in exactly the same way as that of $\mathbf {PL}$ and thus as that in the literature [5, 6]. We will see that the canonical model of $\mathbf {OL}$ is an O-model.

Definition 15

$\mathfrak {F}^\mathbf {OL}= (W^\mathbf {OL}, {\rightarrow ^\mathbf {OL}})$ is the canonical frame of $\mathbf {OL}$, where:

• $W^\mathbf {OL} = \{ \varGamma \subseteq \mathsf {Form} \mid \varGamma \text{ is } \mathbf {OL} \text{-consistent } \text{ and } \mathbf {OL} \text{-closed } \}$;

• ${\rightarrow ^\mathbf {OL}} = \{ (\varGamma , \varDelta ) \in W^\mathbf {OL} \times W^\mathbf {OL} \mid \text{ there } \text{ is } \text{ no } \theta \in \mathsf {Form} \text{ such } \text{ that } \lnot \theta \in \varGamma \text{ and } \theta \in \varDelta \}$.

The canonical model of $\mathbf {OL}$ is an ordered pair $\mathfrak {M}^\mathbf {OL} = (\mathfrak {F}^\mathbf {OL}, V^\mathbf {OL})$ such that $\mathfrak {F}^\mathbf {OL}$ is the canonical frame of $\mathbf {OL}$ and $V^\mathbf {OL} : \mathsf {PV} \rightarrow \wp (W^\mathbf {OL})$ is a function such that, for each $p \in \mathsf {PV}$, $V^\mathbf {OL} (p) = \{ \varGamma \in W^\mathbf {OL} \mid p \in \varGamma \}$.

Lemma 14

(Canonical Model Lemma of $\mathbf {OL}$ )

• 1. ${\rightarrow ^\mathbf {OL}}$ satisfies Reflexivity and Symmetry.

• 2. $\mathfrak {M}^\mathbf {OL}$ is an O-model.

• 3. For any $\varGamma \in W^\mathbf {OL}$ and $\varphi \in \mathsf {Form}$, $\mathfrak {M}^\mathbf {OL}, \varGamma \,\models \, \varphi$ if and only if $\varphi \in \varGamma$.

Proof

For Item 1, Reflexivity can be proved in exactly the same way as that of ${\rightarrow ^\mathbf {PL}}$. For Symmetry, assume that $\varGamma \not \rightarrow ^\mathbf {OL} \varDelta$. Then there is a $\theta \in \mathsf {Form}$ such that $\lnot \theta \in \varGamma$ and $\theta \in \varDelta$. By ($\lnot ^2$I) $\varDelta \cup \{ \theta \} \vdash _\mathbf {OL} \lnot \lnot \theta$, i.e. $\varDelta \vdash _\mathbf {OL} \lnot \lnot \theta$. Since $\varDelta$ is $\mathbf {OL}$-closed, $\lnot \lnot \theta \in \varDelta$. Then $\varDelta \not \rightarrow ^\mathbf {OL} \varGamma$, for $\lnot \lnot \theta \in \varDelta$ and $\lnot \theta \in \varGamma$.

For Item 2, first assume that $\varGamma \in V^\mathbf {OL} (p)$. Then, for each $\varDelta \in W^\mathbf {OL}$ satisfying $\varGamma \rightarrow ^\mathbf {OL} \varDelta$, $\varDelta \rightarrow ^\mathbf {OL} \varGamma$ by Symmetry and $\varGamma \in V^\mathbf {OL} (p)$. Hence $\varGamma \in - (- V^\mathbf {OL} (p))$.

Second, assume that $\varGamma \not \in V^\mathbf {OL} (p)$. By definition $p \not \in \varGamma$. Since $\varGamma$ is $\mathbf {OL}$-closed, $\varGamma \not \vdash _\mathbf {OL} p$. Then $\varGamma \not \vdash _\mathbf {OL} \lnot \lnot p$; otherwise, $\lnot \lnot p \in \varGamma$ and, since by ($\lnot ^2$E) $\varGamma \cup \{ \lnot \lnot p \} \vdash _\mathbf {OL} p$, $\varGamma \vdash _\mathbf {OL} p$, contradicting that $\varGamma \not \vdash _\mathbf {OL} p$. By (A) $\lnot \lnot p \not \in \varGamma$. By Lemma 5 there is a $\varDelta \in W^\mathbf {OL}$ such that $\varGamma \rightarrow ^\mathbf {OL} \varDelta$ and $\lnot p \in \varDelta$. Since $\lnot p \in \varDelta$, by definition for each $\varTheta \in W^\mathbf {OL}$, $\varDelta \rightarrow ^\mathbf {OL} \varTheta$ implies that $p \not \in \varTheta$, i.e. $\varTheta \not \in V^\mathbf {OL} (p)$. Hence $\varDelta \in - V^\mathbf {OL} (p)$. Since $\varGamma \rightarrow ^\mathbf {OL} \varDelta$, $\varGamma \not \in - (- V^\mathbf {OL} (p))$.

The proof of Item 3 is the same as that of Item 2 in Lemma 6.    $\square$

Finally, we prove the completeness theorem.

Theorem 9

(Completeness Theorem of $\mathbf {OL}$). For any $\varGamma \subseteq \mathsf {Form}$ and $\varphi \in \mathsf {Form}$, $\varGamma \,\models _O\, \varphi$ implies that $\varGamma \vdash _\mathbf {OL} \varphi$.

Proof

Assume that $\varGamma \not \vdash _\mathbf {OL} \varphi$. By Lemma 3 there is a $\varDelta \in W^\mathbf {OL}$ such that $\varGamma \subseteq \varDelta$ and $\varphi \not \in \varDelta$. By Lemma 14 $\mathfrak {M}^\mathbf {OL}, \varDelta \,\models \, \varGamma$ and $\mathfrak {M}^\mathbf {OL}, \varDelta \,\not \models \, \varphi$. Since $\mathfrak {M}^\mathbf {OL}$ is an O-model, $\varGamma \,\not \models _O\, \varphi$.    $\square$