Formalizing basic first order model theory
J. Harrison. Formalizing basic first order model theory. Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170.
En este trabajo se presenta una formalización de la teoría de modelo de la lógica de primer orden, El libro de partida es el de Kreisel y Krivine Elements of mathematical logic: model theory. El sistema en donde se realiza la formalización es en HOL-Light. La motivación del trabajo fue la de escribir un libro de texto de lógica matemática.
En el trabajo se describe la formalización realizada:
- Definición de los conceptos sintácticos.
- Definición de los conceptos semánticos.
- Demostración de metateoremas:
- Teorema de compacidad para la sublógica proposicional.
- Formas prenexas y de Skolem.
- Modelos canónicos.
A lo largo del trabajo se explica las razones para elegir la representación utilizada. Generalmente es par mantener la fidelidad al texto y ser la más intuitiva.
Este trabajo pude usarse para la formalización de la metalógica en Isar. Habría que considerar la evaluabilidad de los procedimientos y la conveniencia de usar Isabelle/ZF (para evitar los problemas con los tipos que se comenta en el trabajo).
José A. Alonso 10:20, 4 December 2008 (CET)
