Report Number: CS-TR-74-467
Institution: Stanford University, Department of Computer Science
Title: Checking proofs in the metamathematics of first order logic.
Author: Aiello, Mario
Author: Weyhrauch, Richard W.
Date: August 1974
Abstract: This is a report on some of the first experiments of any size
carried out using the new first order proof checker FOL. We
present two different first order axiomatizations of the
metamathematics of the logic which FOL itself checks and show
several proofs using each one. The difference between the
axiomatizations is that one defines the metamathematics in a
many sorted logic, the other does not.