For a standard classical propositional calculus, strong completeness statesTogether with soundness, this identifies semantic consequence with formal derivability. One proves the contrapositive by the maximal consistent set in propositional logic construction. If , the set is propositionally consistent, by the deduction theorem for propositional logic and classical propositional reasoning. Extend it to a maximal consistent set in propositional logic , deciding each logical formula in turn. At each stage at least one selection of or preserves propositional consistency; a contradiction in the union would use only finitely many assumptions and hence already occur at a stage.
Define a Boolean valuation by exactly when . Maximal consistency in propositional logic gives exactly when , and exactly when either or . Structural induction on logical formulas therefore proves the maximal consistent set truth lemma . Thus satisfies but falsifies , contradicting semantic entailment. The countable language here permits an enumeration of logical formulas; the corresponding general-language argument uses a well-ordering or a principle of maximality in a partially ordered set.
Gödel's completeness theorem for first-order sentences says that, in a standard sound first-order Hilbert calculus,Equivalently every first-order consistent set of first-order sentences has a first-order model: apply this existence statement to for the consequence formulation.
For the first-order model existence formal proof use a Henkin construction. Enlarge the language by fresh constant symbols and adjoin Henkin witness axiomsFreshness of preserves first-order consistency. In detail, if a contradiction followed after adjoining one witness axiom, the deduction theorem for first-order logic would yield its negation, from which one obtains both and over the old theory. Since the new constant symbol does not occur in that theory or in , replace it by a fresh logical variable and generalize to derive , a contradiction. Finitely many witness additions preserve first-order consistency successively, and unions preserve first-order consistency because formal proofs are finite. Iterate the enlargement so that logical formulas involving newly introduced constant symbols also receive witnesses. Include at least one constant symbol to guarantee closed terms.
Extend the resulting first-order consistent witnessed first-order theory to a maximal consistent set of first-order sentences . In the equality-free case make the domain the set of closed terms. Interpret constant symbols and function symbols by their formal first-order term constructions; interpret an atomic formula byThe truth lemma for a Henkin term model follows by induction on logical formulas with closed terms substituted for their free variables. The logical connective steps use maximal consistency of a first-order theory. In the existential step, membership of supplies a witness constant and hence a first-order term satisfying ; conversely a satisfying closed term gives the existential sentence by an inference of the calculus. The term model consequently satisfies and the original theory. Equality is absent here, so distinct closed terms may remain distinct domain elements without further identifications.
In the presence of equality, two syntactically different closed terms can be asserted equal by the Henkin theory, so the raw first-order term domain from part (b) must be replaced by a quotient set. DefineThe equality axioms give reflexivity, symmetry and transitivity, so this is an equivalence relation. Their substitution consequences make it a congruence relation on a first-order structure: replacing an input by an equivalent first-order term preserves equivalence of function values and preserves membership of atomic formulas in .
Take domain . Define a function symbol by , and relations by the same membership test as before using representatives. The congruence relation on a first-order structure makes these definitions independent of representatives. Actual identity of equivalence classes now agrees with the formal equality first-order sentences in :This supplies the equality case of the truth lemma for a Henkin term model; the logical connective and quantifier cases then proceed exactly as in the Henkin construction. Thus the term model built from the quotient set is a genuine first-order model with equality interpreted as identity.
For a countable first-order language, the Henkin construction introduces only countably many constant symbols: each round needs at most one for each logical formula, there are countably many finite strings in a countable alphabet, and countably many rounds suffice. There are therefore at most countably many closed terms. The term model, and also its quotient set by equality, has at most countably many elements.
It follows that every satisfiable theory in a countable first-order language has an at most countable first-order model. If the theory has no finite first-order model, the constructed first-order model is countably infinite. More generally the same counting argument gives a first-order model of cardinality at most for any satisfiable theory in language .
For the elementary-substructure version of the downward Löwenheim-Skolem theorem, begin with a first-order structure and a set of designated elements. Close , the named constant symbols and one initial element under the language's functions and under chosen witnesses in for existential formulas with parameters already chosen. Iterate countably often. The resulting set has cardinality at most , and its induced substructure is elementary: induction on logical formulas proves the truth equivalence, with the existential case supplied by the chosen witnesses. This is the same witness mechanism as the Henkin formal proof, now keeping witnesses inside a given first-order model.
Let in the finite language of rings: it is the set of all first-order sentences true in the field of complex numbers. It is satisfiable, with first-order model , so the countable-language Löwenheim-Skolem theorem gives an at most countable first-order model of .
All field axioms belong to , hence is a field. For every positive integer , the first-order sentence saying that there are at least distinct elements is also true in and belongs to . Thus cannot be finite, and is countably infinite.
Finally, for each first-order sentence , either or . Since satisfies all of , it satisfies exactly when does. ThereforeElementary equivalence concerns first-order first-order sentences and does not imply an isomorphism; the two fields have different cardinalities. The stronger downward form may even choose as a countable elementary subfield of .
Articles by others on the same topic
There are currently no matching articles.