Katalin Bimbo (Alberta) — The development and applications of the Curry–Kripke proof technique
The mid 1930s produced a negative solution (by Church and Turing) to the decidability problem of Hilbert. However, a year earlier propositional intuitionistic logic was shown decidable (by Gentzen), which was known not to be finitely valued by then (due to a result of Gödel). This talk deals with decidability (in the syntactic sense) and focuses on proofs that utilize a sequent calculus — starting with Gentzen’s proof for (propositional) J.
I will illustrate the main ideas and lemmas that comprise the Curry–Kripke technique. On the way, I will also mention decidability proofs by Lambek and Kleene. The Curry–Kripke method allowed to prove the decidability of important logics from among the so-called non-classical logics, such as S4-> and R->. It turns out that using relationships between logics, a couple of more logics are amenable to be handled by this method.
