Formalizing Basic First Order Model Theory

John Harrison.

Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170.

Abstract:

We define the syntax of unsorted first order logic as a HOL datatype and define the semantics of terms and formulas, and hence notions such as validity and satisfiability. We prove formally in HOL some elementary metatheorems such as Compactness, Löwenheim-Skolem and Uniformity, via canonical term models. The proofs are based on those in Kreisel and Krivine's book on model theory, but the HOL formalization raises several interesting issues. Because of the limited nature of type quantification in HOL, many of the theorems are awkward to state or prove in their standard form. Moreover, simple and elegant though the proofs seem, there are surprising difficulties formalizing Skolemization, one of the more intuitively obvious parts. On the other hand, we significantly improve on the original textbook versions of the arguments, proving two of the main theorems together rather than by separate arguments.

DVI or PostScript or PDF

Bibtex entry:

@INPROCEEDINGS{harrison-model,
        crossref        = "hol98",
        author          = "John Harrison",
        title           = "Formalizing Basic First Order Model Theory",
        pages           = "153--170"}

@PROCEEDINGS{hol98,
        editor          = "Jim Grundy and Malcolm Newey",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           11th International Conference, TPHOLs'98",
        series          = "Lecture Notes in Computer Science",
        volume          = 1497,
        address         = "Canberra, Australia",
        date            = "September/October 1998",
        year            = 1998,
        publisher       = "Springer-Verlag"}