Accession Number:

ADA007562

Title:

Checking Proofs in the Metamathematics of First Order Logic

Descriptive Note:

Corporate Author:

STANFORD UNIV CA DEPT OF COMPUTER SCIENCE

Personal Author(s):

• Aiello, Mario
• Weyhrauch, Richard W.

Report Date:

1974-08-01

Pagination or Media Count:

58.0

Abstract:

This is a report on some of the first experiments of any size carried out using the new first order proof checker FOL. The authors 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.

Descriptors:

• *MATHEMATICAL LOGIC
• SET THEORY
• SYNTAX
• THEOREMS

Subject Categories:

• Theoretical Mathematics

Distribution Statement:

APPROVED FOR PUBLIC RELEASE