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.

This is Barzilay's preferred notation. There is
an alternative
.