A Universe of Sorts

§ Compactness theorem of first order logic

Define a theory to be a set of sentences.
Compactness states that if a theory T is such that every finite subset Tfin ⊂ T of the theory has a model, then T itself has a model.

Let L be a language.
We study CONSISTENT := { T ⊂ 2^L : T has a model } to be the set of all theories of L which is consistent.
(1.a) We analyze CONSISTENT and see that it has properties satisfcation ( (S0) ... (S8)).
(1.b) We show that if K is a set of theories which has satisfaction, then so does PROFINITE(K) := { T ∈ K : ∀ Tfin ⊂ T, Tfin has a model }.
(2.a) We analyze, for a model M, the set TRUTHS := { T : T is true for M }. We see that it has properties of called closures ( (C0), ..., (C8)).
(3) We show that if Δ has (C0), ... (C8), then Δ has a model (the term model).
(4) Show that if Γ is a theory, then Γ# is the closure of the theory, such that Γ# obeys (C0)... (C8) and (Γ ⊂ Γ#).
(5) Show that if Γ ∈ S where S has satisfaction, then one can build a Γ ⊂ Γ# ∈ S where Γ# is closed.
(6) To prove compactness, take a theory Δ ∈ PROFINITE(CONSISTENT). Since CONSISTENT has satisfaction, and PROFINITE preserves satisfaction, PROFINITE(CONSISTENT) has satisfaction. Now apply (5) to build the closure Δ#. Use (3) to build the term model M(Δ#), a model for Δ#, which is also a model for Δ.

0. Define a property called "satisfaction" which is possessed by the set of consistent theories.
1. See that the profinite completion of a satisfaction set also obeys satisfcation.
2. Define a property called closure on a theory, where a closed theory possesses a term model.
3. Show that every theory in a satisfaction set also has a closure in the satisfaction set.
4. Take Γ ∈ PROF(CONSISTENT), a theory Γ which is profinite, which we wish to build a model for. Create Γ#, the closure, such that Γ ⊂ Γ#. See that Γ# has a model (the term model MΓ), and that this is also a model for Γ, and thus Γ is consistent.

See that given a S which obeys (S1)... (S8), PROFINITE(S) has finite character .
A family F has finite character is defined to be: A ∈ F iff all subsets of A belong to F.
Show that for any Γ ∈ S*, there is a maximal Γ# ∈ S* which contains Γ. This follows by Zorn on S*. Let the partial order by the subset ordering on S*(Γ) := { Δ ∈ S* | Γ ⊂ Δ }. See that every chain has a maximal element, by the finite character property. Thus, S*(Γ) has a maximal element, call it Γ#.
Show that this Γ# obeys (C0)... (C8) [closure properties ] This will rely on S* having (S1).. (S8). Thus, Γ# possesses a model (the term model).
This means that Γ also possees a term model.