The Jowett Society (Friday - Week 5, MT20)

Philosophical Society

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.


Join Zoom Meeting

Meeting ID: 983 1616 2905

Passcode: 607477

Jowett Society Organising Committee: Sophie Nagler | Jowett Society Website