next up previous contents
Next: Knowledge and complexity Up: Reasoning about algorithmic knowledge Previous: Axioms for algorithmic knowledge   Contents

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.

\par The logic \textbf{K$_N^A$} consists of the following axi...
...\alpha$\ to infer $K_i^{\exists}\alpha$\par\end{description}\par\end{definition}

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.

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

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

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

$\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$.

\par\textbf{S5$_N^A$} and its subsystems are consistent.

\par We map formulae of the language $\mathcal{L}_{N}^{AK}$\ to
...ontradiction like $\alpha\land \lnot
\alpha$\ cannot be derived.

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.

\par The following rules of inference are valid for \textbf{K$_N^A...
... \alpha \leftrightarrow K_i^{\exists} \beta$\par\end{description}\par\end{lemma}

\par The rule \textbf{(CGR$^A$)} is a trivial consequence of
...lpha \to K_i^{\exists} \beta$can be inferred using modus ponens.

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.

\par Let the translation function $tr: \mathcal{L}_{N}^{K} \maps...
...5_N} \alpha$\ iff $\vdash_{KD45^A_N} tr(\alpha)$\end{enumerate}\par\end{theorem}

% latex2html id marker 4043See appendix \ref{app:proof}.

If $\avec{\alpha}{\land}{n} \to \beta$\ is provable then so ar...
...a$\ and
$\avec{K_i^{0}\alpha}{\land}{n} \to K_i^{\exists}\beta$.

next up previous contents
Next: Knowledge and complexity Up: Reasoning about algorithmic knowledge Previous: Axioms for algorithmic knowledge   Contents