Jan von Plato: Two Gödelian Topics in Modal Logic

ABSTRACT

I  The exact correspondence between intuitionistic and modal logic: Let A be a formula of intuitionistic logic and T(A) its modal translation in S4. It is shown that if T(A) is a theorem of S4, indirect proof is not needed in its proof. This conservativity result is based on normalization. A translation of normal derivations of T(A) in S4 to derivations of A in intuitionistic logic is immediate. II  Normal derivability in Gödel-Löb logic: Gigi Bellin  published  in 1985 a proof of normalization  for a system of natural deduction for the Gödel-Löb provability logic, but his very involved proof seems to have remained largely unread. A clear and simple proof of normalization is given, the crux of which is a conversion algorithm that reduces several instances of the modal rule with the same diagonal formula into one.

Speaker: Jan von Plato (University of Helsinki)

Jan has worked both in logic and its development, with three systematic books on proof theory. His work of a historical-foundational character includes two books, The Great Formal Machinery Works, and Saved from the Cellar. The latter is a collection of the shorthand writings on logic and foundations by Gödel’s contemporary Gerhard Gentzen.