{'fraction_non_alphanumeric': 0.05897781243354363, 'fraction_numerical': 0.010065924718224996, 'mean_word_length': 3.883350640359986, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 14, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
A Framework for Intuitionistic Grammar Logics

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.


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. K, S4, and 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 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,14,24,13,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 (♦ and ), but also includes modalities that make reference to the past ( and ). 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.

Intuitionistic Grammar Logics
We define our languages for intuitionistic grammar logics relative to an alphabet Σ consisting of a non-empty countable set of characters, which will be used to index modalities. Following [8], we stipulate that each alphabet Σ can be partitioned into a forward part Σ + := {a, b, c, . . .} and a backward part Σ − := {a, b, c, . . .} such that each part has the same cardinality and the following is satisfied: We use a, b, c, . . . (possibly annotated) to denote the forward characters contained in the forward part Σ + , and a, b, c, . . . (possibly annotated) to denote the backward characters contained in the backward part Σ − . Both forward and backward characters are referred to as characters more generally, and we use x, y, z, . . . (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 · is defined to be a function mapping each forward character a ∈ Σ + to its converse a ∈ Σ − and vice versa; hence, the converse operation is its own inverse, i.e. for any x ∈ Σ, x = x.
Each of our languages includes propositional atoms from the denumerable set Φ := {p, q, r, . . .}. Each language L(Σ) is defined via the following grammar in BNF: where p ranges over the set of propositional atoms Φ and x ranges over the alphabet Σ. We use A, B, C, . . . to range over formulae in L(Σ), define ∼A : We interpret formulae on bi-relational Σ-models, which are inspired by the models for intuitionistic modal and tense logics presented in [2,9,10,24]: The (F1) and (F2) conditions ensure the monotonicity of complex formulae (see Lem. 1) in our models, which is a property characteristic of intuitionistic logics. 1 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 L(Σ) over bi-relational models via the following clauses.
Definition 2 (Semantic Clauses). Let M be a bi-relational Σ-model with w ∈ W . The satisfaction relation M, w Σ A between w ∈ W of M and a formula A ∈ L(Σ) is inductively defined as follows: Proof. By induction on the complexity of A.
⊓ ⊔ As will be shown in the subsequent section, given an alphabet Σ, the set of formulae valid with respect to the class of bi-relational Σ-models is axiomatizable. We refer to the axiomatization as HIK m (Σ) (with H denoting the fact that the axiomatization is a Hilbert calculus), and call the corresponding logic that it generates IK m (Σ). We note that IK m (Σ) is taken to be the base intuitionistic grammar logic relative to Σ; below, we will also consider extensions of IK m (Σ) by extending its axiomatization with common modal axioms.
Definition 3 (Axiomatization). We define our axiomatization HIK m (Σ) below, where we have an axiom and inference rule for each x ∈ Σ.

A0 Any axiomatization for intuitionis
We define the logic IK m (Σ) to be the smallest set of formulae from L(Σ) closed under substitutions of the axioms and applications of the inference rules. A formula A is defined to be a theorem of IK m (Σ) iff A ∈ IK m (Σ).
We also consider logics that are extensions of IK m (Σ) with sets A of the following axioms.
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 (IPAs). We use A to denote any arbitrary collection of axioms of the above forms. Moreover, we note that the collection of IPAs includes multi-modal variants of standard axioms such as T x , B x , 4 x , and 5 x , which are shown below.
In the next section, we show that any extension of HIK m (Σ) with a set A of axioms is sound and complete relative to a specified sub-class of the bi-relational Σ-models. For each axiom we extend HIK m (Σ) with, we impose a frame condition on our class of bi-relational Σ-models. Axioms and related frame conditions are displayed in Fig. 1, and extensions of HIK m (Σ) with seriality and IPA axioms, along with their corresponding models, are defined below.

Definition 4 (Terminology for Extensions).
We define the axiomatization HIK m (Σ, A) to be HIK m (Σ) ∪ A, and define the logic IK m (Σ, A) to be the smallest set of formulae from L(Σ) closed under substitutions of the axioms and applications of the inference rules. A formula A is defined to be an IK m (Σ, A)-theorem, Moreover, we define a bi-relational (Σ, A)-model to be a bi-relational Σ-model satisfying each frame condition related to an axiom A ∈ A. A formula A is defined to be globally true on a bi-relational  Let us now move on to the next section and prove the soundness and completeness results for our logics.

Soundness and Completeness
In this section, we show that the ⊢ Σ A and Σ A relations coincide, that is to say, we show that each intuitionistic grammar logic IK m (Σ, A) is sound and complete. As usual, soundness is straightforward to prove: Proof. One can prove that if ⊢ Σ A A, then Σ A A by showing that each axiom is valid and each inference rule preserves validity. Then, if we assume that A ⊢ Σ A A, it follows that for some B 1 , . . . , B n ∈ A , ⊢ Σ A B 1 ∧ · · · ∧ B n ⊃ A, which further implies that Σ A B 1 ∧ · · · ∧ B n ⊃ A. The last fact permits us to conclude that 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 (A ω , B ω ) with A ω and B ω sets of formulae. If one assumes that A ⊢ Σ A A, then one can show that a pair exists in the canonical model satisfying A , but not A, thus establishing completeness (see Thm. 2 below). We begin by defining two useful notions, viz. the notion of an IK m (Σ, A)consistent set and the notion of an IK m (Σ, A)-saturated pair.
Definition 5 (IK m (Σ, A)-Consistent). We define a pair of sets of formulae Definition 6 (IK m (Σ, A)-Saturated). We define a pair (A , B) to be IK m (Σ, A)saturated iff Let A ω := i∈N A i and B ω := i∈N B i . We now argue that (A ω , B ω ) is saturated. It is straightforward to show that for each n, (A n , B n ) is IK m (Σ, A)consistent and that A n ∩ B n = ∅ from which the saturation properties 1 and 4 can be deduced (see Def. 6 above). We note that saturation properties 3 and 5 follow from the above construction procedure, and 2 follows from 3 since if The following two lemmas are proven in an almost identical fashion to Lem. 3 and 5 of [10].
Proof. It is straightforward to show that M C is a bi-relational (Σ, 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 ≤ C . Below, we show that M C satisfies each frame property associated with an axiom from A.

D x We show that if the seriality axiom [x]
A ⊃ x A is included in our axiomatization, then R x is serial. Let w := (A , B) ∈ W C and observe that the formula [x](p ⊃ p) ∈ A since if it were in B, w would not be IK m (Σ, A)consistent (and hence, not saturated). Therefore, by applying the seriality axiom D x , we may conclude that x (p ⊃ p) ∈ A , from which it follows that there exists a u : in our axiomatization, then for any w 0 , . . . , w n ∈ W C , if w i R C xi+1 w i+1 for each i ∈ {0, . . . , n − 1}, then w 0 R C x w n . Let w 0 , . . . , w n be arbitrary worlds in W C and suppose that w i R C xi+1 w i+1 for each i ∈ {0, . . . , n − 1}. We aim to show that w 0 R C x w n , where w 0 := (A 0 , B 0 ) and w n := (A n , B n ). First, assume that [x]A ∈ A 0 . Then, by the above axiom, [x 1 ] · · · [x n ]A ∈ A 0 , and by our assumption and the definition of the R C x relation, A ∈ A n . Second, assume that A ∈ A n . Then, by our assumption and the definition of the R C x relation, x 1 · · · x n A ∈ A 0 , so by the above axiom, x A ∈ A 0 . Therefore, w 0 R C x w n . ⊓ ⊔ Lemma 6 (Truth Lemma). Let w := (A , B) be saturated. Then, we have Proof. We prove the result by induction on the complexity of A and argue the ∨, ⊃, x , and [x] cases since the other cases are simple.
We note that the second 'iff ' follows from IH an the third follows from the fact that w is saturated (see Def. 6).
B ⊃ C. The right-to-left direction is straightforward, so we show the leftto-right direction by contraposition. Suppose that B ⊃ C ∈ A . It follows that A ∪ {B} ⊢ Σ A C, implying that the pair (A ∪ {B}; {C}) is IK m (Σ, A)-consistent, and so, we may extend it to a saturated pair u := (C , D). Observe that A ⊆ C , B ∈ C , and C ∈ C . By the definition of ≤ C and IH, it follows that u ∈ W C with w ≤ C u, M C (Σ, A), u Σ B, and M C (Σ, A), u Σ C, entailing that M C (Σ, A), w Σ B ⊃ C.
x B. The left-to-right direction is straightforward, so we show the rightto-left direction. Suppose that x B ∈ A . Then, by Lem. 3 we know that there exists a u := (C , D) ∈ W C such that wR C x u and B ∈ C . Therefore, M C (Σ, A), u Σ B by IH, implying that M C (Σ, A), w Σ x B.
[x]B. Follows from Lem. 4 and IH. ⊓ ⊔ is IK m (Σ, A)-consistent and can be extended to a saturated pair w := (A ω , B ω ). By Lem. 6, M C , w Σ B for each B ∈ A ω , but M C , w Σ C for each C ∈ B ω . Hence, A Σ A A. ⊓ ⊔

Conclusion
This paper provided sound and complete axiomatizations for intuitionistic grammar logics. We defined a base intuitionistic grammar logic IK m (Σ), for each alphabet Σ, and provided axiomatizations for extensions of IK m (Σ) 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.