Landau, Grundlagen der Analysis, Alternate Formal Versions

Below are links to different formal developments corresponding to Jutting's Automath encoding of Landau's Grundlagen der Analysis. A tar file containing the Automath files and tex files is available here.

Simply Typed Version

In 2005, I (Chad) wrote lisp code to parse the Automath version in order to port the encoding. Using this, I automatically generated alternative Automath versions, including an Automath version without implicit arguments, where contexts are always freshly declared, there is only one big paragraaf and dependencies on arguments are reduced . I once had HTML pages giving the details of the simply typed version online, but the files are huge. If you want to see these details, please download this (1M) gzip'd tar file. It will expand into a (23M) directory called landau-tps which will contain HTML files. Start by having your browser view landau-tps/landau-tps.html. To get an idea of how the details look, click here.

HOTPTP Version

There is now a version of the original Automath encoding in the hotptp format. Click here for the gzipped file. A corresponding Automath version is here (gzipped).

Simply Typed Version in Detail

I also translated the Automath code into simply-typed lambda-terms as abbreviations. This page provides access to this simply-typed version. The syntax corresponds TPS in GENERIC mode. In principle, one should be able to copy formulas from this page and paste them directly into TPS.

Proof terms were not translated. Any dependence on proof terms was translated away. In particular, all theorems were translated without proof. One reason I made the translation was as a challenge to systems such as Omega and TPS. In these systems, one should be able to reconstruct the proofs interactively, automatically or in a mixture of these modes.

Automath types were translated as partial equivalence relations (pers) over simple types. Certain abbreviations for pers are used.

I assumed the base type I satisfies the Peano Axioms. I also assumed the existence of two basic constants _1 of type I and _SUC of type (II). The Automath type _NAT corresponds to the type I (or technically, as a per, the equality relation on I).

The only axioms after translation are description (at every type) and the Peano Axioms at type (I). The particular version of description is given by _ONEAX. The Peano Axioms are _AX3, _AX4, and _AX5 (induction, not to be confused with the theorem _INDUCTION). Interestingly, we do not need an axiom of choice, axiom of Boolean extensionality or axioms of functional extensionality. The Automath encoding does not use axioms of choice or Boolean extensionality. The Automath encoding DOES use axioms of functional extensionality (see _FISI) which translates into a theorem since we interpret function types as function pers, which are extensional even if the underlying function types are not extensional.

IF the translation is correct, THEN each theorem should be provable using only description and the Peano Axioms.

Slides from my talk at ESHOL, December 2005.

The TPS version of Landau in a proposed HOTPTP format.