A Framework for Intuitionistic Grammar Logics

Abstract

We generalize intuitionistic tense logics to the multi-modal case by placing grammar logics on an intuitionistic footing. We provide axiomatizations for a class of base intuitionistic grammar logics as well as provide axiomatizations for extensions with combinations of seriality axioms and what we call intuitionistic path axioms. We show that each axiomatization is sound and complete with completeness being shown via a typical canonical model construction.

Work supported by the European Research Council (ERC) Consolidator Grant 771779 (DeciGUT).

1 Introduction

Having been introduced in 1988 by Fariñas del Cerro and Penttonen [5], grammar logics form a prominent class of normal, multi-modal logics that extend classical propositional logic with a set of modalities indexed by characters from an alphabet. Such logics obtain their name due to the incorporation of axioms which can be viewed as production rules in a context-free grammar, and which generate sequences of edges (which can be viewed as words) in a relational model. More significantly however, the class of grammar logics includes many well-known logics that have practical value in computer science; e.g. description logics [17], epistemic logics [11], information logics [27], temporal logics [4], and standard modal logics (e.g. $\mathsf {K}$, $\mathsf {S4}$, and $\mathsf {S5}$) [8].

Another logical paradigm that is useful within computer science is that of constructive reasoning (e.g. [18, 22]), that is, reasoning where the claimed existence of an object implies its constructibility [3]. One of the most renowned logics for formalizing constructive reasoning is intuitionistic logic, which employs a version of implication that is stronger than its classical counterpart. Resting on the philosophical work of L.E.J. Brouwer, propositional intuitionistic logic was provided axiomatizations in the early $20^{\mathrm{th}}$ century by Kolmogorov [19], Orlov [21], and Glivenko [15], with a first-order axiomatization given by Heyting [16].

The interest in modal and intuitionistic logics naturally gave rise to combinations of the two, thus giving birth to the paradigm of intuitionistic modal logics. A diverse set of intuitionistic modal logics have been proposed in the literature [1, 2, 9, 13, 14, 24, 25], though the class of logics introduced by Plotkin and Stirling [24] has become (most notably through the work of Simpson [25]) one of the most popular formulations. In the same year that Plotkin and Stirling [24] introduced their intuitionistic modal logics, Ewald introduced intuitionistic tense logic [10], which not only includes modalities that make reference to the future in a relational model ($\Diamond$ and $\Box$), but also includes modalities that make reference to the past ($\blacklozenge$ and $\blacksquare$). As with (multi-)modal and intuitionistic logics, intuitionistic modal logics have proven useful in computer science; e.g. such logics have been used to design verification techniques [12], in reasoning about functional programs [23], and in the definition of programming languages [7].

Due to the practical import of the aforementioned logics, it seems both natural and worthwhile to formulate intuitionistic versions of grammar logics. Hence, the main goal of this paper will be to axiomatize intuitionistic context-free grammar logics with converses, thus generalizing the work of [5, 10, 24]. In the following section (Sect. 2), we axiomatize and provide a semantics for intuitionistic grammar logics. Afterward (in Sect. 3), we prove the soundness and completeness of our logics, with completeness being shown on the basis of a standard canonical model construction (adapting techniques provided in [10]). In the final section (Sect. 4), we briefly conclude and discuss future work.

2 Intuitionistic Grammar Logics

We define our languages for intuitionistic grammar logics relative to an alphabet $\Sigma$ consisting of a non-empty countable set of characters, which will be used to index modalities. Following [8], we stipulate that each alphabet $\Sigma$ can be partitioned into a forward part $\Sigma ^{+}\,{:}{=}\, \{a, b, c, \ldots \}$ and a backward part $\Sigma ^{-}\,{:}{=}\, \{\overline{a}, \overline{b}, \overline{c}, \ldots \}$ such that each part has the same cardinality and the following is satisfied:

$$\begin{aligned} \Sigma \,{:}{=}\, \Sigma ^{+}\cup \Sigma ^{-}\text { where } \Sigma ^{+}\cap \Sigma ^{-}= \emptyset \text { and } a\in \Sigma ^{+}{ \textit{iff} }\,\, \overline{a} \in \Sigma ^{-}\end{aligned}$$

We use $a$, $b$, $c$, $\ldots$ . (possibly annotated) to denote the forward characters contained in the forward part $\Sigma ^{+}$, and $\overline{a}$, $\overline{b}$, $\overline{c}$, $\ldots$ . (possibly annotated) to denote the backward characters contained in the backward part $\Sigma ^{-}$. Both forward and backward characters are referred to as characters more generally, and we use $x$, $y$, $z$, $\ldots$ . (possibly annotated) to denote them. Intuitively, modalities indexed with forward characters make reference to future states within a relational model, and modalities indexed with backward characters make reference to past states. The converse operation $\overline{\cdot }$ is defined to be a function mapping each forward character $a\in \Sigma ^{+}$ to its converse $\overline{a} \in \Sigma ^{-}$ and vice versa; hence, the converse operation is its own inverse, i.e. for any $x\in \Sigma$, $x= \overline{\overline{x}}$.

Each of our languages includes propositional atoms from the denumerable set $\Phi \,{:}{=}\, \{p, q, r, \ldots \}$. Each language $\mathcal {L}(\Sigma )$ is defined via the following grammar in BNF:

$$\begin{aligned} A \,{:}{:}{=}\, p \ | \ \bot \ | \ A \vee A \ | \ A \wedge A \ | \ A \supset A \ | \ \langle x\rangle A \ | \ [x]A \end{aligned}$$

where p ranges over the set of propositional atoms $\Phi$ and $x$ ranges over the alphabet $\Sigma$. We use A, B, C, $\ldots$ . to range over formulae in $\mathcal {L}(\Sigma )$, define ${\sim }A {:}{=} A \supset \bot$, and define $A \supset \subset B \,{:}{=}\, (A \supset B)\wedge (B \supset A)$. We interpret formulae on bi-relational $\Sigma$-models, which are inspired by the models for intuitionistic modal and tense logics presented in [2, 9, 10, 24]:

Definition 1

(Bi-relational $\Sigma$-Model). We define a bi-relational $\Sigma$-model to be a tuple $M = (W, \le , \{R_{x} \ | \ x\in \Sigma \}, V)$ such that:

• W is a non-empty set of worlds $\{w, u, v, \ldots \}$;

• The intuitionistic relation $\le \ \subseteq W \times W$ is a preorder, i.e. it is reflexive and transitive;

• The accessibility relation $R_{x} \subseteq W \times W$ satisfies:

  • (F1) For all $w, v, v' \in W$, if $w R_{x} v$ and $v \le v'$, then there exists a $w' \in W$ such that $w \le w'$ and $w' R_{x} v'$;

  • (F2) For all $w, w', v \in W$, if $w \le w'$ and $w R_{x} v$, then there exists a $v' \in W$ such that $w' R_{x} v'$ and $v \le v'$;

  • (F3) $w R_{x} u$ iff $u R_{\overline{x}} w$;

• $V : W \rightarrow 2^{\Phi }$ is a valuation function satisfying the monotonicity condition: for each $w, u \in W$, if $w \le u$, then $V(w) \subseteq V(u)$.

The (F1) and (F2) conditions ensure the monotonicity of complex formulae (see Lemma 1) in our models, which is a property characteristic of intuitionistic logics.¹ We note that we interpret accessibility relations indexed with forward characters as relating worlds to future worlds, and accessibility relations indexed with backward characters as relating worlds to past worlds. Such an interpretation shows that our models have a tense character, and additionally, shows that our logics generalize the intuitionistic tense logics of [10].

We interpret formulae from $\mathcal {L}(\Sigma )$ over bi-relational models via the following clauses.

Definition 2

(Semantic Clauses). Let M be a bi-relational $\Sigma$-model with $w \in W$. The satisfaction relation $M,w \Vdash ^{\Sigma }A$ between $w \in W$ of M and a formula $A \in \mathcal {L}(\Sigma )$ is inductively defined as follows:

• $M,w \Vdash ^{\Sigma }p$ iff $p \in V(w)$, for $p \in \Phi$;

• $M,w \not \Vdash ^{\Sigma }\bot$;

• $M,w \Vdash ^{\Sigma }A \vee B$ iff $M,w \Vdash ^{\Sigma }A$ or $M,w \Vdash ^{\Sigma }B$;

• $M,w \Vdash ^{\Sigma }A \wedge B$ iff $M,w \Vdash ^{\Sigma }A$ and $M,w \Vdash ^{\Sigma }B$;

• $M,w \Vdash ^{\Sigma }A \supset B$ iff for all $w' \in W$, if $w \le w'$ and $M,w' \Vdash ^{\Sigma }A$, then $M,w' \Vdash ^{\Sigma }B$;

• $M,w \Vdash ^{\Sigma }\langle x\rangle A$ iff there exists a $v \in W$ such that $w R_{x} v$ and $M,v \Vdash ^{\Sigma }A$;

• $M,w \Vdash ^{\Sigma }[x]A$ iff for all $w', v' \in W$, if $w \le w'$ and $w' R_{x} v'$, then $M,v' \Vdash ^{\Sigma }A$.

Lemma 1

Let M be a bi-relational $\Sigma$-model with $w,u \in W$ of M. If $w \le u$ and $M, w \Vdash ^{\Sigma }A$, then $M, u \Vdash ^{\Sigma }A$.

Proof

By induction on the complexity of A. $\square$

As will be shown in the subsequent section, given an alphabet $\Sigma$, the set of formulae valid with respect to the class of bi-relational $\Sigma$-models is axiomatizable. We refer to the axiomatization as $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma )$ (with $\mathsf {H}$ denoting the fact that the axiomatization is a Hilbert calculus), and call the corresponding logic that it generates $\mathsf {IK}_{\mathsf {m}}(\Sigma )$. We note that $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ is taken to be the base intuitionistic grammar logic relative to $\Sigma$; below, we will also consider extensions of $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ by extending its axiomatization with common modal axioms.

Definition 3

(Axiomatization). We define our axiomatization $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma )$ below, where we have an axiom and inference rule for each $x\in \Sigma$.

We define the logic $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ to be the smallest set of formulae from $\mathcal {L}(\Sigma )$ closed under substitutions of the axioms and applications of the inference rules. A formula A is defined to be a theorem of $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ iff $A \in \mathsf {IK}_{\mathsf {m}}(\Sigma )$.

We also consider logics that are extensions of $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ with sets $\mathcal {A}$ of the following axioms.

$$\begin{aligned} \mathrm {D}_{x}: [x]A \supset \langle x\rangle A \quad \mathrm {IPA}: (\langle x_{1} \rangle \cdots \langle x_{n} \rangle A \supset \langle x \rangle A) \wedge ([ x ] A \supset [ x_{1} ] \cdots [ x_{n} ] A) \end{aligned}$$

We refer to axioms of the form shown above left as seriality axioms, and axioms of the form shown above right as intuitionistic path axioms ($\mathrm {IPA}$s). We use $\mathcal {A}$ to denote any arbitrary collection of axioms of the above forms. Moreover, we note that the collection of $\mathrm {IPA}$s includes multi-modal variants of standard axioms such as $\mathrm {T}_{x}$, $\mathrm {B}_{x}$, $\mathrm {4}_{x}$, and $\mathrm {5}_{x}$, which are shown below.

$$\begin{aligned} \mathrm {T}_{x}: (A \supset \langle x\rangle A) \wedge ([x]A \supset A) \quad \mathrm {4}_{x}: (\langle x\rangle \langle x\rangle A \supset \langle x\rangle A) \wedge ([x]A \supset [x][x]A) \end{aligned}$$

$$\begin{aligned} \mathrm {B}_{x}: (\langle \overline{x} \rangle A \supset \langle x\rangle A) \wedge ([x]A \supset [\overline{x}]A) \quad \mathrm {5}_{x}: (\langle \overline{x} \rangle \langle x\rangle A \supset \langle x\rangle A) \wedge ([x]A \supset [\overline{x}][x]A) \end{aligned}$$

In the next section, we show that any extension of $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma )$ with a set $\mathcal {A}$ of axioms is sound and complete relative to a specified sub-class of the bi-relational $\Sigma$-models. For each axiom we extend $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma )$ with, we impose a frame condition on our class of bi-relational $\Sigma$-models. Axioms and related frame conditions are displayed in Fig. 1, and extensions of $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma )$ with seriality and $\mathrm {IPA}$ axioms, along with their corresponding models, are defined below.

Fig. 1.

Axioms and their related frame conditions. We note that when $n=0$, the related frame condition is taken to be $w R_{x} w$.

Definition 4

(Terminology for Extensions). We define the axiomatization $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$ to be $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma ) \cup \mathcal {A}$, and define the logic $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$ to be the smallest set of formulae from $\mathcal {L}(\Sigma )$ closed under substitutions of the axioms and applications of the inference rules. A formula A is defined to be an $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-theorem, written $\vdash _{\mathcal {A}}^{\Sigma }A$, iff $A \in \mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$, and a formula A is said to be derivable from a set of formulae $\mathscr {A}\subseteq \mathcal {L}(\Sigma )$, written $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$, iff for some $B_{1}, \ldots , B_{n} \in \mathscr {A}$, $\vdash _{\mathcal {A}}^{\Sigma }B_{1} \wedge \cdots \wedge B_{n} \supset A$.

Moreover, we define a bi-relational $(\Sigma ,\mathcal {A})$-model to be a bi-relational $\Sigma$-model satisfying each frame condition related to an axiom $A \in \mathcal {A}$. A formula A is defined to be globally true on a bi-relational $(\Sigma ,\mathcal {A})$-model M, written $M \Vdash _{\mathcal {A}}^{\Sigma }A$, iff $M,u \Vdash ^{\Sigma }A$ for all worlds $u \in W$ of M. A formula A is defined to be $(\Sigma ,\mathcal {A})$-valid, written $\Vdash _{\mathcal {A}}^{\Sigma }A$, iff A is globally true on every bi-relational $(\Sigma ,\mathcal {A})$-model. Last, we say that a set $\mathscr {A}$ of formulae semantically implies a formula A, written $\mathscr {A}\Vdash _{\mathcal {A}}^{\Sigma }A$, iff for all bi-relational $(\Sigma ,\mathcal {A})$-models M and each $w \in W$ of M, if $M, w \Vdash ^{\Sigma }B$ for each $B \in \mathscr {A}$, then $M,w \Vdash ^{\Sigma }A$.

Remark 1

Note that the axiomatization $\mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma ) = \mathsf {H}\mathsf {IK}_{\mathsf {m}}(\Sigma ,\emptyset )$ and that a bi-relational $(\Sigma ,\emptyset )$-model is a bi-relational $\Sigma$-model.

Let us now move on to the next section and prove the soundness and completeness results for our logics.

3 Soundness and Completeness

In this section, we show that the $\vdash _{\mathcal {A}}^{\Sigma }$ and $\Vdash _{\mathcal {A}}^{\Sigma }$ relations coincide, that is to say, we show that each intuitionistic grammar logic $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$ is sound and complete. As usual, soundness is straightforward to prove:

Theorem 1

(Soundness). If $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$, then $\mathscr {A}\Vdash _{\mathcal {A}}^{\Sigma }A$.

Proof

One can prove that if $\vdash _{\mathcal {A}}^{\Sigma }A$, then $\Vdash _{\mathcal {A}}^{\Sigma }A$ by showing that each axiom is valid and each inference rule preserves validity. Then, if we assume that $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$, it follows that for some $B_{1}, \ldots , B_{n} \in \mathscr {A}$, $\vdash _{\mathcal {A}}^{\Sigma }B_{1} \wedge \cdots \wedge B_{n} \supset A$, which further implies that $\Vdash _{\mathcal {A}}^{\Sigma }B_{1} \wedge \cdots \wedge B_{n} \supset A$. The last fact permits us to conclude that $\mathscr {A}\Vdash _{\mathcal {A}}^{\Sigma }A$. $\square$

To establish completeness we combine techniques used for establishing the completeness of intuitionistic logic [6] and intuitionisitc tense logic [10]. Our strategy is rather standard and consists of constructing a canonical model where worlds are pairs of the form $(\mathscr {A}^{\omega },\mathscr {B}^{\omega })$ with $\mathscr {A}^{\omega }$ and $\mathscr {B}^{\omega }$ sets of formulae. If one assumes that $\mathscr {A}\not \vdash _{\mathcal {A}}^{\Sigma }A$, then one can show that a pair exists in the canonical model satisfying $\mathscr {A}$, but not A, thus establishing completeness (see Theorem 2 below). We begin by defining two useful notions, viz. the notion of an $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent set and the notion of an $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-saturated pair.

Definition 5

($\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-Consistent). We define a pair of sets of formulae $(\mathscr {A},\mathscr {B})$ to be $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent iff for no finite subsets $\mathscr {A}_{0} \subseteq \mathscr {A}$ and $\mathscr {B}_{0} \subseteq \mathscr {B}$ we have $\vdash _{\mathcal {A}}^{\Sigma }\bigwedge \mathscr {A}_{0} \supset \bigvee \mathscr {B}_{0}$.

Definition 6

($\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-Saturated). We define a pair $(\mathscr {A},\mathscr {B})$ to be $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-saturated iff

• 1. $(\mathscr {A},\mathscr {B})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent;

• 2. if $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$, then $A \in \mathscr {A}$;

• 3. if $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A \vee B$, then $A \in \mathscr {A}$ or $B \in \mathscr {A}$;

• 4. $\mathscr {A}\cap \mathscr {B}= \emptyset$;

• 5. $\mathscr {A}\cup \mathscr {B}= \mathcal {L}(\Sigma )$.

Lemma 2

Suppose that $(\mathscr {A},\mathscr {B})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent. Then, there exists a saturated pair $(\mathscr {A}^{\omega },\mathscr {B}^{\omega })$ such that $\mathscr {A}\subseteq \mathscr {A}^{\omega }$ and $\mathscr {B}\subseteq \mathscr {B}^{\omega }$.

Proof

Let us enumerate all disjunctions from $\mathcal {L}(\Sigma )$ where each disjunction occurs infinitely often: $\langle B_{0,i} \vee B_{1,i} \rangle _{i \in \mathbb {N}}$. We set $(\mathscr {A}_{0},\mathscr {B}_{0}) {:}{=} (\mathscr {A},\mathscr {B})$ and define an infinite sequence of pairs as follows: $\mathscr {A}_{n+1} {:}{=} \mathscr {A}_{n} \cup \{B_{j,n}\}$ and $\mathscr {B}_{n+1} {:}{=} \mathscr {B}_{n}$, if $(\mathscr {A}_{n} \cup \{B_{j,n}\},\mathscr {B}_{n})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent (and if $(\mathscr {A}_{n} \cup \{B_{j,n}\},\mathscr {B}_{n})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent for both $j = 0$ and $j = 1$, then we set $\mathscr {A}_{n+1} {:}{=} \mathscr {A}_{n} \cup \{B_{0,n}\}$), and $\mathscr {A}_{n+1} {:}{=} \mathscr {A}_{n}$ and $\mathscr {B}_{n+1} {:}{=} \mathscr {B}_{n} \cup \{B_{0,i},B_{1,i}\}$ otherwise.

Let $\mathscr {A}^{\omega } {:}{=} \bigcup _{i \in \mathbb {N}} \mathscr {A}_{i}$ and $\mathscr {B}^{\omega } {:}{=} \bigcup _{i \in \mathbb {N}} \mathscr {B}_{i}$. We now argue that $(\mathscr {A}^{\omega },\mathscr {B}^{\omega })$ is saturated. It is straightforward to show that for each n, $(\mathscr {A}_{n},\mathscr {B}_{n})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent and that $\mathscr {A}_{n} \cap \mathscr {B}_{n} = \emptyset$ from which the saturation properties 1 and 4 can be deduced (see Definition 6 above). We note that saturation properties 3 and 5 follow from the above construction procedure, and 2 follows from 3 since if $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$, then $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A \vee A$ (cf. [6, Lemma 5.3.8]). $\square$

Definition 7

(Canonical Model). We define the canonical model $M^{C}(\Sigma ,\mathcal {A}) {:}{=}\, (W^{C}, \le ^{C}, \{R_{x}^{C}\ | \ x\in \Sigma \}, V^{C})$ as shown below, and let $w, u \in W^{C}$ with $w\, {:}{=}\, (\mathscr {A},\mathscr {B})$ and $u \,{:}{=}\, (\mathscr {A}',\mathscr {B}')$.

• $W^{C}{:}{=} \{(\mathscr {C},\mathscr {D}) \ | \ (\mathscr {C},\mathscr {D}) \text { is saturated.}\}$;

• $w \le ^{C}u$ iff $\mathscr {A}\subseteq \mathscr {A}'$;

• $w R_{x}^{C}u$ iff (i) for all $A \in \mathcal {L}(\Sigma )$, if $[x]A \in \mathscr {A}$, then $A \in \mathscr {A}'$, and (ii) for all $A \in \mathcal {L}(\Sigma )$, if $A \in \mathscr {A}'$, then $\langle x\rangle A \in \mathscr {A}$;

• $w \in V^{C}(p)$ iff $p \in \mathscr {A}$.

The following two lemmas are proven in an almost identical fashion to Lemma 3 and 5 of [10].

Lemma 3

Let $w {:}{=} (\mathscr {A}_{0},\mathscr {B}_{0}) \in W^{C}$. Then, $\langle x\rangle A \in \mathscr {A}_{0}$ iff there exists a $u {:}{=} (\mathscr {A}_{1},\mathscr {B}_{1}) \in W^{C}$ such that $w R_{x}^{C}u$ and $A \in \mathscr {A}_{1}$.

Lemma 4

Let $w {:}{=} (\mathscr {A}_{0},\mathscr {B}_{0}) \in W^{C}$. Then, $[x]A \in \mathscr {A}_{0}$ iff for each $u {:}{=} (\mathscr {A}_{1},\mathscr {B}_{1})$ and $v {:}{=} (\mathscr {A}_{2},\mathscr {B}_{2})$ in $W^{C}$, if $w \le ^{C}u$ and $u R_{x}^{C}v$, then $A \in \mathscr {A}_{2}$.

Lemma 5

The canonical model $M^{C}(\Sigma ,\mathcal {A})$ is a bi-relational $(\Sigma ,\mathcal {A})$-model.

Proof

It is straightforward to show that $M^{C}$ is a bi-relational $(\Sigma ,\mathcal {A})$-model. The proof that $M^{C}$ satisfies properties (F1)–(F3) uses axioms A8, A9, and A7, respectively (cf. [10]), and the fact that the valuation function $V^{C}$ is monotonic follows from its definition and the definition of $\le ^{C}$. Below, we show that $M^{C}$ satisfies each frame property associated with an axiom from $\mathcal {A}$.

$\mathrm {D}_{x}$:

We show that if the seriality axiom $[x]A \supset \langle x\rangle A$ is included in our axiomatization, then $R_{x}$ is serial. Let $w {:}{=} (\mathscr {A},\mathscr {B}) \in W^{C}$ and observe that the formula $[x](p \supset p) \in \mathscr {A}$ since if it were in $\mathscr {B}$, w would not be $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent (and hence, not saturated). Therefore, by applying the seriality axiom $\mathrm {D}_{x}$, we may conclude that $\langle x\rangle (p \supset p) \in \mathscr {A}$, from which it follows that there exists a $u {:}{=} (\mathscr {C},\mathscr {D}) \in W^{C}$ such that $w R_{x}^{C}u$ by Lemma 3.

$\mathrm {IPA}$:

We show that if $(\langle x_{1} \rangle \cdots \langle x_{n} \rangle A \supset \langle x \rangle A) \wedge ([ x ] A \supset [ x_{1} ] \cdots [ x_{n} ] A)$ is included in our axiomatization, then for any $w_{0}, \ldots , w_{n} \in W^{C}$, if $w_{i} R_{x_{i+1}}^{C} w_{i+1}$ for each $i \in \{0, \ldots , n-1\}$, then $w_{0} R_{x}^{C} w_{n}$. Let $w_{0}, \ldots , w_{n}$ be arbitrary worlds in $W^{C}$ and suppose that $w_{i} R_{x_{i+1}}^{C} w_{i+1}$ for each $i \in \{0, \ldots , n-1\}$. We aim to show that $w_{0} R_{x}^{C} w_{n}$, where $w_{0} {:}{=} (\mathscr {A}_{0},\mathscr {B}_{0})$ and $w_{n} {:}{=} (\mathscr {A}_{n}, \mathscr {B}_{n})$. First, assume that $[x]A \in \mathscr {A}_{0}$. Then, by the above axiom, $[ x_{1} ] \cdots [ x_{n} ] A \in \mathscr {A}_{0}$, and by our assumption and the definition of the $R_{x}^{C}$ relation, $A \in \mathscr {A}_{n}$. Second, assume that $A \in \mathscr {A}_{n}$. Then, by our assumption and the definition of the $R_{x}^{C}$ relation, $\langle x_{1} \rangle \cdots \langle x_{n} \rangle A \in \mathscr {A}_{0}$, so by the above axiom, $\langle x\rangle A \in \mathscr {A}_{0}$. Therefore, $w_{0} R_{x}^{C} w_{n}$. $\square$

Lemma 6

(Truth Lemma). Let $w {:}{=} (\mathscr {A},\mathscr {B})$ be saturated. Then, we have $M^{C}(\Sigma ,\mathcal {A}), w \Vdash ^{\Sigma }A$ iff $A \in \mathscr {A}$.

Proof

We prove the result by induction on the complexity of A and argue the $\vee$, $\supset$, $\langle x\rangle$, and $[x]$ cases since the other cases are simple.

$B \vee C$. $M^{C}(\Sigma ,\mathcal {A}), w \Vdash ^{\Sigma }B \vee C$ iff $M^{C}(\Sigma ,\mathcal {A}), w \Vdash ^{\Sigma }B$ or $M^{C}(\Sigma ,\mathcal {A}), w \Vdash ^{\Sigma }C$ iff $B \in \mathscr {A}$ or $C \in \mathscr {A}$ iff $B \vee C \in \mathscr {A}$. We note that the second ‘iff’ follows from IH an the third follows from the fact that w is saturated (see Definition 6).

$B \supset C$. The right-to-left direction is straightforward, so we show the left-to-right direction by contraposition. Suppose that $B \supset C \not \in \mathscr {A}$. It follows that $\mathscr {A}\cup \{B\} \not \vdash _{\mathcal {A}}^{\Sigma }C$, implying that the pair $(\mathscr {A}\cup \{B\}; \{C\})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent, and so, we may extend it to a saturated pair $u {:}{=} (\mathscr {C},\mathscr {D})$. Observe that $\mathscr {A}\subseteq \mathscr {C}$, $B \in \mathscr {C}$, and $C \not \in \mathscr {C}$. By the definition of $\le ^{C}$ and IH, it follows that $u \in W^{C}$ with $w \le ^{C}u$, $M^{C}(\Sigma ,\mathcal {A}), u \Vdash ^{\Sigma }B$, and $M^{C}(\Sigma ,\mathcal {A}), u \not \Vdash ^{\Sigma }C$, entailing that $M^{C}(\Sigma ,\mathcal {A}), w \not \Vdash ^{\Sigma }B \supset C$.

$\langle x\rangle B$. The left-to-right direction is straightforward, so we show the right-to-left direction. Suppose that $\langle x\rangle B \in \mathscr {A}$. Then, by Lemma 3 we know that there exists a $u \,{:}{=}\, (\mathscr {C},\mathscr {D}) \in W^{C}$ such that $w R_{x}^{C}u$ and $B \in \mathscr {C}$. Therefore, $M^{C}(\Sigma ,\mathcal {A}), u \Vdash ^{\Sigma }B$ by IH, implying that $M^{C}(\Sigma ,\mathcal {A}), w \Vdash ^{\Sigma }\langle x\rangle B$.

$[x]B$. Follows from Lemma 4 and IH. $\square$

Theorem 2

(Completeness). If $\mathscr {A}\Vdash _{\mathcal {A}}^{\Sigma }A$, then $\mathscr {A}\vdash _{\mathcal {A}}^{\Sigma }A$.

Proof

Suppose $\mathscr {A}\not \vdash _{\mathcal {A}}^{\Sigma }A$. Then, $(\mathscr {A},\{A\})$ is $\mathsf {IK}_{\mathsf {m}}(\Sigma ,\mathcal {A})$-consistent and can be extended to a saturated pair $w {:}{=} (\mathscr {A}^{\omega },\mathscr {B}^{\omega })$. By Lemma 6, $M^{C}, w \Vdash ^{\Sigma }B$ for each $B \in \mathscr {A}^{\omega }$, but $M^{C}, w \not \Vdash ^{\Sigma }C$ for each $C \in \mathscr {B}^{\omega }$. Hence, $\mathscr {A}\not \Vdash _{\mathcal {A}}^{\Sigma }A$. $\square$

4 Conclusion

This paper provided sound and complete axiomatizations for intuitionistic grammar logics. We defined a base intuitionistic grammar logic $\mathsf {IK}_{\mathsf {m}}(\Sigma )$, for each alphabet $\Sigma$, and provided axiomatizations for extensions of $\mathsf {IK}_{\mathsf {m}}(\Sigma )$ with combinations of seriality axioms and intuitionistic path axioms. In future work, we aim to provide nested sequent systems in the style of [26] for the logics discussed here by making use of the structural refinement methodology of [20]. The goal will be to identify decidable fragments of intuitionistic grammar logics via proof-search. Moreover, due to the connection between modal logics and description logics, it could be worthwhile to investigate the use of intuitionistic grammar logics (or close variants thereof) in knowledge representation.