Editing Common knowledge (logic) (section)

== Formalization ==
{{Unreferenced section|date=March 2022}}

=== Modal logic (syntactic characterization) ===

Common knowledge can be given a logical definition in [[Multimodal logic|multi-modal logic]] systems in which the modal operators are interpreted [[epistemic logic|epistemically]]. At the propositional level, such systems are extensions of [[propositional logic]]. The extension consists of the introduction of a group ''G'' of ''agents'', and of ''n'' modal operators ''K<sub>i</sub>'' (with ''i'' = 1,&nbsp;...,&nbsp;''n'') with the intended meaning that "agent ''i'' knows." Thus ''K<sub>i</sub> <math>\varphi</math>'' (where <math>\varphi</math> is a formula of the logical calculus) is read "agent ''i'' knows <math>\varphi</math>." We can define an operator ''E<sub>G</sub>'' with the intended meaning of "everyone in group ''G'' knows" by defining it with the axiom

: <math>E_G \varphi \Leftrightarrow \bigwedge_{i \in G} K_i \varphi,</math>

By abbreviating the expression <math>E_GE_G^{n-1} \varphi</math> with <math>E_G^n \varphi</math>  and defining <math>E_G^0 \varphi = \varphi</math>, common knowledge could then be defined with the axiom

: <math>C \varphi \Leftrightarrow \bigwedge_{i = 0}^\infty E^i \varphi</math>

There is, however, a complication. The languages of epistemic logic are usually ''finitary'', whereas the [[axiom]] above defines common knowledge as an infinite conjunction of formulas, hence not a [[well-formed formula]] of the language. To overcome this difficulty, a ''fixed-point'' definition of common knowledge can be given. Intuitively, common knowledge is thought of as the fixed point of the "equation" <math>C_G \varphi=[\varphi\wedge E_G (C_G \varphi)]=E_G^{\aleph_0} \varphi</math>. Here, <math>\aleph_0</math> is the [[Aleph-naught]]. In this way, it is possible to find a formula <math>\psi</math> implying <math>E_G (\varphi \wedge C_G \varphi)</math> from which, in the limit, we can infer common knowledge of <math>\varphi</math>.

From this definition it can be seen that if <math>E_G \varphi</math> is common knowledge, then <math>\varphi</math> is also common knowledge (<math>C_G E_G \varphi \Rightarrow C_G \varphi</math>).

This ''syntactic'' characterization is given semantic content through so-called ''[[Kripke structure (model checking)|Kripke structures]]''. A Kripke structure is given by a set of states (or possible worlds) ''S'', ''n'' ''accessibility relations'' <math>R_1,\dots,R_n</math>, defined on <math>S \times S</math>, intuitively representing what states agent ''i'' considers possible from any given state, and a valuation function <math>\pi</math> assigning a [[truth value]], in each state, to each primitive proposition in the language. The [[Kripke semantics]] for the knowledge operator is given by stipulating that <math>K_i \varphi</math> is true at state ''s'' iff <math>\varphi</math> is true at ''all'' states ''t'' such that <math>(s,t) \in R_i</math>. The semantics for the common knowledge operator, then, is given by taking, for each group of agents ''G'', the [[reflexive closure|reflexive]] (modal axiom '''T''') and [[transitive closure]] (modal axiom '''4''') of the <math>R_i</math>, for all agents ''i'' in ''G'', call such a relation <math>R_G</math>, and stipulating that <math>C_G \varphi</math> is true at state ''s'' iff <math>\varphi</math> is true at ''all'' states ''t'' such that <math>(s,t) \in R_G</math>.

=== Set theoretic (semantic characterization) ===

Alternatively (yet equivalently) common knowledge can be formalized using [[set theory]] (this was the path taken by the Nobel laureate [[Robert Aumann]] in his seminal 1976 paper).  Starting with a set of states ''S''.  An event ''E'' can then be defined as a subset of the set of states ''S''.  For each agent ''i'', define a [[Partition of a set|partition]] on ''S'', ''P<sub>i</sub>''.  This partition represents the state of knowledge of an agent in a state.  Intuitively, if two states ''s''<sub>''1''</sub> and ''s''<sub>''2''</sub> are elements of the same part of partition of an agent, it means that ''s''<sub>''1''</sub> and ''s''<sub>''2''</sub> are indistinguishable to that agent. In general, in state ''s'', agent ''i'' knows that one of the states in ''P''<sub>''i''</sub>(''s'') obtains, but not which one. (Here ''P''<sub>''i''</sub>(''s'') denotes the unique element of ''P<sub>i</sub>'' containing ''s''. This model excludes cases in which agents know things that are not true.)

A knowledge function ''K'' can now be defined in the following way:

<math block>K_i(e) = \{ s \in S \mid P_i(s) \subset e\}</math>

That is, ''K''<sub>''i''</sub>(''e'') is the set of states where the agent will know that event ''e'' obtains. It is a subset of ''e''.

Similar to the modal logic formulation above,  an operator for the idea that "everyone knows can be defined as ''e''".

<math block>E(e) = \bigcap_i K_i(e)</math>

As with the modal operator, we will iterate the ''E'' function, <math>E^1(e) = E(e)</math> and <math>E^{n+1}(e) = E(E^{n}(e))</math>.  Using this we can then define a common knowledge function,

<math block>C(e) = \bigcap_{n=1}^{\infty} E^n(e).</math>

The equivalence with the syntactic approach sketched above can easily be seen: consider an Aumann structure as the one just defined. We can define a correspondent Kripke structure by taking the same space ''S'', accessibility relations <math>R_i</math> that define the equivalence classes corresponding to the partitions <math>P_i</math>, and a valuation function such that it yields value ''true'' to the primitive proposition ''p'' in all and only the states ''s'' such that <math>s \in E^p</math>, where <math>E^p</math> is the event of the Aumann structure corresponding to the primitive proposition ''p''. It is not difficult to see that the common knowledge accessibility function <math>R_G</math> defined in the previous section corresponds to the finest common coarsening of the partitions <math>P_i</math> for all <math>i \in G</math>, which is the finitary characterization of common knowledge also given by Aumann in the 1976 article.