Midlands Logic Seminar

Week 4: 25 October

Study group: Richard Kaye (Birmingham)

The KKL theory of truth examines the status of Tarski's inductive definition of truth, for nonstandard formulas of the language of arithmetic relative to some model of PA. There are a number of surprises and some common pitfalls. This talk will be an overview, explaining the approach and giving background and stating the main results, without proofs of the key theorems.

Invited speaker: Michael Gabbay (Kings)
"A proof theoretic basis for computation"

I present a proof theory for untyped lambda calculus satisfying cut-elimination. Mathematically the cut-elimination result suggests an interesting extension, and perhaps even replacement, for the familiar language of the lambda calculus. Also a new(ish) denotational model theory for lambda terms becomes apparent. Philosophically, I argue that untyped lambda calculus (or a suitable extension of it) can serve as the logic of computation.