ML Anthology

Checking Proofs in the Metamathematics of First Order Logic

Mario Aiello, Richard W. Weyhrauch
IJCAI 1975 pp. 1-8
doi:10.21236/ada007562 /ijcai/1975/aiello1975ijcai-checking/

Abstract

First order theories not only can be used in proving properties of programs, but have also relevance 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 metamathematics will-eventually allow to construct systems which can formally discuss how they reason. In this paper we present two different first order axiomatizations of the metamathematics of the logic which POL (First Order Logic proof checker) checks and show several proofs using each one. The difference between the axiomatizations is that one defines the metamathematics in a many sorted logic and the other does not. Proofs are then compared and used to discuss the adequacy of some FOL features.

PDF Semantic Scholar

Cite

Text

Aiello and Weyhrauch. "Checking Proofs in the Metamathematics of First Order Logic." International Joint Conference on Artificial Intelligence, 1975. doi:10.21236/ada007562

Markdown

[Aiello and Weyhrauch. "Checking Proofs in the Metamathematics of First Order Logic." International Joint Conference on Artificial Intelligence, 1975.](https://mlanthology.org/ijcai/1975/aiello1975ijcai-checking/) doi:10.21236/ada007562

BibTeX

@inproceedings{aiello1975ijcai-checking,
  title     = {{Checking Proofs in the Metamathematics of First Order Logic}},
  author    = {Aiello, Mario and Weyhrauch, Richard W.},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {1975},
  pages     = {1-8},
  doi       = {10.21236/ada007562},
  url       = {https://mlanthology.org/ijcai/1975/aiello1975ijcai-checking/}
}