{'fraction_non_alphanumeric': 0.05612783460124486, 'fraction_numerical': 0.008881447239107488, 'mean_word_length': 3.6542436049466374, 'pattern_counts': {'":': 0, '<': 2, '<?xml version=': 0, '>': 6, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 18, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Modal Logic LEC for Changing Knowledge, Expressed in the Growing Language

We present the propositional logic LEC for the two epistemic modalities of current and stable knowledge used by an agent who systematically enriches his language. A change in the linguistic resources of an agent as a result of certain cognitive processes is something that commonly happens. Our system is based on the logic LC intended to formalize the idea that the occurrence of changes induces the passage of time. Here, the primitive operator C read as: it changes that, defines the temporal succession of states of the world. The notion of current knowledge concerns variable components of the world and it may change over time. We represent it by the primitive operator k read as: the agent currently knows that, and assume that it has S5 properties. The second type of knowledge, symbolized by the primitive operator K read as: the agent stably knows that, relates to constant components of the world and it does not change. As a result of the axiomatic entanglement of C, K and k we show that stable knowledge satisfies axioms of S4.3. K and k modalities are not mutually definable, stable knowledge implies the current one and if the latter never changes, then it comes to be stable. The combination of K and k with the idea of an expanding language allows questioning of the so-called perfect recall principle. It cannot be maintained for both types of knowledge just because of changes in the vocabulary of the agent and possibly the growing spectrum of possible states of the world. We interpret LEC in the semantics of histories of epistemic changes and show that it is complete. Finally, we compare our logic with selected epistemic logics based on the concept of linear discrete time.


Introduction
Contemporary formal epistemic research are often inspired by Hintikka's considerations on knowledge and beliefs presented in [4]. In particular, they also examine the issue of the changeability of knowledge over time [cf. 2, 3]. Our work aims to describe changes of knowledge in a new context which is the agent's use of a changing language. A change in the linguistic resources of an agent as a result of certain cognitive processes is something that commonly happens. In our approach, the language used by an agent grows by adding new expressions that were not in his earlier vocabulary.
The spectrum of logics that are usually used to describe the notion of knowledge is in between S4 and S5. In temporal multi-agent epistemic logics various kinds of changing knowledge are studied, often described by properties of the modal logic S5 [see 2, pp. 59, 105]. We propose a formalism that may be considered as a logic of one agent who uses two modal concepts of knowledge parametrized by time. Our new system LEC is an epistemic axiomatic extension of the propositional modal logic LC formulated by Świętorzecka [11], later elaborated together with Czermak [12,13]. LC is intended as a formal description of the idea that change is primary in relation to time (the occurrence of changes is to induce the passage of time) and it uses the primitive modal operator C read as: it changes that, which defines the temporal succession of states of the world. The first concept of knowledge that we are interested in here concerns variable components of the world and it may change over time. We call it current knowledge and assume that this modality has S5 properties. The second type of knowledge relates to constant components of the world, and when it is acquired, it is not subject to change. For this knowledge we use Stalnaker's adjective 'stable' [10]. The proposed way of understanding this concept respects some well-known discussions about the adequate formal representation of knowledge, started already by Hintikka who questioned the principle of negative retrospection [4, p. 56]. 1 In the case of stable knowledge, we follow his objection to the principle of negative retrospection expressed by the specific axiom of S5. The stability of our knowledge does not mean that it cannot be expanded. In other words, our lack of stable knowledge may change. If we had negative introspection, then we could not also change the lack of stable knowledge, because stable knowledge does not change. As we will see, in our system it can be proved that stable knowledge has S4.3 properties. The system S4.3 taken as a formal basis for the concept of knowledge was first suggested by Hoek in [5] and then considered by Stalnaker. The latter considered knowledge as a justified true belief that is stable under any potential revision by a piece of information that is, in fact, true [10, p. 187] and he explicitly indicated S4.3 properties in formalization of this concept [10, p. 190]. We follow these interpretative intuitions here. 2 From the philosophical perspective, stable knowledge may be considered as a counterpart of the classical concept episteme, at least in this sense that it cannot change over time. What is different from Platonic associations, is that in our logic the concept of stable knowledge is axiomatically fully entangled with concepts of change and current knowledge. That means that in the axioms and rules of LEC, we do not impose on it any properties that are isolated from other modal concepts. The characteristic properties of stable knowledge itself are consequences of accepted axioms. Such an inferential relationship is a novelty in relation to the results presented in the available literature devoted to the formal modeling of the concept of knowledge.
Formal properties of both types of knowledge are also dependent on the new component introduced in the proposed consideration which is the fact that the agent uses an expanding language. The description of the phenomenon of a growing language was used to expresses logic LC in its original formulation [11] and it was also considered in [12,13]. We continue and extend this study. We express LC in a language that can be expanded by any number of new propositional expressions and we add two primitive epistemic operators: k ("the agent currently knows that") and K ("the agent stably knows that"). Current knowledge may change in time. Stable knowledge does not change and implies current knowledge. If the latter never changes, then it becomes stable.
It turns out that the combination of the two aforementioned concepts of knowledge with the idea of an expanding language allows us to re-discuss the so-called perfect recall principle [see 2, pp. 136-138] often accepted in epistemic temporal systems and game theory [14]. This principle is intended to express the limitation of the cognitive spectrum of an agent who has gained new information. According to this idea, the agent with an increase of knowledge can, at most, 'narrow' the spectrum of his possible states of the world. We could say that he cannot consider new states that could provide new knowledge  once that earlier he could not even take into account. Here we want only to indicate our first intuitions regarding this issue when considered in the framework of expanding language. Let us assume that the agent uses in his current propositional language only two propositions α 1 and α 2 which are mutually independent on the ground of classical logic. We assume that he knows that α 1 is true, but he does not have any knowledge regarding either α 2 or its negation. This means that he can consider two possible states of the world that are candidates for the current real state, which are described by the following conjunctions: α 1 ∧ α 2 , and α 1 ∧ ¬α 2 . If the agent enriches his language by a new atom α 3 , he is still undecided about the value of α 2 , but if his knowledge of α 1 is stable, then he can now consider four possible descriptions of the actual state. They are described by the following conjunctions: If his knowledge of α 1 changed, because it was only the current knowledge, and he is still undecided about the value of α 2 , then the number of possible descriptions will double. It is easy to see now that the perfect recall principle cannot be maintained for both types of knowledge.
Anticipating our considerations, let us say at the outset that the idea of a growing language is essentially different from the concept of awareness elaborated in the framework of the awareness logic introduced in [1]. The first one was already used in formalization of the doxastic logic LCB and was compared with the awareness approach in [8]. This comparison can be repeated here. In brief, we can say that the awareness logic uses an appropriate awareness operator which is applied to these formulas of a given language that the agent is aware of. In the context of this language, it makes sense to speak about formulas which are not in the scope of the awareness operator. In our approach, the agent's language resource, which he does not yet use, can be considered only on the semantic level. The formulas which he is not 'aware of', do not belong to his language and as such, they have even no logical value. We will pay attention to this matter again when interpreting our formalism.
We start our presentation with the description of the idea of a growing language and its epistemic semantics (Section 1). Then we give axiomatization for the intended semantic structures, and we prove the axioms of S4.3 for stable knowledge (Section 2). In Section 3 we give proofs of soundness and completeness theorems for our new logic LEC. Finally, in Section 4, we discuss the relation of our approach to the epistemic temporal logics based on the concept of linear discrete time.

A growing language and its semantics
The concept of a growing language denotes a family of propositional languages. Upper indexes of atomic formulas code the information to which languages they belong. We will inductively define atomic expressions of subsequent languages. For any n > 0 let I n be either the set of all natural numbers or its initial segment. Then we put At 1 = {α 1 i : i ∈ I 1 } and At n+1 = At n ∪ {α n+1 i : i ∈ I n+1 }. Note that in At n+1 , there is at least one new atomic formula that is not a member of At n .
For the operators C, k and K, for any n > 0 every current language is some n-language which formulas are defined as follows: where α ∈ At n . The symbols ∨, ∧ and ↔ are defined as usual. If a formula A belongs to the n-language, we say that A is of level n.
Because of the definition of At n , each n-language contains all formulas from all previous m-languages, and every n-language has new formulas, that are not members of any previous languages.
The minimal level of a formula A (Lv(A), for short) is the highest upper index in the set of atomic expressions occurring in the formula A.
We interpret our growing language in structures of the following kind. An epistemic structure is any 4-tuple E = L, S, d, u , where: is a description function that assigns to each language level a set of those states which the agent can consider using the language. The function d fulfills the following conditions: (iv) u : S → S is an updating function which fulfills the condition: Condition (d1) expresses our conviction that there is no n-language that describes nothing. Secondly, we assume that the description of every state is maximally comprehensive, and this can be done in a rich enough language not containing any superfluous expressions. For this reason, for ever state, the description function assigns only one level, and this is stated in condition (d2).
The function u assigns to any state s ∈ d(n) a state t belonging to d(n + 1) which is the update of s, this being condition (u). The agent may update two different states to one state. We do not exclude the situation where some states from d(n + 1) are not updates of any state from d(n). The agent can always consider new states that he could not describe in his earlier poorer language.
For any structure E and any d(n), there may be chosen a certain state from d(n) which verifies a certain set of atomic n-formulas, and the same can be done for subsequent values of function d. In general, each structure E may be described by successive sets of atomic formulas of subsequent n-languages. Every structure with a certain course of chosen sets of atomic formulas forms a history of epistemic changes.
For any E structure and any n > 0, let Ý n : d(n) → 2 At n be a function which assigns to any state s ∈ d(n) a subset of n-atoms. Furthermore, we put Ý := n Ý n . Then a history of epistemic changes is any pair H = E, Ý . For any structure E = L, S, d, u , any history Ý, any state s ∈ S and any n ∈ L we define the relation of satisfaction.
Firstly, for any atomic formula α m i of level n (i.e., when m n and i ∈ I m ) and any s ∈ d(n) we put: Secondly, for any formulas A and B of level n and any s ∈ d(n) we have: Satisfaction for ∨, ∧ and ↔ is defined in the classical way.
Consequently, the concept of validity of A in E, Ý has to be dependent on Lv(A). For any H = E, Ý , we say that a formula A with Lv(A) = m is H-valid iff for any n m and any s ∈ d(n) we have for any H.
Remark 1.1. If Lv(A) = m then for all n < m, satisfaction of A on n (i.e., |= n A) is not defined. In this way, we model the situation that the agent cannot consider as senseful these propositions that he has not yet added to his language. Thus, these propositions cannot be the subject of both kinds of knowledge. Now we can note the difference between our approach and awareness logic. In our case formulas which the agent is not 'aware of', i.e., formulas of higher levels do not belong to his language, and he cannot even express this fact in his current language. ⊣ Remark 1.2. The original semantics for LC is also based on the idea of an expanding language. There, the language is always enriched with one atomic expression that is added to the previous language. In LC, the set of atomic sentences of level n is just {α 1 , α 2 , . . . , α n } and therefore in LC there is no need for double indexing of atomic formulas, in contrast to our approach. LC deals with the concept of a history of changes. In our approach, LC-structures may be defined as any structure E = L, S, d, u satisfying the following condition: Now, the function d chooses, for every n, only one possible state which is the subject of a comprehensive description formulated in the n-language.
Note that in the result, the function u is redundant. The concept of a history of changes may be defined via the definition of a history of epistemic changes. Satisfaction for atomic formulas and ¬, →, C is defined as for LEC. Taking (d * ), we observe that in LC structures, the operator k gets the same meaning as assertion and K as necessity considered in [13]. ⊣

The logic LEC
Let us now characterize the formal system. The proposed axiomatization is an extension of the original axiomatics for LC. As we have already said, the concept of stable knowledge will be fully entangled in contexts with operators of current knowledge and change. Then we prove that the stable knowledge modality has S4.3 properties.
The considered logic LEC is defined as the smallest subset of the set of all formulas of all n-languages which contains twelve axioms and is closed under five rules presented below. Axioms: • all instantiations of all tautologies of classical logic; • all formulas of the following forms: Schemata (K k ), (T k ), (5 k ) express respectively: the closure principle for the current knowledge, its veridicality, and negative introspection. Implication (kC1) states that a change to the agent's lack of current knowledge of A implies current knowledge of A. Following (kC2), we say that the lack of change regarding the current knowledge of A implies current knowledge of the non-change of A. According to (Kk1), stable knowledge implies current knowledge. Schemata (Kk2) and (KC) state that stable knowledge is currently known and it cannot be changed in the sense of ¬ C.
Rules: The first rule is modus ponens. The second one is replacement: The third one is the rule of introduction ¬ C: if A ∈ LEC then ¬ C A ∈ LEC, (gen ¬ C) Rule (gen ¬ C) states that logical theses do not change.
The fourth rule is the rule for introducing k: if A ∈ LEC then k A ∈ LEC.
(gen k) Rule (gen k) says that the agent always accepts theses expressed in his current language.
To introduce the last, fifth rule, we need two types of abbreviations for certain formulas. The first type is as follows. Firstly, for any formula A let: A 1 A be an abbreviation for: In our interpretation this abbreviation equally expresses that: after one step A holds. Indeed, for arbitrary E = L, S, d, u , Ý, s ∈ S and n ∈ L we have: Secondly, for any formula A and any m > 1 we introduce: A m A be an abbreviation for: Let us also assume that A 0 is blank, i.e., for any A we have A 0 A := A.
The abbreviation A m A in our interpretation equally expresses that: after m steps A holds. Indeed, for arbitrary E = L, S, d, u , Ý, s ∈ S and n ∈ L we have: where u 1 (s) = u(s) and u m (s) = u(u m−1 (s)). We obtain this by using from the law of excluded middle for A m−1 A at n and satisfaction for C. The second type of abbreviation is as follows. Firstly, for any formula A let: T 1 A be an abbreviation for: In our interpretation this abbreviation equally expresses that: A holds and it does not change in one step. Indeed, for arbitrary E = L, S, d, u , Ý, s ∈ S and n ∈ L we have: Secondly, for any formula A and any m > 1 we introduce: T m A is an abbreviation for: Let us also assume that T 1 A := T 1 A and T 0 is blank, i.e., for any A we have T 0 A := A. The abbreviation T m A in our interpretation equally expresses that: A holds and does not change in at least m steps.
Indeed, for arbitrary E = L, S, d, u , Ý and s ∈ S we have: Having the above abbreviations we can formulate the fifth rule. For any m 0: This rule is infinistic because for a given m, the conclusion requires infinitely many premises: . . . Informally we can say that according to (Û-rule), if current knowledge never changes then it is stable.
where 2 is a certain operator for unchangeability. ⊣ The soundness and completeness of the logic LEC will be shown in Section 3. Further, we will write '⊢ A' instead of: 'A ∈ LEC'.

S4.3 properties for K
Stable knowledge is veridical, falls under the principle of positive retrospection, the closure principle and is weakly connected. To be more precise, this means that: Theorem 1. Modality K has S4.3 properties, i.e., LEC has the following theses: and it is closed under the following rule: Proof. For (gen K): If ⊢ A, then from (gen k) and (gen ¬ C) for any n 0 we obtain ⊢ T n k A. Next, using classical logic, for any n 0 we have ⊢ α 1 For (T K ): It is a direct consequence of (Kk1) and (T k ). For (4 K ): It is done by induction: We take as the inductive hypothesis: 2. K A → T n k K A and so: 9, (T m ) Therefore, by 1, 2, 10: 11. for any n 0, ⊢ K A → T n k K A 12. ⊢ K A → K K A 11, (Û-rule)

For (K K ): It is done by induction:
In the proof of (.3) we use the following theses: 1. for any n 0, ⊢ K ¬A → T n k ¬A (L1) 2. for any n 0, For (L4): For (.3): 2 We take as the inductive hypothesis: and so: 11, 7, 13 15. for any n 0,

Soundness and completeness
We start with proving the soundness of LEC.
Theorem 2 (soundness). If A ∈ LEC, then A is logically valid.
For (kC2) we assume that there are E, Ý, s, n such that s ∈ d(n), and E, Ý, s |= n k A ∧ ¬ C k A and E, Ý, s |= n k ¬ C A. We have E, Ý, u(s) |= n+1 k A and u(s) ∈ d(n+1) and next for any t ∈ d(n+1) we have E, Ý, t |= n+1 A. From E, Ý, s |= n k ¬ C A and E, Ý, s |= n k A, we state that there is t ∈ d(n) such that E, Ý, t |= n A ∧ C A and next with (u) there is t ∈ d(n + 1) such that E, Ý, t |= n+1 ¬A which gives a contradiction.
All primitive rules preserve logical validity. ⊣ To prove the completeness of LEC, we adopt Henkin construction used in the completeness proof for LCS4 [see 13].
Our aim is to show for any given formula C with Lv(C) = i, if C / ∈ LEC, then there is an epistemic structure E ⋆ and a history Ý ⋆ which falsify C. We need an epistemic structure E ⋆ = L ⋆ , S ⋆ , d ⋆ , u ⋆ in which: Furthermore, this structure is to meet the following conditions: (E ⋆ 1) there is an s ∈ S ⋆ such that ¬C ∈ s and s ∈ d ⋆ (i); (E ⋆ 2) for all s ∈ S ⋆ with s ∈ d ⋆ (n) and n i, and formulas A and B of the i-language: We start with the definition of a LEC-consistent set. A set X is LECconsistent iff there are no A 1 , . . . , A n ∈ X such that ⊢ ¬(A 1 ∧ · · · ∧ A n ).
We relativize the notion of maximal consistency to maximal LEC nconsistency. A set X is maximally LEC n-consistent (we say: maximally n-consistent) iff X is consistent, all elements of X are formulas of level n, and for every formula A of level n: A / ∈ X, then X ∪ {A} is inconsistent. For given n, for maximally n-consistent sets, we have the following lemmas, that we use in the proof of the completeness theorem. Firstly, the following lemma can be proved in the standard way.
Lemma 1. If a set X is consistent, and all elements of X are formulas of level n, then there exists a set Y such that X ⊆ Y and Y is maximally n-consistent.
Lemma 2. If X is maximally n-consistent, then {A : A ∧ ¬ C B ∈ X} ∪ {¬A : A ∧ C A ∈ X} is a maximally n-consistent set.
Thirdly, in a standard way, using only (gen k) and (K k ), we obtain: Lemma 3. If X is maximally n-consistent, and ¬ k ¬A ∈ X then set {A} ∪ {B : k B ∈ X} is consistent. Now we consider the following: Lemma 4. For any finite consistent set X of formulas and any formula F : if for some n 0 we have ¬ A n K F ∈ X, then there is an m 0 such that X ∪ {¬ A n T m k F } is consistent.
Proof. Assume for a contradiction that X is finite, consistent, and for some n 0 we have ¬ A n K F ∈ X but for any m 0 the set X ∪ {¬ A n T m k F } is inconsistent. Then for any m 0 we have ⊢ X → A n T m k F , where X is a conjunction of formulas from X. Hence from (Û-rule) we have ⊢ X → A n K F , but ¬ A n K F ∈ X, which means, that X is inconsistent. ⊣ For the formula C / ∈ LEC we will now show how to build the structure E ⋆ that we are looking for. Assume that C with Lv(C) = i is not an LECtheorem. We have that {¬C} is consistent. We take the enumeration of all formulas of level i: A 0 , A 1 , A 2 , . . . ; and we define the sequence (S j ): For S 2j+2 we consider two cases. If A j belongs to S 2j+1 and A j = ¬ A n K F , for some n 0 and some formula F , then  in virtue of Lemma 4  for some m 0 we can put S 2j+2 := S 2j+1 ∪{¬ A n T m k F }. Otherwise, we put S 2j+2 := S 2j+1 .
Let s = j S j . From Lindenbaum's lemma we obtain that s is maximally i-consistent and ¬C ∈ s. In the set s it is guaranteed that if for any n 0 we have A i T n k A ∈ s, then A i K A ∈ s. Now we define the sequence W i , W i+1 , . . . of families of sets It is well defined because of Lemmas 1-3. All maximally i-consistent sets from the above sequence have the following property: if for any n 0 we have This is a consequence of Lemma 8 that we prove later. 3 The above sequence will be used to define the domain of the structure that we are looking for.
We have that every X ∈ W n is maximally i-consistent. To each X ∈ W n , we will add new atoms of all level m such that i < m n (these atoms do not belong to the i-language). This will allow us to check to which the language level the given state (which now will be a set of formulas) is assigned.
We Proof. Condition (E ⋆ 1) is fulfilled by the definition of sequence (S j ) and the definition of E ⋆ . Conditions (⋆ ¬ ) and (⋆ → ) are consequences of the definition of the sequence of sets W i , W i+1 , . . . , the definition of E ⋆ and the fact that each X ∈ W n is maximally i-consistent. Condition (⋆ C ) is a consequence of the definition of the sequence of sets W i , W i+1 , . . . , and (⋆ ¬ ), (⋆ → ). We get (⋆ T ), (⋆ A ) from (u ⋆ ), (d ⋆ ), (⋆ ¬ ), (⋆ → ) and (⋆ C ). ⊣ Lemma 7. In the structure E ⋆ condition (⋆ k ) is fulfilled.
For the converse implication, we assume that there exists formula A, of the i-language and ∀ t∈d ⋆ (n+1) A ∈ t and ¬ k A ∈ s and s ∈ d ⋆ (n + 1). Thus, from the definition of the sequence of sets W i , W i+1 , . . . , and (d ⋆ ) there must be t ∈ d ⋆ (n + 1), such that A ∈ t, which contradicts our assumption. ⊣ Lemma 8. In the structure E ⋆ condition (⋆ K ) is fulfilled.
Proof. "⇒" We assume that for some formula A of the i-language we have: K A ∈ s, s ∈ d ⋆ (n) and for some m n and t ∈ d ⋆ (m) we have A ∈ t. We have that there exists m 0 n and t 0 ∈ d ⋆ (m 0 ) such that A / ∈ t 0 . If m 0 = n, then a contradiction arises because of (Kk1) and (⋆ k ). Let m 0 > n. We have, that K A ∈ s, thus from (KC) we obtain K A ∧ ¬ C K A ∈ s and therefore with (⋆ C ) K A ∈ u ⋆ (s), so again from (KC) we obtain K A ∧ ¬ C K A ∈ u ⋆ (s), and again from (⋆ C ) we have K A ∈ u ⋆ (u ⋆ (s)). In this way, we will get to K A ∈ u ⋆ (u ⋆ (...(s)...) ∈ d ⋆ (m 0 ); and so by using (Kk1) and (⋆ k ) we obtain A ∈ t 0 which gives a contradiction.
"⇐" We assume that for any l n and v ∈ d ⋆ (l) we have A ∈ v and ¬ K A ∈ s and s ∈ d ⋆ (n). First we show that ¬ A n−i K A ∈ s (note, that s is an element of d ⋆ (i) and formula ¬C ∈ s and Lv(C) = i). We assume that A n−i K A ∈ s, then from (⋆ A ) K A ∈ u n−i ⋆ (s) and u n−i ⋆ (s) ∈ d(n). Thus, using axiom (Kk2) we obtain k K A ∈ u n−i ⋆ (s). Now, because of u n−i ⋆ (s) ∈ d ⋆ (n), and from (⋆ k ), we have K A ∈ s which is false by assumption. Now, from ¬ A n−i K A ∈ s and the definition of the sequence (S j ), we obtain that ¬ A (n−i) T m k A ∈ s for some m, therefore from (⋆ A ) we have T m k A / ∈ u n−i ⋆ (s), for some m. Thus, from (⋆ T ) there exists a state t ∈ d ⋆ (j) such that n j m and ¬ k A ∈ t. Therefore, for some v with v ∈ d ⋆ (j) and n j m we have ¬A ∈ v from (⋆ k ), which contradicts our assumption. ⊣ Theorem 3 (completeness). If A ∈ LEC, then A is not logically valid.
Proof. Assume that C / ∈ LEC and Lv(C) = i. We construct a state s with ¬C ∈ s defined as in the sequence (S j ). Using the definition of the sequence of sets W i , W i+1 , . . . , we define E ⋆ = L ⋆ , S ⋆ , d ⋆ , u ⋆ in the way described by conditions (L ⋆ ), (S ⋆ ), (u ⋆ ) and (d ⋆ ), which fulfils to K-free fragment of LEC. Formula (NL K ) is logically valid and thus from completeness we know that it is also a thesis of LEC.
In our approach formulas (NL k ) and (NL K ) describe the situation in which the agent is learning, in the sense that he always can discover new states. He can describe them in his new richer language. Our idea is that the agent adapts his states to his current knowledge, and does not reject them as in the case of perfect recall. The extension of LEC by (PR k ) imposes a restriction of the class of E structures to the class which additionally fulfils the following condition: ∀ s,t∈d(n+1) ∃ s ′ ,t ′ ∈d(n) (u(s ′ ) = s and u(t ′ ) = t).
We have similar problems when we accept (PR K ) as an axiom. This shows that if the agent wants to make full use of the idea of a growing language, he cannot accept the perfect recall postulate.
The changeability of the agent's knowledge over time has been also studied in the frame of branching-time temporal logic [9]. The idea of using two primitive concepts of change interpreted in branching structures linked with the concept of growing language is elaborated in [7]. Perhaps this approach could be used as a starting point for a new version of the epistemic formalism presented here.