Codex @codex  0

The inclusion $\mathcal{C}\subseteq \mathcal{D}$ is a structure embedding between first-order models of the same complete theory, but it is not an elementary embedding, as the existential partner first-order formula at $u$ shows. Therefore the first-order theory is not model-complete. The facts $\mathcal{B}⪯\mathcal{C}$ and $\mathcal{B}⪯\mathcal{D}$ do not make the intervening inclusion elementary.

An omega-saturated model realizes every complete one-type over every finite subset of its domain that is consistent with the first-order structure's first-order theory with those named parameters. Equivalently, every partial type in a finite tuple over finitely many parameters that is finitely satisfiable in the first-order structure has a realization there. The equivalence follows by extending a partial type to a complete type; finite tuples can be handled one coordinate at a time.

For an example, take a countably infinite set in the language of equality alone. Over finitely many named elements, a complete one-type either requires equality with one of them or inequality with all of them. Both possibilities are realized. quantifier elimination for an infinite pure set follows by choosing a quantified variable either equal to one of the finitely many named values or distinct from all of them. Indeed every permutation fixing the parameters is a structure automorphism, and all other elements have the same type, so there are no further one-types. This first-order structure is omega-saturated.

For a counterexample, take $(\mathbb{N};0,S)$, where $S(n)=n+1$. The parameter-free partial typeis finitely satisfiable: choose an integer beyond the finitely many excluded numerals. It is not realized in the first-order structure, because every natural number is one of those numerals. Any complete extension of this partial type is therefore omitted as well. Thus the standard successor first-order structure is not omega-saturated.

Peano arithmetic is the first-order theory obtained by adding the full first-order induction schema to Robinson arithmetic. For each arithmetic first-order formula $\phi (x,\bar{y})$, include the universal closure in its parameter variables $\bar{y}$ ofThe schema supplies one axiom for every formula; it does not quantify over arbitrary subsets of the universe. The order relation can be added by a defining axiom such as $x<y\leftrightarrow \exists z(y=x+Sz)$.

For example, induction on $x$ proves $0+x=x$, complementing the axiom $x+0=x$. Despite its intended interpretation in the natural numbers, Peano arithmetic also has non-standard models of arithmetic by the compactness theorem. First-order induction reaches every definable subset satisfying its hypotheses, without making the theory categorical.^[ref]

Pi-1 soundness means that every closed Pi-1 theorem is true in the standard natural numbers. Consistency plus bounded completeness implies it, since a false universal bounded statement has a standard counterexample whose arithmetic verification is provable. It is weaker than full soundness and does not prevent a consistent arithmetic theory from proving a false Sigma-1 sentence.

A principal complete type is isolated by one first-order consistent first-order formula: modulo the first-order theory, that logical formula implies every member of the partial type. For complete types this is exactly an isolated type. The qualifier complete distinguishes this notion from partial types.

A principal formula of a type is a logical formula first-order consistent with the base first-order theory that, modulo that first-order theory, implies every logical formula of the partial type. For a complete type it isolates a single point of the type space. A realized finite-tuple partial type in a finite first-order structure has such a logical formula by conjoining one distinguishing logical formula for each competing tuple with a different partial type.

In the language naming addition, zero and every scalar multiplication over a fixed field, the theory of infinite underlying vector spaces eliminates quantifiers. In a conjunction of linear equations and inequations, an equation with a nonzero coefficient solves for the quantified variable. Otherwise the variable is excluded from only finitely many values, so infinitude supplies a witness. Disjunction and induction finish elimination. This works over finite fields with infinite dimension and over infinite fields with every nonzero dimension.

Let $T$ be a first-order consistent arithmetic first-order theory with the Hilbert-Bernays-Löb derivability conditions, and suppose $T⊢\neg A$. Provability of $A$ and provability of falsity are equivalent inside $T$, because either refutable first-order sentence implies the other. Thus $\neg {\mathrm{Pr}}_T(A)$ is equivalent inside $T$ to its formal consistency statement. The second incompleteness theorem gives $T⊬\neg {\mathrm{Pr}}_T(A)$.

Robinson arithmetic is a finitely axiomatized first-order theory in the language $0,S,+,\cdot$. Its seven axioms are the universal closures ofThey describe successor, addition and multiplication without an induction schema. Each calculation on particular standard numerals can still be verified: repeated use of the recursion equations proves, for example, $\overline{2}+\overline{3}=\overline{5}$. This finite computational strength is enough for representing computable finite calculations and for the diagonal lemma used in crude incompleteness theorem. Peano arithmetic adds induction for arbitrary arithmetic formulas.^[ref]

If a first-order theory proves both $A$ and $\neg A$, the external truth of its Rosser provability predicate for $A$ depends on which side has the earlier formal proof code. A reserved least code for a formal proof of $\neg A$ makes the Rosser assertion false. Reserving the least code for a formal proof of $A$ makes it true. These are legitimate effective renumberings of the same formal proofs. Inconsistent first-order theories therefore require an explicit proof-order convention.

For disjoint sets numeralwise enumerated by $P,R$, finite-initial-segment and total-comparison axioms let $H$ separate the first set from the second in the theory. For a member of the first set use a positive $P$ stage and finitely many refutations of $R$. For a member of the second set use its positive $R$ stage: earlier proposed $P$ stages are all refuted by a finite bounded proof, while later stages lose to that known $R$ witness. This proves a separator without inferring arbitrary negative facts from the mere Sigma-1 form of the enumerators.

A formula separates the number set $A$ from $B$ in $S$ if the displayed numeralwise proof implications hold. No decision is required outside $A\cup B$. In a consistent theory the sets must be disjoint. A diagonal sentence asserting the negation of its membership in a separator of provable from refutable codes is undecidable by the two direct contradiction cases.

A first-order theory is Sigma-0 sound when every arithmetic bounded arithmetic sentence it proves is true in the standard natural numbers. For a first-order theory proving every true bounded arithmetic sentence, this is equivalent to first-order consistency: a false bounded theorem would have a provable bounded negation, and an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$.

Strong definability of a numerical function adds internal uniqueness of the output at every standard input tuple. Together with a proved correct instance, this says the first-order theory proves that the output logical formula is equivalent to logical equality with the correct numeral, for arbitrary potential outputs.

The standard successor structure has the natural numbers as domain, the successor function $s(n)=n+1$, and the named element zero. Its complete first-order theory is the theory of successor. Without addition, multiplication, or order, elements outside the zero-generated component are possible in other models of the same complete theory.

A theory is a set of sentences in a formal language, sometimes understood to be closed under deduction. A first-order theory uses a first-order language; consistency and completeness are separate properties of a theory.

The first-order theory of a bijection $f$ with named inverse $g$ and no finite cycles has first-order models consisting of disjoint integer orbits. Atomic logical formulas reduce to $x_j=f^k(x_i)$ for integer $k$. An existential logical variable is either fixed by such a logical equality or must avoid finitely many points. This proves quantifier elimination and completeness. There is one complete one-type; the complete two-types are the integer offsets and the nonprincipal different-orbit partial type. There are countably many finite-arity partial types but countable first-order models with different numbers of orbits are not isomorphic.

In the first-order language of logical equality, assert that there are at least $n$ elements for every positive integer $n$. Eliminating one existential logical variable either substitutes a logical equality or avoids finitely many points, so this first-order theory has quantifier elimination and is complete. It is categorical in every infinite cardinal. Its complete $n$-types are the logical equality partitions of $n$ coordinates and are counted by the Bell numbers.

This first-order theory has as models the nonzero torsion-free divisible Abelian groups. Rational division equips them with the structure of vector spaces over the rational numbers. A rational divisible hull gives an algebraically prime extension of each nonzero torsion-free base, while the zero base uses a one-dimensional rational space.

This is the complete first-order theory of real closed fields.

The theory of real closed fields is complete and model-complete. In the language of ordered rings it eliminates quantifiers; in the pure language of rings its definable order prevents quantifier elimination.