Logics of algorithmic knowledge

The basic logic of algorithmic knowledge with agents will be
called **K**. It is specified by the following axioms and
rules of inference.

The definition of **K** calls for some explanation and
comment. Axiom **(K)** and rule **(NEC)** correspond
to the familiar modal postulates. However, the intended interpretation
of the operator is now different: unlike the necessity
operator of modal logic, which has an universal flavor (``true
in all possible worlds''), the operator 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)** and
**(Q)** characterize the operators for natural
numbers . By means of **(Q)**, formulae like
(``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 because nothing can be assumed to be
(explicitly) known a priori. However, for certain formulae a
number can be determined such that 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)**-
(Truth axiom)
**(D)**-
(Consistency axiom)
**(4)**-
(Positive introspection axiom)
**(5)**-
(Negative introspection axiom)

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

Obviously, **K** 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
is consistent with
**K**, i.e., **K** 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 unit
of time) needs not be closed under logical consequences or even under
any logical law, e.g.,
is perfectly
**K**-consistent. Moreover,
can also be seen to be consistent
for any . On the other hand, many closure properties hold for the
notion of implicit knowledge. For example,
is provable in
**K**. 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 to a formula of and show that provability is preserved.