Let us consider an inference rule, say . It can be a valid inference rule of classical logic, or some other (non-classical) logic, for example, intuitionistic logic, conditional logic or relevant logic. Assume that an agent accepts as valid and he can use . What does it mean? In the modal approach we formalize this idea by an axiom saying that the knowledge set of the agent is closed under this rule, that is, if all premises of the rule are known then the conclusion of is also known. However, as we noted before, it is only true of implicit knowledge. In the context of explicit knowledge it must mean something different. It means rather that, if the agent knows all premises of the rule, and if he perform the inference according to the rule , then he will know the conclusion. The agent does not know the conclusion automatically, but rather as the result of some action, viz. the (mental) action of performing the corresponding inference. If he does not perform this action, then we cannot require him to know the conclusion, although this conclusion may seem to be an obvious consequences of the sentences under consideration.

The same line of argumentation applies to logical axioms, which can be viewed as inference rules without any premises. We cannot require an agent to know all axioms automatically and permanently, he must rather carry out some action before he can acquire knowledge of a certain axiom. Gaining knowledge of other, less obvious theorems is even harder: agents usually need to perform more complex computations in order to establish a theorem. Thus, it is possible that the agent knows all logical truths, but merely in principle. This knowledge is only implicit. In reality he never knows them all at once explicitly.

For formalizing the reasoning actions it is natural to use (a form of)
dynamic logic ([Har84], [Gol87], [KT90]; see
also appendix A for a brief overview.) We can add a set
of basic actions to the language of epistemic logic. The set of
formulae now includes formulae like
or
with the intended meaning: ``always after using
rule (or sometimes after using ) the agent knows
''. The formalization of the idea that an agent accepts and is
able to use an inference rule is straightforward. For example, the
idea that the agent accepts modus ponens can be formalized by the
axiom:
. This axiom says no more than if agent knows
and he also knows that implies , then after a suitable
inference step he will know .^{4.1}

As the axioms can be viewed as special inference rules we can
introduce an action corresponding to each agent and each axiom of the
basis logic, which describes the ability of the agent to use this
axiom in his reasoning. (In general, different agents may have
different logics, so that the sets of basic actions are different for
different agents. However, we assume a set of homogeneous agents, for
the sake of simplicity.) By means of the familiar program connectives
for dynamic logic (such as composition or iteration) we can formalize
the idea that the agent may know the consequences of some sentence
which he already knows explicitly, provided that he performs the right
reasoning steps. For example, assume that the agent knows the
conjunction of and
, that is,
. In all normal modal systems we
can deduce
. However, this inference is not
sound for actual knowledge of realistic agents. There is no guarantee
that the agent will know
automatically, as the
modal approach suggests. We can only say that *if* the agent
reasons correctly, *then* he will know
. In our
concrete case, let be the conjunction elimination rule, the
conjunction introduction rule, and modus ponens, respectively, and let
the symbol ``;'' denote the composition of actions. Then our theorem
must be:
, and not
as in
the standard modal approach.

In general, suppose that follows from in some basis logic (which is accepted by the agent) and that the agent knows . For explicit knowledge we cannot assume that the agent automatically knows . Let a proof of from be given, where the axioms and inference rules used in the proof are ,..., (in this order, where the same axiom or inference rule may occur at different places in the sequence.) Then, instead of the monotonicity rule in the standard modal approach we have the axiom: , where is 's reasoning action of applying the inference rule (). This axiom says that if the agent performs the sequence of actions corresponding to the rules (in this order) then he will know under the given circumstances. Whether or not the agent can come to this conclusion depends crucially on his logical ability. In this way we see that the logical omniscience problem can be solved easily in a natural way: we can describe agents whose knowledge may or may not be closed under logical laws. On the other hand we can still say that the agent thinks rationally, that he is not logically ignorant. Theoretically he may produce all logical truths, and all logical consequences of his knowledge, but only if he is interested in doing so, if he has enough time and memory, et cetera.

In the above argumentation we have made an implicit assumption. We have assumed that all premises, once known by the agent, are still available after the agent performs a reasoning step. In the previous example, if the agent forgets the premise immediately after using modus ponens, then he cannot apply the conjunction introduction rule to come to the conclusion . Thus, we have to postulate that the agent does not forget what he previously knows after performing some reasoning action. This assumption can be formalized using persistence axioms for knowledge, for example, .

Are such persistence axioms reasonable? Only under two conditions. First, the truth value of should not change over time. If becomes false after 's inference using rule then it is not reasonable to postulate that still knows after the use of . This point should be taken into account when we formally define the language of our logic. In particular, if our language contains temporal indexicals then sentences containing them cannot be regarded as persistent. Second, the truth value of may not change through the agent's actions. This excludes formulae such that : it is possible that agent does not know now, but will know it as a result of his reasoning. In general, a formula in which a knowledge operator occurs essentially negative (i.e., within the scope of an odd number of the negation sign) is not a suitable candidate for a persistent one. So, we may assume that persistent formulae are built up from objective formulae using conjunction, disjunction, and the knowledge operators only.