Implementing Frege in the style of Quine: the Gottlob Proof System

This is first introduced as of 8/19/2018.

Here I present a concrete implementation of the program suggested by my notes on Frege which have appeared on my web page for some time: Here find an outline of how to fix the foundational system of Frege using stratification in the style of Quine. Here find another approach to the same subject. It is important to note that the idea of repairing Frege's system by imposing stratification was first proposed by Nino Cocchiarella, though the details of what we do here are entirely our own.

Here find the documentation and here the Moscow ML 2.01 source for the Gottlob theorem prover. As an exercise in literate programming, the source differs by one character from the LaTeX source for the documentation (in which the source appears in full as verbatim blocks).

Here find the commands implementing as much of Frege's book as I have processed so far. Here is the same development in the form of a much more informative log file generated by Gottlob.