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

The gentlemen in question...

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.

For the log file shown to be visually informative, you need to be using UTF-8 encoding and ideally a constant width font (achievable in Notepad and in common browsers). The script files produced directly by Gottlob use code page 437 (Western European/OEM-US in Notepad++ encoding list) and cannot be read successfully in Notepad (they still work as scripts: the visual issues occur in ML comments).