For unrestricted consistency self-strengthening is inconsistent, again take . In the axiom and the preceding implication prove . The additional rule then proves .
However consistency of an extension implies consistency of its subtheory by the formalized inclusion of proofs: . Thus the ordinary theory contains and derives , so it has a finite contradiction proof. Checking that concrete proof in arithmetic gives . This theorem is also present in , contradicting the result of the new rule. Therefore is inconsistent.
The error in the added rule is its unrestricted internal use on arbitrary arithmetically presented systems, including systems containing false consistency assertions. A true external consistency progression for a specified sound system is not this unrestricted inference rule.
The literal semantic hypothesis is insufficient: a semantic Gödel fixed point need not be canonical. A sentence can be false and provable in a consistent, unsound arithmetic theory, in which case both sides of the stipulated semantic biconditional can be false.
For a concrete counterexample, assume PA is consistent and set . Gödel's second incompleteness theorem makes this extension consistent: otherwise PA would prove its own consistency. It is still bounded-complete. Use ordinary numeralwise proof and refutation enumerators for this recursively axiomatized theory, and take . This is false in the standard natural numbers but is an axiom of . Since it is provable, is true; its negation is false. Thus the semantic fixed-point biconditional required in this part is true, with both sides false.
Choose by the usual canonical Rosser construction for these proof matrices. Its undecidability follows from the preceding parts, and it is a true sentence: if it were false, its true negation would be provable in this bounded-complete theory, contradicting undecidability. Hence is false and true, so their proposed semantic equivalence is false. This counterexample meets the literal assumptions and does not exploit a missing source page.
Under the intended canonical Gödel/Rosser convention, the expected answer does hold. Consistency plus bounded completeness implies soundness: a false theorem has a standard bounded counterexample whose negation the theory proves. If canonical were false, its truth fixed point would make it provable, contradicting this soundness; thus is true. Canonical is true by the preceding -negation argument, so both canonical sentences are true and their equivalence is true. This last conclusion needs that canonical construction or an equivalent additional restriction; truth of a biconditional alone does not supply it.
Gödel's second incompleteness theorem says that a consistent effectively presented arithmetic theory with an adequate proof predicate cannot prove its formal consistency statement. The background strength must support the diagonal lemma and the derivability conditions, as in the present arithmetic setting.
Löb's theorem says
It is a theorem about derivability for every sentence , not merely an external soundness assertion about the interpretation of . Taking , a proof of consistency gives ; Löb then gives . Thus a consistent cannot prove consistency. This is how the second incompleteness theorem is the contradiction-sentence instance of Löb's more general result.
Under the deductively closed convention, an -theory is a set of -sentences containing all its first-order logical consequences: if , then . By completeness this is equivalent to closure under provability. An axiom set is often called a theory too, with its deductive closure understood. Neither convention by itself requires completeness or satisfiability; an inconsistent deductively closed theory contains every sentence.
A complete satisfiable theory has a model and decides every -sentence: for each , exactly one of and is a consequence. Under the closed convention, exactly one belongs to . Satisfiability excludes the possibility of both. Equivalently all models of the theory are elementarily equivalent, even though they need not be isomorphic or have equal cardinality.
If a model of contains as a substructure, every existential sentence true in remains true in : use the same witness tuple and preservation of quantifier-free truth. Hence satisfies the required joint theory.
For the existential-theory embedding criterion, conversely suppose that joint theory has a model. Expand the language by a constant for each , and add the atomic and negated atomic diagram to . Any finite collection of its literals is a quantifier-free conjunction true of the corresponding tuple in . Replacing those named constants by variables and existentially closing gives a sentence in . A model of the assumed joint theory can supply its witnesses, and hence an expansion satisfying those finitely many diagram requirements and any finite subset of .
Compactness therefore gives a model of . Its named Elements define an embedding of into its -reduct: inequalities ensure injectivity, and all function and relation literals ensure preservation and reflection. Replace the ambient model by an isomorphic copy identifying this image with itself. Thus a model of containing exists. The diagram step explains how parameter-free existential information nevertheless yields an embedding of the whole structure.
If and , every universal sentence of holds in and is preserved by passage to the substructure . Thus witnesses satisfiability of the joint theory.
For universal theory and substructures of elementarily equivalent models, conversely let satisfy together with the universal theory of . Every existential sentence true in must be true in : if an existential were false in , its universal negation would belong to and hold in , a contradiction. Hence . In particular is satisfiable, with model . Apply the preceding embedding result to the theory and structure . It supplies a structure containing . Therefore and , as required. Elementary equivalence here does not assert that itself contains a copy of .
The natural-number successor chain embeds into the integer successor chain by ordinary inclusion. Thus witnesses the existential joint satisfiability in the first assertion. The two chains are not elementarily equivalent: every integer has a predecessor, whereas zero has none in the natural-number chain.
For the universal assertion, construct an elementary extension of the natural-number chain containing a two-sided successor chain. To its elementary diagram add distinct constants for with and require them to differ from all named natural numbers. Every finite subset is realized in the natural-number chain: place the finitely many required consecutive blocks sufficiently far to the right, away from the finitely many forbidden named Elements. Compactness yields an elementary extension with the required two-sided chain. That chain is a substructure isomorphic to the integer successor structure and hence is a model of its complete theory.
Consequently both joint theories in the two assertions are satisfiable, though the integer chain cannot embed into the natural-number chain itself: repeated predecessors would give an infinite descending sequence of natural numbers. The second assertion correctly uses an elementarily equivalent ambient structure rather than the original one.
The complete theory is the set of all -sentences true in . The existential theory of a structure consists of those true sentences of the form with quantifier-free . The universal theory uses with quantifier-free matrix. Allow equivalent formulas and empty quantifier blocks, or insert dummy variables in nonempty domains. These are sentences in the original language, distinct from diagrams, which add constants naming Elements of the structure.
A theory is -categorical if it has a model of cardinality and any two models of that cardinality are isomorphic. The existence clause prevents vacuous categoricity at cardinalities where there is no model.
To show that infinite-cardinal categoricity forces completeness, suppose were incomplete. Then some sentence has both and satisfiable, by completeness of first-order logic. Their models must be infinite because has no finite models. For an infinite , the upward and downward Löwenheim-Skolem theorems produce a model of each extension of cardinality exactly : pass to an elementary submodel of size at most and then to the desired size, or reduce a larger model to that size. Categoricity makes these two models isomorphic, but one satisfies and the other its negation. Contradiction. Therefore is complete. If language size is defined without automatically including , the infinite-cardinal qualification is explicit; the assumed existence of a -sized model and absence of finite models already force it here.
Let be the formulas whose free variables are among . Define when . The n-variable Lindenbaum algebra quotient is a Boolean algebra, with meet, join and complement induced by conjunction, disjunction and negation; its zero and one are contradiction and truth classes. Its order is exactly when .
The Ryll-Nardzewski theorem states that for a complete theory with infinite models in a countable language, the following are equivalent: the theory is countably categorical; for every finite there are only finitely many complete -types over the empty set; and every Boolean algebra is finite. Equivalently each such type is isolated. The countable-language and completeness hypotheses are essential parts of this formulation.
A complete -type over is a maximal set of formulas in variables consistent with ; it decides each such formula or its negation. A partial type drops maximality. A tuple realizes the type if it satisfies every member. A complete type is principal, or isolated, if some formula consistent with implies every member of the type modulo ; then itself belongs to that type.
The omitting types theorem says that in a countable first-order language, a consistent theory has a countable model omitting a specified nonprincipal type; more generally a countable family of nonprincipal types can be omitted simultaneously. In the present complete-theory setting it applies directly to complete nonisolated types. “Omitted” means that no tuple in the model realizes all formulas of the type, even though each finite subset is compatible with the theory.
An -saturated model realizes every complete type in finitely many variables over every finite parameter subset of itself. It suffices equivalently to require one-variable types and then realize finite tuples successively. The definition puts no countability restriction on the size of the model.
For any model , collect all complete types over its finite parameter sets. Add to its elementary diagram, for each such type, a new tuple of constants satisfying all that type's formulas. Any finite selection of these requirements is realizable in : each finite type fragment has its existential closure true there, since it is consistent with the complete theory of the corresponding named finite tuple. Distinct new tuples have no additional mutual restrictions. Compactness gives an elementary extension realizing all these types simultaneously.
Start from any model and apply this construction repeatedly to obtain , with each successor realizing all types over finite subsets of its predecessor. The elementary-chain theorem makes a model of with every stage elementary in it. A finite parameter set lies in some . Every type over consistent with is consistent with , since the expanded complete theories at those parameters agree by elementarity. It is realized in , hence in the union. Therefore an -saturated model always exists, possibly with uncountable cardinality.
No infinite cardinal is categorical for this theory, as described by no categorical cardinal for the complete named rational diagram. For an arbitrary infinite , choose a dense linear order without endpoints of size ; for example the lexicographic order on works, since every rational block is dense and has no endpoints.
Construct one order by inserting into a fixed irrational cut of the named rational order. Every element of this order is bounded above by some named rational. Construct a second order by putting an tail above all named rationals, as the ordered sum . Both are dense linear orders without endpoints, both have cardinality , and both contain the named rational copy as an elementary substructure by quantifier elimination. Hence both satisfy its complete diagram .
They are not isomorphic over the named constants: the second has an element greater than every named rational, and the first has none. This property need not be expressible by a single sentence in the infinite language to be an isomorphism invariant. Finite cardinalities have no models at all because the constants name infinitely many distinct Elements, so the existence clause excludes categoricity there too.
For the additive first-order structure, let
It defines . These sets are pairwise distinct: if , the integer belongs to but not to . Thus there are infinitely many inequivalent one-variable first-order formulas modulo the complete theory of the additive integers. The Ryll-Nardzewski theorem implies that first-order theory is not aleph-zero-categorical.
For the multiplicative first-order structure define divisibility by . For , the first-order formula
asserts the existence of at least distinct integer divisors. The integer has exactly such divisors, namely for , so it satisfies but not any with . Again there are infinitely many inequivalent one-variable first-order formulas. The Ryll-Nardzewski theorem therefore implies the first-order theory of the multiplicative integers is not aleph-zero-categorical.
A model-complete theory is a first-order theory for which every structure embedding between two of its first-order models is an elementary embedding. Thus, if is such an embedding, then for every first-order formula and tuple from ,
first-order model completeness does not assert that every two first-order models are elementarily equivalent: it constrains embeddings that exist between first-order models, whereas completeness constrains all first-order models.
A first-order theory has quantifier elimination if every first-order formula is equivalent over the first-order theory to a quantifier-free formula with the same free variables:
Logical truth and falsity may be treated as the empty Boolean combinations when considering sentences in a language without closed terms. The assertion concerns first-order formulas with free variables, not merely sentences.
A complete theory is a consistent first-order theory deciding every sentence in its language:
Equivalently, every two first-order models of are elementarily equivalent. Consistency excludes the vacuous situation in which a first-order theory has no first-order models and entails both alternatives.
No. Let be the displayed infinite axiom set. Any finite subset mentions only finitely many of the two infinitude requirements. Choose at least as large as every index mentioned. A finite equivalence relation with exactly singleton classes and doubleton classes satisfies , but is not a first-order model of the complete theory.
If a finite axiomatization existed, let be the conjunction of its axioms. Then , so the compactness theorem gives a finite with . Every first-order model of would then satisfy the full first-order theory, contradicting the finite first-order model above. This is the finite subaxiomatization from an equivalent finite theory argument: finite axiomatizability would force one finite fragment of the explicit axioms to suffice.
Write
These are first-order formulas in the original language, not new predicate symbols. An axiomatization consists of the equivalence relation axioms for , the bound
and, for every , the two sentences
The first scheme supplies infinitely many singleton classes. The second supplies infinitely many distinct non-singleton classes; the size bound makes these doubletons.
Every countable first-order model has countably infinitely many classes of each size. A bijection between singleton classes, and another between doubleton classes followed by a bijection inside each matched pair, gives an isomorphism between any two countable first-order models. To infer completeness, suppose a sentence had different truth values in two arbitrary first-order models. The Downward Lowenheim-Skolem theorem supplies countable elementary substructures of those first-order models, which would still disagree on the sentence, contradicting the isomorphism just constructed. Thus all first-order models satisfy the same sentences. Since the original first-order structure satisfies the axioms, these axioms form a complete axiomatization of its first-order theory. This is the theory of infinitely many singleton and doubleton equivalence classes.