Checking Proofs in the Metamathematics of First Order Logic

Aiello, Mario; Weyhrauch, Richard W.

Checking Proofs in the Metamathematics of First Order Logic

Download BibTeX Cite

Proceedings of the Fourth International Joint Conference on Artificial Intelligence. Mathematical and Theoretical Aspects of A.I. Pages 1-7.

Abstract

First order Llteoril' s not only ca n ht• used in proving properti,•s of programs, but have <Jlso rclevance in representation theory. The desire to represent first order theories in a computer in a feasible way requires the facility to discuss meta mathematical notions. Using metamath e matics willeventually allow to construct systems which can form<Jlly discuss how they reason. In thi s paper we present twu different first order axiomatizations of the metamathematics of the logic which FOI. (First Ordc•r Logic proof checker) checks and show sevt·ral proofs using each one. The difference betwl'en the axiomatizations is that one defines the metamathematics in a raany sorted logi c and the otlwr docs not. Proofs arc then compared and used to discuss the adequacy of sorae FOL features.

Mario Aiello, and Richard W. Weyhrauch. 1975. Checking Proofs in the Metamathematics of First Order Logic. In Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75. IJCAI, 1–7. https://ijcai.org/proceedings/1975/1

@inproceedings{ijcai1975p1,
  title     = {Checking Proofs in the Metamathematics of First Order Logic},
  author    = {Aiello, Mario and Weyhrauch, Richard W.},
  booktitle = {Proceedings of the Fourth International Joint Conference on
               Artificial Intelligence, {IJCAI-75}},
  publisher = {International Joint Conferences on Artificial Intelligence},
  editor    = {Patrick Winston and Carl Hewitt},
  pages     = {1--7},
  year      = {1975},
  note      = {Mathematical and Theoretical Aspects of A.I},
  url       = {https://ijcai.org/proceedings/1975/1},
}

TY  - CPAPER
TI  - Checking Proofs in the Metamathematics of First Order Logic
AU  - Aiello, Mario
AU  - Weyhrauch, Richard W.
T2  - Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75
PB  - International Joint Conferences on Artificial Intelligence
PY  - 1975
SP  - 1
EP  - 7
UR  - https://ijcai.org/proceedings/1975/1
ER  -