ElisTarskiPf B Sections NuprlLIB Doc

ElisTarskiPf_B
Nuprl Section: ElisTarskiPf_B - Eli Barzilay's formalization of Tarski's unrepresentability of Truth

These are the definitons, theorems and unproved assumptions (FIATS) developed by Eli Barzilay for his proof of Tarski's result. He also has added some primitive rules not shown here (see below), especially regarding computation rules.

This Formalization was based on an informal proof .

There are postscript listings of the formal objects as well:

Short listing with thm statements but no proofs.

Long listing with proofs.

Listing of Rules and FIATS.

There is a parallel set of pages using Barzilay's preferred notation .

ElisTarskiPf B Sections NuprlLIB Doc