Next: Bibliography Up: Formal Proofs Previous: Theorem 22   Contents

Theorem 28

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:

• for all

• , for all

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.

Next: Bibliography Up: Formal Proofs Previous: Theorem 22   Contents
2001-04-05