BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-74-467
       ENTRY:: August 23, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Checking proofs in the metamathematics of first order logic.
        TYPE:: Technical Report
      AUTHOR:: Aiello, Mario
      AUTHOR:: Weyhrauch, Richard W.
        DATE:: August 1974
       PAGES:: 60
    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.
       NOTES:: [Adminitrivia V1/Prg/19950823]
         END:: STAN//CS-TR-74-467