Take the 2-minute tour ×
Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It's 100% free, no registration required.

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?

share|improve this question
Have you tried asking on the Coq or Isabelle mailing lists? –  Dave Clarke Feb 3 '12 at 9:42
I am not sure if this is suitable for cstheory, but see this. Completeness is there, and compactness is not far from it. –  Kaveh Feb 5 '12 at 5:30
See also the AFP entry for a version in Isabelle/HOL (from 2004). –  Makarius Mar 4 '13 at 11:09
add comment

1 Answer 1

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.

share|improve this answer
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.