LFCS Theory Seminar
Room 2511, JCMB, King's Buildings
3pm, Thursday 20th November 1997

(* NOTE NONSTANDARD DAY AND TIME *)

Title: Classical Brouwer-Heyting-Kolmogorov interpretation

Speaker: Masahiko Sato (Univ. of Kyoto, Japan)

We give an interpretation for first order Peano arithmetic where each formal proof in the theory is interpreted by an abstract proof. We also show that any formula of the theory is true in the sense of Tarski iff it has an abstract proof. These abstract proofs are obtained by giving a classical version of BHK interpretation.