Meta-Theorem: Every true sentence of the predicate calculus has a formal proof.

Gödel had proven this theorem in 1929 but Henkin’s later proof is much more accessible. The top lemma of Henkin’s proof (and Gödel’s) is that every consistent sentence has a model where the sentence is true. In short: “consistent sentences are satisfiable”. A consistent sentence is one from which no contradiction can be derived using the axioms and rules of deduction. There is no decision procedure for consistency but the distinction is nonetheless meaningful. (Hilbert has suggested this idea a bit earlier when he said that mathematical existence was the mere absence of contradiction.)

To prove this lemma Henken outlined a procedure that would create a model, one element at a time, fill in decisions for predicate values for the new individual forced by the consistent sentences. This construction was enabled by the consistency of the statements. For technical reasons it is necessary for the model to be ω-consistent which means that if ⸢¬Πα¬φ⸣ (whose supplied semantics meant there existed something that made φ true) was derivable from the sentences. (Much more detail here) There were delicate maters to choose in an order so as not to have to backtrack.

Now if every consistent sentence can be satisfied by some model then: Any sentence with no model is inconsistent! For α to be inconsistent means that there is a formal proof of ⸢¬α⸣. If α is valid (satisfied in all models) there is no model where ⸢¬α⸣ holds and thus there is a proof of ⸢¬¬α⸣ and thus of α. Here is better detail.