<p>The compactness theorem for classical first-order logic is a direct consequence of the completeness theorem, and, actually, one can prove directly Compactness by the Henkin-style argument used for Completeness without ever mentioning derivation.</p>

<p>The Completeness theorem for classical FOL with respect to standard Tarski models has been formalized in Mizar. See the series of articles under <a href="http://fm.mizar.org/2005-13/fm13-1.html">http://fm.mizar.org/2005-13/fm13-1.html</a></p>

<p>The same completeness theorem, but with a constructive proof, has been almost formalized in the Coq proof assistant by myself, see the zip file under <a href="https://sites.google.com/site/dankoilik/publications/phd-thesis">https://sites.google.com/site/dankoilik/publications/phd-thesis</a></p>

<p>I say "almost" because there is one technical point, proving a correctness of a sorting algorithm, that I have not yet had time to finish, however the main ingredient (constructive ultra-filter theorem for countable languages) is formalized.</p>

<p>One can also consider Completeness, and hence Compactness, for a non-standard notion of validity, and get a complete and formalized constructive proof.</p>

CC BY-SA 3.0
2012-02-06T18:14:46.700Z
2012-02-06T18:14:46.700Z
Danko Ilik
<p>Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998.  See <a href="https://doi.org/10.1007/BFb0055135" rel="noreferrer"><em>Formalizing basic first order model theory</em></a>.</p>

CC BY-SA 4.0
2020-03-09T22:59:18.633Z
2020-03-09T22:59:18.633Z
Michael Norrish
<p>I've been searching for a formalization of the compactness theorem for FOL, but haven't found any. Is anyone aware of such a development or related work?</p>

CC BY-SA 3.0
2012-02-03T09:42:05.607Z
Have you tried asking on the Coq or Isabelle mailing lists?
Dave Clarke
CC BY-SA 3.0
2012-02-05T05:30:21.570Z
I am not sure if this is suitable for cstheory, but see [this](http://www.cs.ru.nl/~freek/100/). Completeness is there, and compactness is not far from it.
Kaveh
CC BY-SA 3.0
2013-03-04T11:09:21.290Z
See also the [AFP entry](http://afp.sourceforge.net/entries/Completeness.shtml) for a version in Isabelle/HOL (from 2004).
Makarius
<reference-request><lo.logic><coq><proof-assistants>
Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?
Stefan Ciobaca
# Has the compactness theorem for FOL been formalized in Coq/Isabelle/etc?

(Asked by: username_0 on 2012-02-03)

I've been searching for a formalization of the compactness theorem for FOL, but haven't found any. Is anyone aware of such a development or related work?

**Tags:** reference-request, lo.logic, coq, proof-assistants

> **Comments:**
> **username_1**: Have you tried asking on the Coq or Isabelle mailing lists?  
> **username_2**: I am not sure if this is suitable for cstheory, but see [this](http://www.cs.ru.nl/~freek/100/). Completeness is there, and compactness is not far from it.  
> **username_3**: See also the [AFP entry](http://afp.sourceforge.net/entries/Completeness.shtml) for a version in Isabelle/HOL (from 2004).  

---

## 2 answers

### Answer by username_4 on 2012-02-06. Score: 18

The compactness theorem for classical first-order logic is a direct consequence of the completeness theorem, and, actually, one can prove directly Compactness by the Henkin-style argument used for Completeness without ever mentioning derivation.

The Completeness theorem for classical FOL with respect to standard Tarski models has been formalized in Mizar. See the series of articles under <http://fm.mizar.org/2005-13/fm13-1.html>

The same completeness theorem, but with a constructive proof, has been almost formalized in the Coq proof assistant by myself, see the zip file under <https://sites.google.com/site/dankoilik/publications/phd-thesis>

I say "almost" because there is one technical point, proving a correctness of a sorting algorithm, that I have not yet had time to finish, however the main ingredient (constructive ultra-filter theorem for countable languages) is formalized.

One can also consider Completeness, and hence Compactness, for a non-standard notion of validity, and get a complete and formalized constructive proof.


---

### Answer by username_5 on 2020-03-09. Score: 5

Compactness for FOL was done in HOL by John Harrison, and reported at TPHOLs 1998. See [*Formalizing basic first order model theory*](https://doi.org/10.1007/BFb0055135).


---

