We prove the first correspondence. That is, we shall show that
is K
-provable if and only if
is
K
-provable. The other results are obtained in the same
way.
First, we show that the translation of every K-theorem is
a K
-theorem. Let
be a theorem of
K
. We show inductively over the length of the proof of
in K
that
is a theorem of
K
.
Assume that is one of K
-axioms, i.e., it
is either a propositional tautology or an instance of the schema
K. In the former case
is also a propositional
tautology, and in the latter case
is an instance of
(K
), so in any case
is a
K
-theorem.
Now suppose that has been derived by applying modus ponens to
and
. By induction hypothesis, both
and
are
K
-theorems. By definition,
is
, so in K
we can apply modus
ponens to infer
.
Finally, suppose that has been derived from
using the
knowledge necessitation rule (NEC), i.e.,
is
and
is a K
-theorem. Then
is a theorem of K
, by induction hypothesis. According
to the definition of
,
is
, which can be derived from the theorem
by
applying the rule (NEC
). Hence,
is a
K
-theorem.
To prove the converse, we define the inverse function
of
as follows:
It is easy to see that
for all
. However, the converse does not hold:
generally
and
are different
formulae. For instance,
.
Assume that is provable in K
. Then there
is a K
-proof leading to
, i.e., there is a
sequence
of K
-formulae such
that
is
and each
(
) is
either an axiom of K
or is derived from previous
formulae in the sequence using one of the inference rules. We show
that the sequence
is a
proof of
in K
.
Suppose that is axiom of K
. If
is a
propositional tautology then so is
. If
is
an instance of (K
) then
is an instance
of (K). If
is an instance of (P
) or
(Q
) then
is a propositional tautology.
Suppose that is derived from
and
by modus ponens. Then
and
are K
-theorems, so
can
be inferred from
and
(which is by definition the same formula as
.)
Finally, let be derived from
by applying
(NEC
). Then
is
, hence
is
, which can be derived from
using (NEC).
Thus, in any case
is a theorem of
K
. As observed earlier,
. So
is a theorem of
K
. This completes the proof.