Knowledge’s acquisition happens
time. However, this feature is not reflected in the standard epistemic logics, e.g.
with its possible world semantics suggested by Hintikka in , and hence their applications are limited. In this paper we adapt these normal modal logics to increase their expressive power such that not only is
is known modeled but also
it is known is recorded. We supplement each world with an awareness function which is an augmentation of Fagin-Halpern’s to keep track of the time when each formula is to be derived. This provides a new response to the logical omniscience problem. Our work originates from the tradition of study of
, also known as
Logic of Proofs
, introduced by Artemov (,,). We will give the axiom systems of the models built here, accompanied with soundness and completeness results.