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.
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.
The Midlands Logic Seminar was founded in 2011 and aims to cover all areas of mathematical logic, as well as related areas of theoretical computer science, and philosophy of mathematics. We typically have a study group session from 4:00-5:00 (term 1 topic: satisfcation classes) and a research talk from 5:00-6:00.
Dr Walter Dean
Department of Philosophy
University of Warwick