A framework for the transfer of proofs, lemmas and strategies from classical to non classical logics (Q687153)

Proofs in non-classical logics, in particular in modal logics, can be found by operating on the original syntax, or by translating the formulae into predicate logic and proving the translated theorem with a predicate logic theorem prover. Translating the proofs of the translated theorem back into the original syntax, however, is non-trivial and sometimes impossible. In this paper the backwards translation of proofs into the syntax of propositional modal logic is investigated. Two cases are considered. In the first propositional modal logic S5 is treated. The semantics of the S5 \(\square\)-operator, \(\square p\) is true in a world iff \(p\) is true everywhere, is turned into the translation rule from modal into predicate logic: `\(\square p\to \forall x p(x)\)'. It turns out that in this case there is a one-to-one correspondence between derivable translated formulae and derivable original S5 formulae. Therefore proofs found in predicate logic can be completely translated back into S5. In the second case the `functional' translation of the propositional modal systems S4, K, T and K4 is investigated. In the functional translation, a `functional semantics' of the \(\square\)-operator is used: \(\square p\) is true in a world iff \(p\) is true in all worlds computed by a set of `accessibility functions'. This is turned into a corresponding translation rule, where sequences of existentially or universally quantified variables correspond to the nesting of Box and Diamond operators. Derivations of the so translated formulae may instantiate these variables in such a way that there is no corresponding modal formula. Therefore the translation back function as presented in the paper is only partial. A proof found with the translated formulae is translated back into a sequence of modal formulae which has some gaps. These back translated formulae can be taken as lemmas, and the whole proof can be reconstructed by proving the lemmas with a calculus operating on the original syntax.