Logics of algorithmic knowledge

The basic logic of algorithmic knowledge with $N$ agents will be called K$_N^A$. It is specified by the following axioms and rules of inference.

The definition of K$_N^A$ calls for some explanation and comment. Axiom (K$^A$) and rule (NEC$^A$) correspond to the familiar modal postulates. However, the intended interpretation of the operator $K_i^{\exists}$ is now different: unlike the necessity operator $\Box$ of modal logic, which has an universal flavor (``true in all possible worlds''), the operator $K_i^{\exists}$ has a rather existential flavor (``the computation eventually terminates with the correct answer''). Hence, our postulates must be justified in a different way. The axiom schemata (P$^A$) and (Q$^A$) characterize the operators $K_i^n\alpha$ for natural numbers $n$. By means of (Q$^A$), formulae like $K_i^0\alpha \land K_i^0(\alpha \to \beta) \to K_i^{\exists}\beta$ (``agents are able to compute consequences of their explicit knowledge'') can be proved and need not be postulated separately. We do not have any axiom of the form $K_i^0\alpha$ because nothing can be assumed to be (explicitly) known a priori. However, for certain formulae $\alpha$ a number $n>0$ can be determined such that $K_i^n\alpha$ may be assumed to be logically valid. We shall investigate such formulae later and use them to define more powerful logics of algorithmic knowledge.

Another way to enrich the basic system is to use postulates which capture additional properties of knowledge. We have discussed axioms which have often been used in the context of modal epistemic logic.

(T$^A$)

$K_i^{\exists} \alpha \to \alpha$ (Truth axiom)

(D$^A$)

$K_i^{\exists} \alpha \to \lnot K_i^{\exists} \lnot \alpha$ (Consistency axiom)

(4$^A$)

$K_i^{\exists} \alpha \to K_i^{\exists}K_i^{\exists} \alpha$ (Positive introspection axiom)

(5$^A$)

$\lnot K_i^{\exists} \alpha \to K_i^{\exists}\lnot K_i^{\exists} \alpha$ (Negative introspection axiom)

Adding suitable postulates from that list to the basic system will yield stronger logics of algorithmic knowledge. Those extensions of K$_N^A$ are named in the same manner as the modal systems in chapter 2. For example, S5$_N^A$ is the logic K$_N^A$ plus the axioms T$^A$, 4$^A$ and 5$^A$.

Obviously, K$_N^A$ solves all variants of the logical omniscience problem with respect to the explicit concept of knowledge. To see that, it suffices to observe that the set $\{\lnot K_i^0\alpha \vert \alpha\in \mathcal{L}_{N}^{AK}\}$ is consistent with K$_N^A$, i.e., K$_N^A$ can describe agents who (at some of their information states) know nothing explicitly. (However, they always know something implicitly.) Likewise, it is easy to see that what an agent explicitly knows (i.e., what he knows in $0$ unit of time) needs not be closed under logical consequences or even under any logical law, e.g., $K_i^0\alpha \land K_i^0(\alpha \to \beta) \land \lnot K_i^0\beta$ is perfectly K$_N^A$-consistent. Moreover, $K_i^n\alpha \land K_i^n(\alpha \to \beta) \land \lnot K_i^n\beta$ can also be seen to be consistent for any $n$. On the other hand, many closure properties hold for the notion of implicit knowledge. For example, $K_i^0\alpha \land K_i^0(\alpha \to \beta) \to K_i^{\exists}\beta$ is provable in K$_N^A$. In general, agents described by our logic are rational in the sense that they can draw all logical consequences of their knowledge if the necessary resources are available, as the following lemma shows.

The next theorem shows that the common systems of modal epistemic logic can be embedded into the corresponding systems of logic for algorithmic knowledge. For that purpose we map each formula of the language $\mathcal{L}_{N}^{K}$ to a formula of $\mathcal{L}_{N}^{AK}$ and show that provability is preserved.