Personal tools
You are here: Home Events Abstract Archives 1997 Classical Brouwer-Heyting-Kolmogorov interpretation

Classical Brouwer-Heyting-Kolmogorov interpretation

Masahiko Sato (Univ. of Kyoto, Japan) LFCS Theory Seminar Room 2511, JCMB, King's Buildings 3pm, Thursday 20th November 1997

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.

Document Actions