### 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.

##### About the seminar

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.

##### Logistics

All meetings for Term 1 2013 will be Friday from 4:00-6:00 in room 310 of Watson Building (School of Mathematics) on the campus of the University of Birmingham.

campus map
google maps

To get to campus, take train from Birmingham New Street to the University stop (7 minutes).

##### Organizers:

Dr Richard Kaye

School of Mathematics

University of Birmingham

http://web.mat.bham.ac.uk/R.W.Kaye/

Dr Walter Dean

Department of Philosophy

University of Warwick

http://go.warwick.ac.uk/whdean