2nd Semester 2006/07: Translating Between Logics

Instructors

Theo Janssen
If you are interested in this project, please contact Theo by e-mail.

ECTS

6

Description

There are several translations between logics, e.g. between modal logic and predicate logic, and between classical logic and intuitionistic logic. A surprising example of a translation is given by Béziau (1999). He considers PL/2 which is propositional logic (PL) with only one half of the meaning of negation, and provides a translation from PL into the seemingly weaker logic PL.

One might ask when a translation between logics is a correct translation, and under which circumstances such a translation is possible at all. A general perspective on this issue is given in Carnielli & d'Ottaviano (1997) and Feitosa & d'Ottaviano (2001). A reaction on this is Janssen (2007). The proposals in these papers are of algebraic nature. One might expect that a correct translation from a logic that makes fine distinctions into a logic that makes few distinctions is not possible (because in the translation essential information is lost). But it is reasonable to expect that a translation from a logic that makes few distinctions (propositional logic) into a logic with finer distinctions (intuitionistic propositional logic) is possible (the G�del translation).

Problem. (Humberstone 2005) gives a counterexample to the intuitive result mentioned above. One of the involved logics is KT, which is the basic normal logic K extended with BoxA implies A. The other is the minimal modal logic L. He shows that there is no translation (satisfying certain requirements) from KL into L, whereas on intuitive considerations one would expect this to be easy.

Task.

1. Humberstone (2005, sect. 5) is rather a sketch, and uses some results I did not know. Give a proof in which all details are filled in.
2. His proof assumes a rather restrictive notion of what a translation would be, stricter than in Carnielli & d'�Ottaviano (1997) and Janssen (2007). I expect that without Humberstone�s restrictions, a translation is possible. Find one.

References

• Béziau, J-Y (1999), �Classical negation can be expressed by one of its halves�, Logic Journal of the IGPL 7(2), 145-151.
• Carnielli, W.A. & d'�Ottaviano, I.M.L. (1997), �Translations between logical systems: A manifesto�, Logique et Analyse 15, 67-82.
• Feitosa, H.A. & d'�Ottaviano, I.M. L. (2001), �Conservative translations�, Annals of Pure and Applied Logic 108, 205-227.
• Humberstone, L. (2005), �éziau�s translation paradox�, Theoria 71, 138-181.
• Janssen, T. M. V. (2007), Compiler correctness and the translation between logics., to appear as ILLC preprint.