{'fraction_non_alphanumeric': 0.04248174404349448, 'fraction_numerical': 0.003118170673205053, 'mean_word_length': 3.9515703351807865, 'pattern_counts': {'":': 0, '<': 1, '<?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': 8, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Epistemic Logic with Functional Dependency Operator

Epistemic logic with non-standard knowledge operators, especially the"knowing-value"operator, has recently gathered much attention. With the"knowing-value"operator, we can express knowledge of individual variables, but not of the relations between them in general. In this paper, we propose a new operator Kf to express knowledge of the functional dependencies between variables. The semantics of this Kf operator uses a function domain which imposes a constraint on what counts as a functional dependency relation. By adjusting this function domain, different interesting logics arise, and in this paper we axiomatize three such logics in a single agent setting. Then we show how these three logics can be unified by allowing the function domain to vary relative to different agents and possible worlds. A multiagent axiomatization is given in this case.


Introduction
De re knowledge or in general non-standard knowledge in epistemic logic is attracting continuing attention. This line of research started from the very beginning of epistemic logic: Hintikka discussed a "knowing-who" operator in [3], and Plaza a "knowing-value" operator Kv in his seminal work [4]. However, it is the recent effort in providing formal semantics and axiomatizations of those nonstandard knowledge operators, as outlined in the survey [8], that layed a solid foundation for further investigation. Among all the non-standard knowledge operators axiomatized so far, the "knowingvalue", or equivalently the "knowing-what" operator, has received most attention, partly due to its mathematical elegance and partly because of its potential application in information security reasoning.
Recent major development of this Kv operator started with the axiomatization in [10,9], followed by the all epistemic scenarios. Thus, F can be seen as an agent's prior knowledge about possible functional dependency relations, and to know the dependency between variables is to find a possible function that works or explains all possibilities. To put it more colloquially, to know the functional dependency between c and d is not simply to see that functionality holds between them, but also to see that the functional relation "make sense". Let us use Kf (C, d) to express this knowledge of functional dependency of d upon a finite set of variables C.
As argued above, when "knowing-dependency" serves as a tool for expressing potential "knowingvalue", we do not need a requirement stronger than functionality. But this is not always the case. Certainly the functionality from c to d holds as d has only one possible value. But agent A is apparently ignorant about the functional relationship between variables d and c. The witness to the functionality here is the constant function 0, which is extremely unlikely to be the encryption function enc that B uses. So agent A would not in this case assert that she knows that the message d she receives is derived from the message c that B intends to send through some encryption: no encryption function she deems possible would allow all those possibilities. Thus, to claim the knowledge of the functional dependency of d on c, we do need something more than functionality. With our operator Kf , we can use Kf A ({c}, d) to express "A knows a functional dependency relation between c and d that is plausible in the information security context", if we let F to be the set of all functions that is plausible in this context.
Thus, the Kf operator can be used to model scenarios where the value of variables in the realized world (the agent's world) is not the sole concern of the agent. It might be that our agent does not want an inexplicable relationship between variables, or it might be that the agent requires that any functional dependency she knows to be applicable not only to her actual world but also to worlds metaphysically possible or worlds evolved in time, where some a priori rules preclude too strange functional dependency relationships. In the previous case, certainly d is known to A already, but the constant function that witnesses the functionality there is not likely to be applicable to another round of message exchange.
In the rest of the paper, we first define the logic that incorporates knowledge K, "knowing-value"Kv and "knowing-function"Kf operators which we call LKVF and the corresponding base axiom system LKVF. Then we show how different domains of functions, viewed as a parameter of LKVF, induce different sets of validities and axioms. Then all those cases will be put into a unified framework where a multiagent logic with the same operators is axiomatized. In the last section, we will discuss further interpretations of "knowing a/the functional dependency between variables" and possible future work.

Syntax and Semantics of LKVF
Definition 1 (Syntax) Given a countably infinite set P of propositional letters and a set Q of the names of variables, the formulas in LKVF are defined by: where p ∈ P, d ∈ Q, and C ⊆ f in Q. ⊆ f in means a finite subset, possibly empty.
Here Kv(d) is to be interpreted as "knowing the value of d", and K φ "knowing that φ is the case".
In order to interpret the Kf operator in LKVF, we need a predefined domain G of possible values for variables in Q, and a set of F functions on this G. F might contain polyadic functions in G G n and also zero-adic functions. Formally F ⊆ ∞ n=0 G G n . It is important to note here that in this setting, F and G are important parameters of LKVF instead of parts of the models. In other words, they are shared by all models in the logic.
As we are considering single agent S5, no explicit accessibility relation is needed. So formally, a model is: where W is the set of possible worlds, U : W × P → {0, 1} is the assignment for propositional letters, and V : W × Q → G is the assignment for variables. For any finite subset C of Q, we fix an order of the elements in C and define V(w, C) = V(w, d) | d ∈ C . When C is empty, this degenerates into the unique empty tuple. We call this the joint assignment of variables in C, and whenever we have a function from Q to G, if it is applied to a set C, we mean this joint assignment. Now the truth conditions are: Here the Kv operator has the same meaning as that of Kv in [10]: To summarize, our logic LKVF extends the standard propositional epistemic logic by adding Kv(d) and Kf (C, d) to the language, adding a valuation of the variables to the models, and introducing a new function domain F as part of the logic. Now it has the following parameters: • P: the set of propositional letters • Q: the set of variable names • G: the set of values that variables can take • F: the set of functions that the agent deems possible a priori.
All of them will have some effect on the validities of LKVF, but P and Q will remain unchanged throughout the whole paper, since they can be viewed as part of the language. G needs to be large for completeness results, and we will specify how large it should be. F will change the validities in LKVF in an interesting way. Thus, it will be one of the main focuses of this paper. Later we show how F can also be put into the models.

Base Axiom System and Soundness Condition
As defined above, the Kf operator expresses functional dependencies among variables and thus resembles the dependency relation in database theory. Using Armstrong's three axioms in [11], we obtain this base system LKVF: Here only the projectivity and transitivity axioms are used. The reason is that in our language the syntax of Kf allows only one variable to be dependent upon a set of variables, not a set upon a set. Thus, By convention, an empty conjunction is ⊤. So when the set D in TRAN is empty, it actually says Kf (∅, e) → Kf (C, e) for all C ⊆ Q. And when the set C in VF is empty, it says Kf (∅, d) → Kv(d).
We will discuss the axiomatizations of three different settings using a large, a small, and an intermediate F in LKVF respectively. For them, we either use LKVF itself or add some other special axioms. To simplify repetitive work, here we give a condition on F in LKVF for the soundness of LKVF: Proposition 1 When F satisfies the following, LKVF is sound with respect to LKVF: • For every i, j ∈ N such that 0 < i ≤ j and function f : We denote this special projection function as id i, j .
Namely, F is closed under function composition.
Proof. Here we only prove the soundness of the three less trivial axioms: • By the first property of F, PROJ holds. If d ∈ C, suppose d appears in C as the ith variable, then • We want to show VF : Let C be enumerated as c 1 , . . . , c n and suppose the antecedent in VF holds. Then c ∈C Kv(c) is true. This means we have a tupleā ∈ G n such that ∀w, V(w, C) =ā.
Further we have Kf (C, d), which means we have a f ∈ F such that Thus, there exists an element b := f (ā) ∈ G such that d evaluates to it in all possible worlds.
We will briefly mention how F is going to satisfy this soundness condition in all the following cases.

Full Domain of Functions
In this section, we deal with the case where F is as large as possible, namely Now the Kf operator degenerates into a functionality test, as all functions are allowed: This is true because once we have the right hand side true, we will obtain a partial function f satisfying And it is trivial to extend this partial function into a total function.
, so the right hand side of the above truth condition holds, and consequently, Kf (C, d) is true in M, w. This justifies the soundness of our new axiom in this case: where C ⊆ f in Q, possibly empty. We name this axiom EXT because it means that in this case every function on G, regardless of its meaning, can serve as a witness of the truth condition of Kf . Further, F satisfies the condition given in Proposition 1, so LKVF + EXT is sound. In the following, we prove that if G is sufficiently large, then LKVF + EXT is in fact complete as well.
Given an arbitrary set A of formulas consistent in LKVF + EXT, the Lindenbaum lemma enables us to construct a maximal consistent set Γ such that A ⊆ Γ. Now to build a model for Γ, we need To this end, we first define some useful sets. Given any maximal consistent set Γ, define They collect all the propositional and the value knowledge respectively in Γ. For any C ⊆ Q, we say well. Using axioms TRAN and PROJ, it is not hard to see that for all C ⊆ f in Q, is closed under Kf in Γ and C ⊆ C +Γ . This can be seen as the dependency hull of the finite set C.
in particular Kv Γ ⊆ ∅ +Γ . So Kv Γ = ∅ +Γ . This motivates us to define the set of all finitely generated closed sets: Clearly M Γ is non-empty, and Kv Γ ∈ M Γ . Also, for all X ∈ M we have Kv Γ ⊆ X, so in other words, any finitely generated closed set contains all variables with known value. Then, we have the following disjoint decomposition of Q using X ∈ M Γ : Intuitively, the values of the variables in Kv Γ must hold fixed among all possible worlds; the values of the variables in X\Kv Γ must vary relative to those in Kv Γ in a uniform way to respect the functional dependencies among them; and the values of the variables in Q\X must vary even when all values in X\Kv Γ are fixed, since they are not determined by X.
where the columns are possible assignments. For every X ∈ M Γ which collects all closed set of variables, we need such possibilities to take care of all formulas of the form ¬Kf (C, d) in Γ, because there will be one X, namely C +Γ , that separates C and d. Then, the value of d can vary even when those of C are fixed.
The reason we are using only finitely generated closed subsets of Q is that, when |Q| is infinite, the cardinality remains the same.
Notice how this satisfies the informal requirement, illustrated by the example above, over the values the variables in different regions should take. When d ∈ Kv Γ , its value is fixed to g(∅, 0). When d ∈ X\Kv Γ , its value depends on X as a whole but nothing else, so all variables in X\Kv Γ change uniformly from what they are assigned by g(∅, ·). When d ∈ Q\X, its value further depends on i, so will change even when the values of the variables in X are fixed.
Formally, this definition allows us to show: Proof. For the first part, the witness is x = g(∅, 0) and can be verified easily. For the second part, For the third part, two cases are possible.
to d on all X, i , making the consequent of the implication to be proven true throughout. Now suppose C Kv Γ and take c ∈ C\(Kv Γ ) and X, i , . We first show X = X ′ by focusing on this c Kv Γ . Since c Kv Γ , by the definition of V p , there exists j, k ∈ {0, 1} such that By the injectivity of g, they are equal only if at least X = X ′ . Based on this, if i = i ′ then X, i = X ′ , i ′ and trivially d receives the same value from V p .
. For all c ∈ C, it follows that c ∈ X as otherwise the values V p gives to c differ on i and i ′ . Hence C ⊆ X and by assumption X ∈ M Γ , which means X is closed. Thus, as Kf (C, d) ∈ Γ, d ∈ X as well. By definition, For the last part, we assume that Kf (C, d) Γ. Then d C +Γ . By the injectivity of g and the fact The above proposition handles the knowledge and ignorance about values and functional dependencies.
Now we need to combine it with a traditional completeness proof for epistemic S5 logic. Denote Here L is non-empty since by axiom T, K Γ ⊆ Γ so at least Γ ∈ L. Then we define a model on possible where [p ∈ ∆] is the indicator function of the statement p ∈ ∆, which evaluates to 1 if the statement is true and 0 otherwise. Here each possible world has three components: a maximally consistent set which contains all formulas true at the world (truth lemma), a closed set of variables C which is responsible for instantiating the ignorance of the values of variables in C under the functional dependency constraint, and a number 0 or 1 which is responsible for instantiating the ignorance of the functionality property between variables in C and variables outside C.
Now the goal is to show a truth lemma, i.e., for all ∆, To this end, we first need the following simple observation.
Proof. Simply use the axioms 4, 5. For example, the third property follows from Proof. A standard exercise using necessitation and axiom K.
Now we can prove the truth lemma: Proof. By induction on φ, with the following possibilities: • φ is a propositional letter or a boolean combination. This is standard.
As such, From this proposition, we know that for all φ ∈ Γ, M, Γ, ∅, 0 φ. As the consistent set A we chose at the very beginning is contained in Γ, M, Γ, ∅, 0 A, which brings us:

Minimal Function Domain
In Proposition 1 we proved the soundness condition for LKVF. Notice that the minimal function domain that satisfies this soundness condition is In this section, we consider the axiomatization of the validities of LKVF with this F. Here, two axioms besides our base system LKVF are valid: The validity of the first axiom is justified by: and notice that when C = ∅, it degenerates to Kf (∅, d) → ⊥ or equivalently ¬Kf (∅, d), which is true because no zero-ary function exists in F. This also means that EXT is unsound in this case, because The validity of the second axiom follows from Thus, LKVF + CHOO + EQU is sound. Given these two axioms and the fact that F consists only of projection functions, Kf (c, d) is actually talking about the equality of c, d over all possible worlds, even though the value might not be known. This motivates the construction of the equivalence relation by Now we turn to the proof of the completeness of LKVF + CHOO + EQU. Again, given a consistent set A, our plan is that we first extend it to a maximal consistent set Γ, then deal with its de re knowledge and propositional knowledge separately, and finally take their Cartesian product to obtain a model of

Γ.
First, we partition Q into equivalence classes with equivalence relation ∼ defined by Its reflexivity, symmetry and transitivity follow from the axioms PROJ, EQU, and TRAN. Indeed, if we use the C +Γ and M Γ construction, M Γ will contain precisely those partitions and their unions. Every maximally consistent set, or a "world", naturally gives rise to such an equivalence relation on Q.
the collection of the equivalence classes which contain at least one of its elements. In particular, For example, we can let u be any injection and then make a rotation over the function values of u on in case of Q being infinite (assuming it can be well ordered). We do not need to seek more valuations of variables to prove the truth lemma in this case or to instantiate the ignorances of the knowledge about values in Γ. Any one of them is capable of refuting Kf (C, d) Γ and together they instantiate , the following proposition is true: Proof. The first two parts are immediate from the definition of u, v: For the third property, suppose Kf (C, d) ∈ Γ and enumerate C by c 1 , . . . , c j . By axiom CHOO and the maximality of ) and we see that the functional By axiom PROJ, Kf (C, c) ∈ Γ, and then by axiom . Actually we can use v here as well. The reason we need both of them is that we need to instantiate ¬Kv(d) for d Kv Γ .
To build a model for Γ, define Then we have the following truth lemma: Proof. The proof is similar to that of Lemma 1. The difference is that we need to use Proposition 5 instead of Proposition 2.
The completeness of LKVF + CHOO + EQU follows, so we conclude:

Intermediate Function Domain
In the previous two sections, we considered the minimal and the maximal function domains subject to our soundness condition. As we can see, in both cases the axiomatizations require some axioms besides the base system LKVF. And those axioms are not very intuitive if we intend to interpret Kf as "knowing a/the functional dependency". In this section, we show that we can construct a function domain such that if F is set to it, LKVF will be complete and no extra axiom is needed. The construction is somewhat artificial but in the next section, we can view this as just one step of a completeness proof at a higher level.
The main difficulty here is to refute the axiom scheme EXT used in the axiomatization of the full function domain case. EXT is validated in that case because whenever the value of a variable is known, a constant function can be used to explain the functional dependency between it and any other variables in all epistemic possibilities. Thus, to refute this scheme as an axiom, we must make sure that the function domain encodes information more than just functionality so that we can refute Kf (c, d) even when functionality holds, such as when Kv(d) is true. The function domain to be constructed below will enable a suitably constructed model to refute Kf (C, d) without ever looking into the functionality condition.
To do this, we go to higher dimensions by assuming G = 2 P f (Q) , interpreted as functions from the finite subsets of Q to {0, 1} or as a rather long sequence indexed by P f (Q) where at each index (dimension) C we can choose from {0, 1}. This is actually only a size requirement, since so long as |G| ≥ |2 P f (Q) |, we can always embed 2 P f (Q) into G by an injection. For any x ∈ G and C ⊆ f in Q, we use x[C] to retrieve the image of C under x, which will be 0 or 1. Now we construct the intermediate Alternatively, where Notice that the requirement is specified for all dimensions individually, and they do not interfere with each other. This allows us to do constructions and proofs for each dimension separately. not by a failure of functionality but by a failure of conformation to F. Breaking functionality requires at least two possible value assignments, but if F says no, a single possibility is too many. Recall the C +Γ we used in the previous two cases, which is defined as {d ∈ Q | Kf (C, d) ∈ Γ}. Now we need to define a slightly different M Γ : This is the collection of all finitely generated closed sets plus Kv Γ . We need this extra union since axiom EXT is not available now, which means Kv Γ is not automatically contained in any C +Γ , and it is quite possible that Kv Γ is not finitely generated. But still, M Γ has a cardinality no larger than P f (Q), since if Q is finite, P f (Q) contains all subsets of Q, and if infinite, P f (Q) is also infinite and adding one more element into it does not increase its cardinality. Thus, there is still a surjection g from P f (Q) to M Γ . We can think of this g as a pseudo (·) +Γ function, and it does not matter which surjection we use for g. Now we can specify the two valuations we need: The use of V 0 is to refute Kf (C, d) if ¬Kf (C, d) ∈ Γ, and the use of V 1 is to refute Kv if ¬Kv(d) ∈ Γ.
Now we prove this in detail: Proof. To prove the first claim, assume Kf (C, d) ∈ Γ with C enumerated by c 1 , . . . c n . We will construct a function f ∈ F that works in both V 0 and V 1 : and . Obviously this construction should be done dimension by dimension.
For any D ⊆ f in Q, the possibilities are: To prove the second claim, recall that C +Γ = {d | Kf (C, d) ∈ Γ} is closed under Kf in Γ and contains C by axioms TRAN and PROJ. Now since Kf (C, d) Γ, d C +Γ . As g is a surjection from P f (Q) , which makes it impossible to find a function f ∈ F such that f (V 0 (C)) = V 0 (d).
If Kv(d) Γ, d Kv Γ . Since we explicitly added Kv Γ to Γ, Kv Γ ∈ M Γ , and we can find a C ⊆ f in Q such that g(C) = Kv Γ . Then, using the definition of V 0 and V 1 , we know V 0 (d) Based on the previous two propositions, we can build a model for Γ by defining   when functionality cannot be used. This is actually the reason why the cardinality requirement for G is very high there. However, in the current setting where function domains are part of the models, the only thing needed is a method to build a function domain for each maximal consistent set Γ so that the functional dependency relation between C, d is rejected if ¬Kf (C, d) ∈ Γ. The difference will be made more clear in the following multiagent case.

Multiagent logic with variable function domain
Given an index set A of agents, to accommodate multiple agents, the language is now expanded to with p ∈ P, i ∈ A, d ∈ G, and C ⊆ f in G. The only difference from the single agent language defined in Definition 1 is that now we have for each agent i a separate Kv i , Kf i , and K i .
For semantics, a model is now defined as: where F i is intended to assign a collection of functional relationships that agent i deems possible a priori to all possible worlds in W. Thus, for all w ∈ W, i ∈ A, F i (w) is required to include all projection functions and to be closed under function composition. ∼ i is the epistemic accessibility relation of agent i and is required to be an equivalence relation on W, the set of possible worlds (complete epistemic scenarios). Now since F i is supposed to be "prior knowledge", it is also required that if w ∼ i w ′ , then . However, we are not assuming that the prior knowledge of any agent is public to other agents, so it is quite possible that F j (w) F j (w ′ ) if j i, even when w ∼ i w ′ . In a nutshell, F i s are not common knowledge.
The semantic clauses are defined similarly with agent indices for knowledge sentences: Let LKVF * m name this multiagent logic. Also, let LKVF m denote the axiom system adapted from LKVF with indexed version of those axioms involving knowledge operators. In particular, no interaction between agents is allowed, as there are no axioms saying that we can derive any knowledge about other agents from any agent. We will see that this is precisely because we allow each agent to possess its own prior knowledge about possible functional dependencies, not necessarily known to other agents. Once we assume that F i s are common knowledge, interactions will arise, and we will discuss this point in the last section.
The soundness of LKVF m with respect to LKVF * m follows from an indexed version of Proposition 1. For completeness we need a new construction: Definition 5 (Dependency lattice) Given a maximal consistent set Γ in LKVF m and an agent index i, first define the indexed version of the (·) +Γ operator, Cl Γ i , on finite subsets of Q as Then, extend this operator to P(Q) by When the context is clear, we may drop the superscript or subscript of Cl Γ i . Now this is a finitary closure operator as it satisfies, through the axioms of LKVF m , When a set C ⊆ Q satisfies C = Cl(C), it is called a closed set. A classical result is that the collection of all closed sets under a closure operator forms a lattice L, ∧, ∨ with to save a few brackets.
Also, given Γ, the indexed version of the propositional knowledge and the value knowledge of agent i is denoted by Then, it is not hard to see that This is because the closure operator Cl Γ i uses only the formulas of the form Kf i (C, d) in Γ, and if we assume For the completeness proof to go through, there is again a cardinality requirement for G: |G| ≥ |Q × {0, 1}|, and without loss of generality, we identify G with Q × {0, 1}. The Q part will be used to construct the function domains and refute Kf (C, d), while the {0, 1} part will be used for refuting

Kv(d).
To use the Q part to construct the function domains, we need to forget the {0, 1} part. Define This map is forgetful about the second coordinate and turns a variable name into its closure. Again the superscript and subscript are dropped when no confusion arises. Now we are able to define a new version of the Lmax function set: Definition 6 Given a maximal consistent set Γ and an agent index i, we can construct the dependency lattice L and the corresponding h. Then define F i (Γ) to be the collection of all functions f on G with any arity n ∈ N such that: The empty disjunction is the bottom element of L: Cl(∅).
It is straightforward to see that F i (Γ) is dependent only on K i,Γ . Then we need to verify the soundness conditions immediately: Proposition 8 For every maximal consistent set Γ and i ∈ A, F i (Γ) contains all projection functions on G and is closed under composition.
Proof. Take a projection function f (x 1 , . . . x n ) = x k . Then by the definition of join in a lattice, For function composition, let x represent a sequence of variables and h(x) the sequence after the application of h. Then take a function f (x) = g 0 (g 1 (x 1 ), · · · g n (x n )) where x includes the union of all x k s and all g functions are already in F i (Γ). Now This shows that the composition f satisfies the requirement and is in F i (Γ).
The next proposition shows why we use the dependence lattice to define the function domains for each agent. The proposition says that to make Kf i (C, d) true, we only need to make sure that functionality holds, and to make Kf i (C, d) false, we do not need to pay any special attention as the function domain F i (Γ) has already taken care of everything.

Proposition 9
For every σ ∈ 2 Q , define v σ : Q → G, d → d, σ(d) . This means we restrict the value of d ∈ Q to be d, 0 or d, 1 . Now for every maximal consistent set Γ, i ∈ A, C ⊆ f in Q, d ∈ Q, and Σ ⊆ 2 Q : • if Σ satisfies the functionality condition for C, d, namely for all σ 1 , σ 2 ∈ Σ, σ 1 (C) = σ 2 (C) Proof. First notice that in the definition of F i (Γ), the restriction actually forgets the second coordinate of the inputs and outputs. But it is the second coordinate that all σ ∈ Σ try to adjust. By definition, the first coordinates of v σ (c) for all c ∈ Q are just themselves. So for all c ∈ Q, σ ∈ Σ, h(v σ (c)) = Cl(c).
If Kf i (C, d) ∈ Γ, then (dropping the super and subscripts) d ∈ Cl(C). This means the same as {d} ⊆ Cl(C), which, by the fact that Cl is a closure operator, implies Cl(d) ⊆ Cl(Cl(C)) = Cl(C). Then Cl(d) ⊆ Cl(C), which means h(v σ (d)) ≤ Cl(C) in L for all σ ∈ Σ. Also, Together with the functionality assumed for Σ, this means mapping v σ (C) to v σ (d) simultaneously for all σ ∈ Σ is allowed in F i (Γ). Then we can extend this partial map to a map from G n to G in F i (Γ).
An easy solution is to do projection for all other possible inputs.
If Kf i (C, d) Γ, then d Cl(C) and hence Cl(d) Cl(C). If Σ is empty, the statement is trivially true. So assume Σ is not empty. Now take an arbitrary σ ∈ Σ. Then h(v σ (d)) ≤ h(v σ (C)), which violates the restriction on This proposition says that the dependency lattice L Γ i and the corresponding function domain . So in this case, no functional dependency exists from C to d, but the reason is not that d is at the wrong place in the lattice, but instead the failure of functionality. We must avoid this situation, by changing all values of variables in Kv i,Γ simultaneously when producing a new possible assignments in a new possible world.
This motivates the following definition: Definition 7 (Value Move) Given Γ a maximal consistent set and i ∈ A, define the value move This operator captures agent i's switching of the values of the variables in Kv i,Γ all at once. Two important properties should be noted. First, Mv Γ i is dependent only on K i,Γ . Indeed it only depends on Kv i,Γ but because of the axioms KV4 and KV5, it is equivalent to say that it depends only on K i,Γ . This means that if K i,Γ = K i,Γ ′ , then as an operator, Mv Γ i = Mv Γ ′ i . Another important property of this operator is that Mv Γ i (Mv Γ i (σ)) = σ for all Γ, i, σ ranging over maximal consistent sets, A and 2 Q . Thus, it is actually an inverse operator.
Equipped with the above definitions, the canonical model can now be defined: which says that two worlds must share the same set of knowledge of i, and 2. σ = σ ′ or σ = Mv Γ i (σ ′ ), which says that any agent i needs to see some different possible assignments of the variables, but not too many: just two, • V( Γ, σ , d) = d, σ(d) , or equivalently using notations introduced above in Proposition 9, Before proving the truth lemma, it must be shown that M is indeed a model of LKVF * m . This amounts to checking the following: • ∼ i is an equivalence relation for all i ∈ A, • F i ( Γ, σ ) satisfies the soundness condition, Because ∼ i is defined using equality, its reflexivity is easy to see. We need the two special properties of Mv Γ i noted right after the Definition 7 to show symmetry and transitivity. For symmetry, suppose Γ, . Also, as Mv Γ ′ i is an inverse operator, by applying it twice, we get σ ′ = Mv Γ ′ i (σ). So it can be concluded that Γ ′ , σ ′ ∼ i Γ, σ .
Transitivity can be shown similarly. Suppose Γ 1 , σ 1 ∼ i Γ, σ ∼ i Γ 2 , σ 2 . It immediately So we can treat all of them as Mv Γ i . Then we know σ = σ 1 or σ = Mv Γ i (σ 1 ), and σ = σ 2 or σ = Mv Γ i (σ 2 ). There are in total four possibilities depending on which disjuncts hold, and the only less trivial one is when So transitivity holds. The soundness condition was already shown when F i ( Γ, σ ) = F i (Γ) is defined in Proposition 8.
We also noted that F i (Γ) only depends on K i,Γ because it only depends on the dependency lattice L Γ i , which in turn only depends on The unconventional second condition for ∼ i is there for the purpose of preventing unwanted failure of functionality. As explained after Proposition 9, we are not refuting Kf (C, d) using functionality, so it is better to keep the functionalities between as many variables as possible. In particular, all functionalities between the variables in Kv i,Γ can be preserved. Proof. Use induction on φ. The propositional letters and boolean combination cases are conventional.
We focus on the knowledge cases.
Then we should first show that the functionality condition holds. For any Γ 1 , σ 1 , Γ 2 , σ 2 ∼ i Γ, σ , if V( Γ 1 , σ 1 , C) = V( Γ 2 , σ 2 , C), then there are two possibilities • C ⊆ Kv i,Γ . Then by axiom VF, d ∈ Kv i,Γ as well, and by the argument in the previous case, . But the latter case cannot happen because if that is true, then σ 1 (c) σ 2 (c) since c ∈ Kv i,Γ . So σ 1 = σ 2 and in particular σ Indeed, by our definition of ∼ i , among all worlds accessible from Γ, σ by ∼ i , there are altogether only two possible valuations: σ and Mv Γ i (σ). Thus, by applying Proposition 9 to set If Kf i (C, d) Γ, then by Proposition 9 again, for every function From the truth lemma, it can be concluded that every consistent set is satisfied somewhere in the canonical model M built above. So the completeness of LKVF with respect to LKVF * m follows. Together with the soundness proven in Proposition 8, we obtain an axiomatization of LKVF * m : It could be argued that the agent can nevertheless regard all those candidates as equivalent, because they must have exactly the same behavior over the partial domain P = {V(w, C) | w ∈ W }. And things in G |C | but outside this set P are epistemically impossible. Thus, the behavior of functions on G |C | \P is something that our agent can and will ignore if situations epistemically impossible do not concern the agent. One example, also mentioned in the introduction, is when "knowing-value" is the real objective of the agent and "knowing-dependency" only expresses the agent's potential to know more values. The semantics proposed in this paper allows adjustments to F, which might be a consequence of an agent's concern about situations epistemically impossible, but not necessarily. Thus, it might be of interest to capture knowledge of functional dependency in another modality.
To do this we can add a new modality interpreted by a relation R. Then "knowing a/the functional dependency" can now be expressed by an operator Kf with the following semantics: where ∼ is the epistemic indistinguishability relation. This definition still says that there exists a function that works for all epistemically indistinguishable worlds. But here "works" means f captures the functional dependency of d upon C with respect to another modality which might be different from K. to be valid, we need R to be reflexive. Otherwise, the functional dependency might be only talking about worlds far away from the actual world, though accessible through R. Since the choice for R can be flexible, there will be many interesting results to be discovered under this semantics. In particular, for the study of completeness, we might want to add more first order features to facilitate a proof more similar to its first order counterpart, a strategy successfully employed in [1]. It might be desirable because, with two modalities, a direct construction of value assignments can be unmanageable.
But a demanding reader may still not be satisfied, as even if we add a new modality, the choice of the functions could be nonunique again. This motivates another interpretation of knowledge of functional dependency, emphasizing even more the "knowledge" part: Kf (C, d) says that the agent has gathered so much information that there is (almost) exactly one function that can be used to explain the data he/she has seen so far. Thus, knowledge appears only when there is only one possible or a few very plausible explanations. If there is no possible explanation in the sense that no function in the function domain F is applicable, or there are too many explanations, no knowledge is obtained. This sounds natural, but much more technically will be needed to formalize this: either a counting operator, or a probabilistic operator tracking the posterior distribution over the candidate explanations.
There are also interesting possible extensions of the framework given in this paper. For example, the multiagent case here assumed a no-interaction semantics. But once we require prior knowledge of possible functions to be available to other agents, interesting interactions will appear. For example, suppose F j is known to agent i, i.e., if w ∼ i w ′ then F j (w) = F j (w ′ ). Then the following is valid: Intuitively this says that if agent i knows the values of c, d and knows that agent j knows, then either i knows that j has an explanation of the value of c, d or i knows that j does not have one. The antecedent fixes the value of c, d in all worlds accessible first from i and then from j. Thus if j fails or succeeds to explain this particular instance, agent i knows it. Stronger interactions will appear if we require all agents to share a single prior knowledge base F, i.e., for all i, w, F i (w) = F. Then the following is valid: j (c, d)).
This says that if i knows the value of c, d and knows that j knows them, then i being able to explain this instance implies that j can explain it as well. To axiomatize these two cases, new axioms and techniques will emerge. Further, we can also add an operator that expresses knowledge about other agents' function domain.
Computationally, we see without too much surprise that the finite model property holds. For all the three single agent cases with a finite language, the required size of G and the size of the model constructed can be explicitly computed. In the multiagent case, a standard filtration method can also be applied quite straightforwardly. Notice that in each of the three cases, the completeness proof requires a minimal size of G. A natural question is whether we can bring down the size requirement by giving more economic completeness proofs. In particular, the double exponential size requirement in the single agent fixed intermediate function domain case seems to be too large, while the number of value assignments seems too small (just 2). We might be able to implement a trade-off here or a smarter lattice construction.
In summary, introducing knowledge about functional dependency relations brings us ample new opportunities to extend the border of epistemic logic. There will be a lot more to achieve.