This page provides resources related to a current little project of mine, whose motivation is actually philosophical. I have in mind a view of the philosophy of mathematics under which the objects of classical, nonconstructive, impredicative mathematics with higher orders of infinity are naturally accessible by finitary means, all the infinities being merely potential. This view exploits the Curry Howard isomorphism and some thoughts of mine about the nature of abstraction, and if it is to be taken seriously should be implementable on a computer. The implementation (given the intellectual ingredients I have mentioned) should resemble Automath. And it does.

An implementation is now found here with documentation and examples.

The name is admittedly a bit of mischief: I am Holmes, I already have a prover called Watson, and my son suggested that I call this one Lestrade...

Here is the source for the implementation in Moscow ML 2.01 of the Lestrade Type Inspector. The version date is shown in the files. As of 10/14/2017 this differs by one character from a LaTex document here (literate programming attempted): the idea is that I can maintain a readably commented source in this way.

I no longer support multiple versions. It is useful to be aware that after July 2019 what was the `construct` command is now the `postulate` command and `rewritec` has become `rewritep`. Those two string replaces will likely fix any old files. Most if perhaps not all of the Lestrade source files on this page have been edited and tested with the current version and should run. I might have missed one or two.

There have been significant updates to display and file handling during the development of the Zermelo implementation.

The files which follow embody the largest Lestrade implementation project, now underway (summer 2019). I am implementing Zermelo's 1908 papers on axiomatization of set theory and proof of the well-ordering theorem.

- Here are the logical preliminaries.
- Here is the axiomatics of 1908 Zermelo set theory, anachronistically provided with a proof of the basic property of the Kuratowski pair (but this is not used in our quite faithful implementation of the 1908 well ordering theorem proof).
- Here are opening definitions and results in the well-ordering theorem proof.
- Here is the proof of the central result, essentially that the theta-chain of interest is totally ordered. This file is very large and runs slowly.
- Here are consequences of the big result of file 4; I expect this file to eventually contain the final result. I am still working on it. The sheer size of file 4 forced me to perfect the ability to load and develop files incrementally (Lestrade already had some support for this, but it was awkward and limited; it is improved, of necessity).

Here is a paper I was working on in fall 2017, simultaneously an account of Lestrade and a treatment of foundational topics; it is another pass at the aims of the paper just below, and discusses new additions to the capabilities of Lestrade.

Here is a paper I was working on in summer 2017, simultaneously an account of Lestrade and a treatment of foundational topics.

Here is another paper I was working on in summer 2016, focussed more narrowly on the philosophical approach.

Here is an old manual (which I updated for a while but which doesn't have the latest changes; it does not say everything that the paper designated as the manual above says, but it has a different emphasis and I think it might still be useful).

Here are the slides (slightly improved) for the talk I gave to the Boise State logic seminar Oct 24 2017. Here is an older set of slides (misleadingly also dated Oct 24 due to the date function of LaTeX).

Here are the slides for a talk I am giving locally on October 25th 2016. Here is the supporting Lestrade script file.

Here is my scratch work as I read through Mike Nahas's Coq tutorial and proved analogous things under Lestrade.

Here is a paper I am working on in fall 2017, outlining implementation of homotopy type theory under Lestrade. I'm not finished with this by any means, it is rather tricky.

Here is an axiomatization of ZFC in Lestrade. Not of much interest until I prove something with it!

Here
is a paper I am working on in fall 2017, exhibiting the rewriting
capabilities, and the ability to use rewrite rules provably valid in a
theory to implement programming behavior: the file is intended to
support computation of Fibonacci numbers (thus the name) but at the
moment supports a fully implemented adder for binary numerals on top of a
simple theory of arithmetic: all of its computations are theorems.
The `rewrited` command, not witnessed so far in other files, is used extensively in this one.

And here is another paper I am working on in fall 2016, which pretends to be an initial segment of an elementary discrete math test supported by Lestrade text.

Here is the source for the implementation in Moscow ML 2.01 of a reimplementation of the Lestrade Type Inspector.

Here is the source as a PDF, demonstrating my devotion to literate programming.

Here is the directory containing output files for the new version. The new version has the same input language (except that it does not support rewriting) but a quite different file format. There is a utility for exporting files from the first version, and files from the first version which do not use rewriting can now reliably be revised to run under the second version: all the files for the proof of the well-ordering theorem have been converted, as have the examples embedded in my large papers. There are some differences in the parser and in move saving and implicit argument inference which require occasional changes.

Here are the converted versions of the files for Zermelo's 1908 papers on axiomatization of set theory and proof of the well-ordering theorem.

- Here are the logical preliminaries.
- Here is the axiomatics of 1908 Zermelo set theory, anachronistically provided with a proof of the basic property of the Kuratowski pair (but this is not used in our quite faithful implementation of the 1908 well ordering theorem proof).
- Here are opening definitions and results in the well-ordering theorem proof.
- Here and here is the proof of the central result, essentially that the theta-chain of interest is totally ordered. This file is very large and runs slowly.
- Here and here are consequences of the big result of file 4; I expect this file to eventually contain the final result. I am still working on it. The sheer size of file 4 forced me to perfect the ability to load and develop files incrementally (Lestrade already had some support for this, but it was awkward and limited; it is improved, of necessity).

- russell.lti is a self-contained implementation of Russell's paradox. Needless to say, there are
**assumptions**which lead to the paradox; the logic of Automath itself is consistent. - landau_axioms.lti
is my ongoing implementation of Landau's Foundations of Analysis
(following in the footsteps of the original Automath project). I'm
currently in the middle of proposition 4. This is not a polished
production; I am hacking as I go. It will get cleaned up later! [This
is a stalled project from summer 2015, but I have made a little progress
on it recently].
- landau2
.lti More Landau stuff.
- summer2016book.lti is a new set of declarations I am working on in summer 2016. This includes general logic and now basic declarations for natural numbers and the simple typed theory of sets.
- summer2016.ltxt is a new set of declarations I was working on in summer 2016, revised for the new 2020 version of Lestrade. This includes general logic and now basic declarations for natural numbers and the simple typed theory of sets.
- rewrites.lti is a new set of declarations I am working on in summer 2016. This is to be run with the new version of Lestrade with rewriting, and exhibits elementary examples of rewrite rule programming, similar in style to that found in Watson. I want to develop examples where rewrite rules are demonstrated on the basis of proofs rather than introduced by fiat, but the rewrite construction command is a perfectly reasonable way to introduce an equational axiom -- if one is willing for it always to be applied as a simplification.
- auto37.lti is another new summer 2016 file I am working on: I am translating file
37 in the Automath archive from Automath to Lestrade, which is quite instructive (for me at any rate).
- autoi37.lti is the auto37 translation as far as it goes, making full use of the implicit arguments feature.
- autoi37b.lti is the auto37 translation in another test version making more use of local declarations.
- newautoi37.pdf is the autoi37b translation in another test version making more use of local declarations, adapted to the new version of Lestrade, more conveniently viewed here
- implicittest.lti contains some examples of implicit argument inference.
- maclane.lti contains a set of declarations for Mac Lane set theory (somewhat modified). >maclanetest.lti has a few more test declarations I am working on which motivated recent upgrades of implicit argument inference.
- geometry.lti contains a set of declarations for Euclidean plane geometry (in a very preliminary state).
- discretemath.lti contains the declarations supporting the purported discrete math text.
- pocket.lti contains the basic declarations for "pocket set theory"; before reading it, you need to read discretemath, which it imports.
- logicpackage.lti
is a new logic file that I'm working on which is intended for use as a
module via the import command: once it is ready I'll try eliminating
logical preambles from some other files.

Here is Freek
Wiedijk's Automath site, including the only currently available
implementation of standard Automath (as far as I know). What I present
here is **not** standard Automath!

Here is the official Automath archive site.