How might we prove that certain results cannot be deduced from certain axioms? There is an easy technique. To show that “ab = ba” cannot be deduced from the group axioms it suffices to show an explicit model for the axioms that is not commutative. Show an unsymmetric multiplication table that satisfies the group axioms.
It is somewhat trickier in the case of models for set theory perhaps because those axioms strive for completeness and do their best to be canonical which would mean that there was but one model, up to isomorphism. That there are many models that can be “constructed” is the realm of incompleteness proofs.
I will talk about a completeness proof of a theorem originally proved by Gödel. It states that all true propositions in predicate calculus are provable from standard axioms. In light of the fact that there is no decision procedure for theoremhood in the predicate calculus this is a remarkable result that cannot be constructive for then there would be a decision procedure.
The proof that I describe here was found by Leon Henkin and is much easier than Gödel’s.
I must now describe the predicate calculus. Most formulations are equivalent except for minor syntactic matters. There are individual variables and individual constants that designate elements of the model. We write individual variables as a1, a2, etc, and individual constants as b1, b2, etc. There are infinitely many of each. Each argument is either an individual variable or individual constant. We write predicates as P1, P2, etc. In some particular theory there are some predicates each of which take some definite number of arguments. We shall never need more than a finite number of predicates here. We write the predicates with their arguments as P1a3b4, where P1 is some predicate that takes two arguments. There are boolean connectives which we limit here to → (if ... then ...) and ~ (not). There is also the universal quantifier symbol ∀. If x is some individual variable then ∀x is a quantifier. ∀a2α means that α is true for all a2. A sentence is an expression with no free variables.
We need to be clearer about models. A model is a set of objects and a map from the individual constants to the objects and a map that for each predicate, specifies for which tuples of the objects the predicate is true. Expressions with free variables can then assigned truth values depending on values assigned to the free variables therein. If α is an expression all of whose free variables are among x, ... z. then ∀x ... ∀zα is true in then model just if it is true for α
First what is “truth”?, or more accurately, what is truth? In the predicate calculus a sentence is considered true if any interpretation of the constants of the language in any model turn out to be true for that model. There is no general test for truth; there is no algorithm guaranteed to stop and report whether an input sentence is true or not.
A sentence is satisfiable if there is a model for which it is true. The proof proceeds first by proving that if a collection of sentences is mutually consistent; that is if no contradictions can be derived therefrom, then there is a model that satisfies all of them. |−
Henkin’s proof proceeds by enumerating all sentences and considering them in turn. For each a decision is made to declare it true or false in light of preceding decisions. The enumeration is such that a sentence that is a proper part of another, comes before the other. If the sentence is consistent with the decisions before, it is declared true, otherwise false. When a sentence ∀aj φ beginning with a universal quantifier is found to be inconsistent and declared false, a previously unmentioned individual constant bk is selected and φ(bk/aj) is prematurely declared as false. (φ(bk/aj) is the sentence that is like φ except for having bk where ever aj is free in φ.)
In general an infinite supply of individual constants is necessary to complete the process for some consistent set of sentences. The collection of sentences consisting of a predicate followed by individual constants, and whether we declared them true, prematurely or otherwise, gives the denumerable model explicitly.
The denumerable models generated by Henkin’s method are not constructive for while the top level the proof is constructive, the consistency decisions are not.
A few simple lemmas are needed which had been skipped over. For instance it is necessary to prove that the premature decisions leave the set of decisions consistent. The purpose of the premature decisions is to ensure omega consistency.