Proof assistants or libraries in proof assistants for working with model theory

Question

The basics of model theory contain, as far as I understand, some theorems that are difficult to prove in their full generality.

For example, the compactness theorem in FOL for languages with arbitrarily many symbols was proven by Maltsev in 1936. Gödel originally proved the countable case in 1930.

Trying to formalize model theory and make a usable library in a proof assistant seems like it would be pretty tough, since you have to make some awkward foundational choices. What exactly is $\models$? It's probably too big to be a set.

I'm wondering if there are any proof assistants out there that have a model theory library or ones that were specifically designed to tackle this area (or do other similar things, like study set-based semantics of non-classical logics with a classical set theory in the background).

Answer 1

First, recall that model theory (of FOL) is just mathematics about certain types of mathematical objects, "structures" as they are defined in model theory. So it isn't really any more difficult than working with say groups or topological spaces. (I'm probably brushing too much under the rug, but at least Lean and Coq, since they have universes, they should avoid the "set" issue you mention. Also, I think the technical term for how model theory is usually handled is "deep embedding", but I'm not sure I could give a good definition off hand.)

HOL-Light

John Harrison formalized FOL model theorem in HOL-Light. The paper is Formalizing basic first order model theory. Some code I've found is some theorems on logic up the the compactness theorem, and this folder about the logic of arithmetic which I think also has other logic stuff including some completeness theorem results (and maybe also the incompleteness theorem). This is another completeness theorem possibly for a different logic.

Other theorem provers

Also see the Lean project A formalization of forcing and the unprovability of the continuum hypothesis. Besides being the type of work I think you are interested in, it also has a good background section which I'll quote here:

First-order logic, soundness, and completeness There are many existing formalizations of first-order logic. Shankar [39] used a deep embedding of first-order logic to formalize incompleteness theorems. Harrison gives a deeply embedded implementation of first-order logic in HOL Light [18] and a proof-search style account of the completeness theorem in [19]. Margetson [33] and Schlichtkrull [34] use the same argument for the completeness theorem in Isabelle/HOL, while Berghofer [6] (in Isabelle) and Ilik [22] (in Coq) use canonical term models.

Answer 2

Lean powers https://flypitch.github.io/ which formally verifies the independence of the continuum hypothesis.

Some of that material is currently being ported to mathlib's model_theory folder: https://leanprover-community.github.io/mathlib_docs/model_theory/basic.html (see the sidebar for other files in that directory). So far, it's really the basic definitions, and nothing like the compactness theorem or so.