Model theory and Gödel's incompleteness theorems course of the University of Oxford (C1.1)

Source release: Oxford examination archive release thread, Part C bundle pages 300–304. This is one combined paper covering both courses: section A concerns Gödel second incompleteness theorem and provability logic, and section B concerns model theory. The cover cross-lists Mathematics and Mathematics and Philosophy, both Part C, Thursday 10 June 2010, 2.30pm–5.30pm.

Answer availability checked on 28 October 2026: bounded official Oxford searches by exact year, paper label and both subjects found no advertised exact-paper answers. The official Part C syllabus for the 2010 examination confirms the paired course identity. No later-year answer-release policy was assumed applicable.

Write $\square A$ for the arithmetical provability predicate applied to the Gödel number of $A$. Use the Hilbert-Bernays-Löb derivability conditions that belong to the course meaning of a provability predicate: external necessitation rule, internal modus ponens rule, and positive introspection. No incompleteness theorem is needed here.

If $S⊢G$, necessitation rule gives $S⊢\square G$. The displayed Gödel sentence equivalence also gives $S⊢\neg \square G$. These two theorems contradict the assumption that $S$ is a consistent first-order theory. ThereforeFor this part alone, the external necessitation rule condition suffices; the stronger internal conditions are used in the next part.

Again abbreviate provability by $\square$. The Gödel sentence equivalence gives $S⊢G\to \neg \square G$. Internalizing this implication using the first two Hilbert-Bernays-Löb derivability conditions givesPositive introspection also gives $S⊢\square G\to \square \square G$. Internal modus ponens rule combines proofs of a sentence and its negation into a proof of a contradiction; a contradiction implies any sentence. ConsequentlyThese are syntactic manipulations of provability, not an appeal to soundness. If $S⊢\neg \square \neg G$, taking the contrapositive of the last implication gives $S⊢\neg \square G$, and the diagonal equivalence gives $S⊢G$. Part (a) rules that out for a consistent theory. Hence

An arithmetic theory is one-consistent if there is no bounded arithmetic formula $\delta (x)$ for which it proves $\exists x\delta (x)$ and also proves $\neg \delta (\overline{n})$ for every standard natural number $n$. A finite tuple of existential witnesses can be coded by one natural number. The associated Sigma-1 soundness property says that every ${\Sigma }_1$ sentence it proves is true in the standard natural numbers.

Suppose first that the theory is one-consistent, but proves a false ${\Sigma }_1$ sentence $\exists x\delta (x)$. For every standard $n$, $\neg \delta (\overline{n})$ is then a true bounded sentence. Bounded completeness makes each such sentence a theorem, violating one-consistency.

Conversely suppose the theory is ${\Sigma }_1$-sound. If it proved both the existential sentence and every negated standard instance, soundness would supply an actual witness $n$. Its positive instance $\delta (\overline{n})$ is a true bounded sentence and hence provable. Together with the assumed negative instance this would make the theory inconsistent; an inconsistent theory proves a false ${\Sigma }_1$ sentence, contrary to soundness. Thusunder the stated bounded-completeness assumption. In particular either condition implies that the theory is a consistent first-order theory.

By part (c), one-consistency gives Sigma-1 soundness and hence ordinary consistency. First, $S$ cannot prove $\neg G$: if it did, the diagonal equivalence would give $S⊢\square G$. This is a ${\Sigma }_1$ sentence, so soundness would make it true. The stipulated standard interpretation of the arithmetical provability predicate would then supply an actual proof of $G$, contradicting consistency.

Now suppose $S⊢\square \neg G$. This too is a ${\Sigma }_1$ theorem. Soundness and the standard correctness of the predicate would imply that there is an actual $S$-proof of $\neg G$, which was just excluded. ThereforeThe two applications of soundness concern the provability assertions, not the truth of arbitrary arithmetic sentences.

Write $\mathrm{Prf}(n,m)$ for the specified proof relation and $R(n)$ for its Rosser provability predicate. If $R(\overline{n})$ is true in the standard natural numbers, its existential witness $m$ is the code of an actual proof of the expression with code $n$. Thus that expression is provable.

Conversely, suppose an actual proof has code $m$. If Peano arithmetic is consistent, there is no proof of the negation at all, in particular none with code at most $m$. The same $m$ therefore witnesses the bounded proof-order condition as well as the positive proof condition. Henceunder consistency. For numbers that do not code well-formed expressions, neither side holds under the usual proof coding. This is an external equivalence of theoremhood; it does not establish every internal derivability conditions for $R$.

Let $\perp$ abbreviate the fixed false arithmetic equality, and fix an actual proof of $\neg \perp$ with code $m$. For a proposed proof code $y\ge m$, that known proof of the negation already violates the bounded negative-proof test in $R(┌\perp ┐)$.

For the finitely many codes $y<m$, either one is an actual proof of $\perp$, in which case Peano arithmetic is inconsistent and proves the requested conclusion by explosion, or none is. In the latter case the finitely many true bounded facts $\neg \mathrm{Prf}(┌\perp ┐,\overline{y})$ are all provable by bounded completeness. Their conjunction excludes every code below $m$. The positive bounded fact that $m$ proves $\neg \perp$ is likewise provable. Splitting $y<m$ and $y\ge m$ inside arithmetic now givesThus the consistency statement for this Rosser provability predicate is provable. The argument uses only a fixed finite initial segment of proof codes; it does not prove the usual unbounded consistency statement.

The external necessitation rule assertion is valid. Suppose $PA⊢X$ and fix a proof code $m$. If $PA$ is inconsistent the assertion follows by explosion. Otherwise there is no actual proof of $\neg X$. Each of the finitely many bounded checks up to $m$ is therefore a true bounded arithmetic fact and is provable. Together with the positive proof check at $m$ this gives

The requested internal modus-ponens assertion needs an additional coding property. Combining a proof of $X$ and a proof of $X\to Y$ produces a proof of $Y$, but its code can exceed both original codes. The two Rosser hypotheses exclude proofs of $\neg X$ and $\neg (X\to Y)$ only up to their respective witness bounds. They provide no bound excluding proofs of $\neg Y$ below the new proof code. Ordinary internal modus ponens rule for the unbounded provability predicate does not fill this gap.

Consequently the premises printed here do not, just by themselves, justifyThis property varies with the Rosser proof-order dependence: some specially chosen proof predicates satisfy it, while general Rosser proof predicates need not. ^[ref].

The reference to a proof predicate “as given in the course” would need an explicit additional proof-order lemma to establish this part for that particular coding. Standard correctness on numeral instances and the ordinary Hilbert-Bernays-Löb derivability conditions alone are insufficient. The next solution gives the intended argument with the missing condition stated explicitly.

Assume additionally that the internal modus-ponens condition requested in part (c) holds for this $R$. If positive introspection also held for every sentence, then $R$ would satisfy all three Hilbert-Bernays-Löb derivability conditions: external necessitation rule was proved in part (c), modus ponens rule is the added condition, and introspection is the supposition.

The diagonal lemma applies to $R$ just as to any arithmetic formula. The usual Gödel second incompleteness theorem for a predicate with these conditions would then implywhen $PA$ is consistent. Part (b) proves the opposite. Therefore the three conditions cannot all hold, and under the added modus-ponens hypothesis there must be some sentence $X$ such thatThis is the intended contradiction argument and requires no identification of a particular $X$.

Without that extra hypothesis, the valid conclusion is only that at least one of internal modus ponens rule and positive introspection fails. Rosser predicates can be constructed that satisfy positive introspection, so a failure of that condition cannot be inferred from the printed general assumptions alone. ^[ref]. The distinction concerns proof coding, not a missing page of the exam.

Abbreviate the arithmetical provability predicate by $\square$, with the Hilbert-Bernays-Löb derivability conditions understood. Löb's theorem saysChoose a diagonal sentence $D$ with $S⊢D\leftrightarrow (\square D\to A)$. Internalizing its forward implication gives $S⊢\square D\to \square (\square D\to A)$. Internal modus ponens rule gives $\square (\square D\to A)\to (\square \square D\to \square A)$, while positive introspection gives $\square D\to \square \square D$. Combining these yields $S⊢\square D\to \square A$.

Now use the assumed theorem $\square A\to A$. It follows that $S⊢\square D\to A$, and the reverse direction of the diagonal equivalence gives $S⊢D$. External necessitation rule gives $S⊢\square D$, and the previously derived implication gives $S⊢A$. This proves the theorem from the supplied fixed-point property and the derivability conditions.

The Gödel second incompleteness theorem states that a consistent arithmetic theory in this setting cannot prove its own consistency sentence ${\mathrm{Con}}_S=\neg \square \perp$. If it could, it would prove $\square \perp \to \perp$; applying Löb's theorem with $A=\perp$ would make it inconsistent. Therefore $\boxed{S⊬{\mathrm{Con}}_S}$ when $S$ is consistent.

The language of Gödel-Löb logic has propositional variables, $\perp$, implication, and the unary operator $\square$; the other logical connectives are abbreviations. Its axioms are all classical tautologies, the distribution scheme $\square (A\to B)\to (\square A\to \square B)$, and the Löb scheme $\square (\square A\to A)\to \square A$. Its rules are modus ponens rule, necessitation rule of theorems, and uniform substitution.

For a single boxed equation $p\leftrightarrow \square C(p)$, set $F=\square C(\top )$. The identity supplied in the source gives directly $GL⊢F\leftrightarrow \square C(F)$. If $p$ does not occur, take $F=\square C$ instead.

Proceed by induction for a system of $m$ equations, allowing other propositional variables as parameters. Treat $p_1,\dots ,p_{m-1}$ as parameters in the last equation and putThe one-variable result proves $D\leftrightarrow \square C_m(p_1,\dots ,p_{m-1},D)$. Substitute this $D$ for $p_m$ in the first $m-1$ equations. They are still boxed equations, so induction supplies solutions $F_1,\dots ,F_{m-1}$. Define $F_m=D(F_1,\dots ,F_{m-1})$.

By construction, the first $m-1$ equations hold after this substitution; substituting into the theorem for $D$ proves the last. HenceThe elimination introduces no new parameter letters and removes every unknown letter. This gives a constructive simultaneous boxed fixed-point elimination in GL.

Take the outermost boxed subformulas of $X(p)$ containing the distinguished letter. Because $X$ is modalized in $p$, every occurrence of $p$ lies inside one of these boxes. The supplied decomposition therefore has the formwhere $H$ has no occurrence of $p$. Other letters and subformulas not involving $p$ may be retained as parameters in $H$ and the $C_i$.

Introduce temporary letters $q_1,\dots ,q_m$ and solve the boxed systemby part (b), obtaining $Q_i$ without the temporary letters or $p$. Put $F=H(Q_1,\dots ,Q_m)$. Each solved equation gives $GL⊢Q_i\leftrightarrow \square C_i(F)$. The supplied replacement-of-equivalents principle then givesOnly letters already present in $X$, apart from the removed $p$, occur in the constructed $F$. If $p$ is absent from $X$ to begin with, take $F=X$. This is the modalized fixed-point theorem for GL, proved by finite elimination rather than a semantic completeness argument.

One can takeFor the first formula, the Löb axiom with conclusion $\perp$ gives $\square (\square \perp \to \perp )\to \square \perp$, that is, $\square F_1\to \square \perp$. Conversely, the tautology $\perp \to F_1$, necessitation rule, and distribution give $\square \perp \to \square F_1$. Thus $GL⊢\square F_1\leftrightarrow \square \perp$. Negating both sides gives $GL⊢\neg \square F_1\leftrightarrow F_1$.

For the second formula, $\neg F_2=\top$ is a theorem, so $GL⊢\square \neg F_2$. Hence $\neg \square F_2\wedge \neg \square \neg F_2$ is false in the logic and is equivalent to $\perp =F_2$. A fixed point is a formula satisfying the equivalence; it need not itself express a nontrivial undecidable assertion.

A complete theory is $\kappa$-categorical when it has a model with underlying cardinality $\kappa$ and any two of its models of that cardinality are isomorphic structures. Thus categoricity means uniqueness up to isomorphism at the specified cardinal, not a unique underlying set or a unique isomorphism.

For the infinite cardinals relevant here, the existence clause is automatic from the stated infinite model and the Löwenheim-Skolem theorem. One may equivalently require exactly one isomorphism class of models of size $\kappa$.

An $n$-type over the empty set is a set $p(x_1,\dots ,x_n)$ of formulas of the language, with no additional parameters, jointly consistent with $T$. Equivalently every finite set is simultaneously satisfiable with $T$. A complete type decides every formula in these variables: for each $\phi$, exactly one of $\phi$ and $\neg \phi$ belongs to $p$.

A principal type has an isolating formula $\theta (x)$ consistent with $T$, such that $T\models \forall x(\theta (x)\to \phi (x))$ for every $\phi \in p$. For a complete type this is an isolated type; its isolator determines the entire type. A principal partial type may be weaker than a complete type, so its isolator need not decide all formulas.

A tuple $a\in A^n$ realizes $p$ if $\mathcal{A}\models \phi (a)$ for every formula in $p$. The model omits $p$ if it contains no such tuple. Thus omission is a simultaneous failure of realizing the whole type, even though each finite fragment can be realized.

Let $\theta (x)$ isolate the principal type. Consistency with $T$ means $T\cup \{\exists x\theta (x)\}$ is satisfiable. Because $T$ is a complete theory, it must imply $\exists x\theta (x)$; the alternative would make that extension inconsistent.

Therefore every model of $T$ has a tuple $a$ satisfying $\theta$. Each implication $T\models \theta \to \phi$ then makes $a$ satisfy every member of the type. HenceCompleteness is what turns possible realization of the isolating formula into realization in every model.

Add constants $c_1,\dots ,c_n$ and form $T\cup \{\phi (c):\phi \in p\}$. Every finite set has a model by consistency of the type. The compactness theorem gives a model $\mathcal{M}$ realizing the whole expanded theory, so $c^{\mathcal{M}}$ realizes $p$.

Apply the downward Löwenheim-Skolem theorem to the countable expanded language, retaining these finitely many named elements. The resulting countable elementary substructure still satisfies every formula of $p$ at the same tuple. Its reduct to the original language is a countable model of $T$ realizing $p$. Since $T$ has no finite models, this model is countably infinite.

The countable omitting types theorem says that for a consistent theory in a countable language and countably many nonprincipal types of finite arities, there is a countable model omitting all those types. In particular a nonisolated complete type of $T$ can be omitted in a countable model.

Interpret “definable” here as without parameters. If parameters were allowed freely, every infinite structure would have infinitely many definable singleton sets, and the claimed implication would be false even for a dense linear order without endpoints.

Infinitely many distinct parameter-free definable subsets of $A^n$ imply infinitely many complete $n$-types: if there were only $r$ such types, each formula would select a subset of those $r$ types, giving at most $2^r$ distinct definable subsets. There must also be a nonisolated complete type. To see this, suppose each complete type $p$ had an isolator ${\theta }_p$. The family of their basic open sets covers the type space. Its compactness theorem gives a finite subcover, which would account for only finitely many complete types, a contradiction. Equivalently apply logical compactness theorem to $T\cup \{\neg {\theta }_p(c):p\text{ complete}\}$.

Choose a nonisolated type $p$. The omitting types theorem gives a countable model omitting it, while part (d) gives a countable model realizing it. An isomorphism of structures preserves realization of parameter-free types, so these models are not isomorphic. Thus $\boxed{T\text{ is not }{\aleph }_0\text{-categorical}}$.

No. In the standard successor structure, every element other than the named zero has a predecessor:The proposed structure fails this first-order sentence at the integer $-1$. Its nonnegative elements map to positive elements, while every negative element maps to an integer at most $-2$; hence no element maps to $-1$. This gives a direct first-order distinction, without treating the negative branch as a two-sided successor chain.

Take the standard successor structure and its disjoint union with one two-sided integer successor chain:Both interpret the named zero in the natural-number component. The classification of models of the successor theory describes every model as this distinguished one-sided chain together with an arbitrary collection of two-sided chains. Its axioms are injectivity of $s$, zero outside its range, a predecessor for every nonzero element, and absence of finite cycles. These axioms are complete; equivalently the theory has the successor quantifier-elimination property explained in the concept proposal.

Consequently both displayed structures are models of the standard complete theory. They are not isomorphic: any isomorphism must fix zero and hence every element $s^n(0)$. The first structure has no other elements; the second has the entire extra integer chain. Being in that additional component is an isomorphism invariant even though being outside all standard iterates of zero is not expressible by one first-order formula.

For each natural number $n$, the formula $x=s^n(0)$ defines the singleton $\{n\}$ in the standard successor structure. These are pairwise distinct parameter-free definable subsets. ThereforeIn particular the criterion in part (e) applies already at arity one.

Consider the partial typeEach finite fragment is realized by a sufficiently large standard natural number, so it is consistent. It is omitted in the standard successor structure, since each of its elements equals one of the named iterates.

There is exactly one complete type extending this partial type. By classification of models of the successor theory and its quantifier-elimination property, a parameter-free one-variable formula is equivalent to a Boolean combination of finitely many equalities $x=s^n(0)$ and sentences whose truth is fixed by the theory. For a point on an extra integer chain every displayed equality is false, so all such points have the same complete type. Thusis the required omitted complete type. More formally take all formulas true at such a point; $p_{\infty }$ axiomatizes that type modulo the theory, and its deductive closure is complete.

The distinguished chain generated by zero is countable, and every other component in the classification of models of the successor theory is a countable copy of the integer successor chain. A model of cardinality ${\aleph }_1$ therefore has exactly ${\aleph }_1$ additional components: a finite or countable collection would be countable, while the union of $\kappa$ countable components has size $\max (\kappa ,{\aleph }_0)$.

Given two such models, match their zero chains in the forced way and choose a bijection between their additional components. On each component choose an origin and match corresponding integer iterates; this commutes with successor. The union of these maps is an isomorphism of structures. Existence is given by a disjoint union with ${\aleph }_1$ integer chains. HenceThe same argument works at every uncountable cardinal. Countable models can still differ by the number of extra components, as part (ii) shows.

A term-generated model is a structure in which every element is the value of a closed term of the original language. Equivalently its substructure generated by the empty set, including interpretations of named constants, is the entire structure. This is the relevant meaning of “term model” for a model of an arbitrary complete theory, rather than a claim about one particular syntactic construction.

Each closed term $t$ gives the parameter-free defining formula $x=t$. ThusThe next parts show that pointwise definability implies atomicity, and countable atomicity is equivalent to primeness. Therefore property (i) implies all three other properties.

An element $a$ is parameter-free definable if some formula $\theta (x)$ of the original language has $a$ as its unique solution in the structure. Saying this for every element makes the model pointwise definable.

If a finite tuple has individually defining formulas, their conjunction uniquely defines that tuple. Its complete type is isolated by this conjunction: for each formula $\phi$, the sentence saying the unique tuple does or does not satisfy $\phi$ is decided by the complete theory. ThusIt follows that the countable model is also prime. The converse implication to property (i) fails. In $(\mathbb{N},<,0)$ every element is defined by having exactly $n$ predecessors, but the only closed term in this language is the constant $0$. This infinite model is pointwise definable and is not term-generated.

An atomic model is a model in which every finite tuple realizes an isolated complete type over the empty set. For a complete theory in a countable language, every countable atomic model is prime. The underlying argument is a back-and-forth method in the one-sided form needed for an embedding: enumerate the atomic model, and extend a finite partial elementary map one element at a time using an isolating formula for the enlarged tuple. The target model has the required witness because the already matched tuple has the same complete type.

Thus property (iii) implies property (iv). It need not imply pointwise definability or term-generation. The countable dense linear order without endpoints with a single named point, for example $(\mathbb{Q},<,0)$, is atomic: quantifier elimination for dense linear orders without endpoints isolates a tuple by its finite order-and-equality pattern relative to zero. But order structure automorphisms fixing zero move every nonzero rational. Such elements are not parameter-free definable, and no closed term names them. This supplies the failed implications (iii)$\nRightarrow$(ii) and (iii)$\nRightarrow$(i).

A prime model admits an elementary embedding into every model of its complete theory. In the countable setting a prime model is atomic. If a tuple in the prime model had a nonisolated complete type, the omitting types theorem would give a model omitting that type; an elementary embedding of the prime model into it would realize the omitted type, a contradiction.

Combining the four parts, all positive implications are exactly those generated byThe structure $(\mathbb{N},<,0)$ refutes (ii)$\Rightarrow$(i). The structure $(\mathbb{Q},<,0)$ is a countable atomic and hence prime model of its complete theory, while failing both (i) and (ii); it refutes every remaining reverse arrow, including (iv)$\Rightarrow$(i) and (iv)$\Rightarrow$(ii). The counterexamples therefore cover all ordered pairs of distinct properties not forced by the boxed chain.

An omega-saturated model realizes every complete type of a finite tuple over every finite set of its domain. It suffices to require this for one-variable types: realize the coordinates successively, enlarging the finite parameter set at each step.

Every complete theory here has such a model, with no countability requirement on its size. Start with a model of size at most $\lambda =2^{{\aleph }_0}$. There are at most $\lambda$ types over its finite sets, because the language is countable and each such type is a set of formulas in a countable collection. By the compactness theorem and the elementary diagram construction, pass to an elementary extension realizing all these types, keeping size at most $\lambda$ by the Löwenheim-Skolem theorem.

Repeat this for stages $0,1,2,\dots$ and take the union of the elementary chain. Any finite parameter set in the union lies in some stage, and every type over it is realized at the next stage. The union is therefore omega-saturated. Countable language does not by itself guarantee that a countable saturated model exists.

Yes. The pure order on the reals is a dense linear order without endpoints and has quantifier elimination for dense linear orders without endpoints. Over a finite parameter set $a_1<\cdots <a_m$, a complete one-variable type either specifies equality to one of these points or specifies one of the open intervals and exterior rays they determine.

Each such interval or ray contains a real number. Hence every complete one-variable type over a finite parameter set is realized. The successive-coordinate characterization gives saturation for all finite tuples. This uses finite parameter sets; it does not say that arbitrary types over a countably infinite set of parameters are realized.

Yes. As an Abelian group, the reals are a nontrivial torsion-free divisible group, equivalently a vector space over the rationals. Rational scalar multiplication is uniquely definable by equations such as $ny=mx$, so adding those operations is a definitional expansion.

In this language, quantifier elimination for torsion-free divisible Abelian groups reduces formulas to Boolean combinations of rational linear equations. Over finitely many parameters, a complete one-variable type either fixes a value in their linear span or excludes every value in that span. The first kind is realized in the span itself; the second is realized by any real number outside it. That span is countable, while the reals are uncountable. Thus every such type is realized and the additive real group is an omega-saturated model.

For finite tuples, the same argument successively supplies any required finite number of new rationally linearly independent elements. The order and multiplication of the real field are absent from this language, so they cannot impose additional type conditions.

No. The parameter-free partial typeis finitely satisfiable in the ordered real field: choose a number larger than the finitely many bounds. By compactness theorem it extends to a complete type over the empty set. But no real number realizes it, by the Archimedean property. Therefore the ordered real field is not an omega-saturated model.

The named unit and addition make every integer bound expressible, even without extra parameters. This is why the obstruction is present in the ordered-field language and absent in the two reducts above.

Suppose $T$ is an omega-categorical theory. By the Ryll-Nardzewski theorem, every finite-arity complete type over the empty set is isolated. Let $p(x,a)$ be a complete type over a finite tuple in the unique countable model $M$, and take an elementary extension realizing it at $b$. The joint type of $(b,a)$ is isolated by a formula $\theta (x,y)$.

The complete type of $a$ contains $\exists x\theta (x,y)$, since this formula is true of $a$ in the extension. Hence it is true of $a$ in $M$, and some $b^{\prime }\in M$ satisfies $\theta (b^{\prime },a)$. Isolation of the joint type implies that $b^{\prime }$ realizes $p$. Thus the countable model is an omega-saturated model.

The converse fails. The complete successor theory from question 4 has a countable modelwith countably infinitely many two-sided successor components. It is omega-saturated. Over finitely many parameters, a complete one-variable type either fixes a finite successor/predecessor translate of a parameter or zero, or asks for a point in no component represented by those parameters and zero. The first kind is realized in the named component, and the second in an unused integer component. The quantifier-elimination description of classification of models of the successor theory shows there are no other cases.

Nevertheless this theory is not omega-categorical: $M$ and its standard model $\mathcal{N}$ are countable and not isomorphic. Thus existence of a countable saturated model is strictly weaker than countable categoricity.

Expand the language by a constant $c_a$ for every element of the structure. Its diagram of a structure consists of all atomic and negated atomic sentences true in this expanded structure. Its elementary diagram, also called the complete diagram, consists of all first-order sentences true in the expansion.

For a model $M$ of the diagram, the map $a\mapsto c_a^M$ is injective because the diagram includes all required inequalities. It preserves functions and constants by the corresponding equations, and it preserves and reflects relations by the positive and negative atomic sentences. Thus it is a structure embedding onto a substructure of the reduct of $M$. Conversely, a structure containing an isomorphic copy of the original as a substructure can interpret the new constants at that copy and satisfy its diagram.

For the elementary diagram the same argument works for every formula, not just atomic ones. The map is therefore an elementary embedding. Conversely any elementary embedding gives an expansion satisfying the elementary diagram. These are characterizations up to the named copy; a model of either diagram may have additional unnamed elements.

For a structure in a countable language and any subset $C$ of its domain, there is an elementary substructure containing $C$ of cardinality at most $\max (|C|,{\aleph }_0)$. In particular a finite or countable $C$ lies in a countable elementary substructure. This is the downward Löwenheim-Skolem theorem.

Construct it directly inside the given structure $A$. Start with $C_0$ containing $C$, the interpretations of the constants, and one element if needed to ensure a nonempty domain. Given $C_n$, for every formula $\exists x\phi (x,a)$ with its finite parameter tuple from $C_n$ that is true in $A$, choose one actual witness in $A$ and place it in $C_{n+1}$. Retain $C_n$ as well. There are at most $\max (|C|,{\aleph }_0)$ choices at each stage. Let $B={\bigcup }_{n<\omega }{C}_n$.

The construction closes $B$ under every function of the language: for a tuple in $C_n$, the formula $x=f(a)$ forces its unique value into the next stage. Thus $B$ carries the induced substructure, and it has the asserted cardinal bound.

Prove elementarity by structural induction. Atomic formulas agree by the induced-substructure construction; logical connectives preserve agreement. For an existential formula with parameters in $B$, if it is true in $A$, all its parameters occur in some $C_n$, so the chosen witness lies in $C_{n+1}\subseteq B$. The induction hypothesis makes its matrix true in $B$. In the other direction a witness in $B$ is also a witness in $A$, again by induction. This is the Tarski-Vaught test, with its witness argument proved explicitly. No completeness or compactness theorem theorem enters the construction.

Skolem's paradox is the apparent conflict between a countable model of a sufficiently strong set theory and that model's theorem asserting the existence of uncountable sets. Downward Löwenheim-Skolem theorem gives a countable elementary model whenever an appropriate infinite model exists; internally the same model still proves, for example, that its real-number set is uncountable.

The two uses of “countable” quantify over different collections of functions. Externally the whole model, and therefore the elements it regards as members of its real-number set, can be enumerated. Internally a set is countable only if an enumerating function exists among the sets of the model. The external enumeration need not be an element of the model.

Thus there is no contradiction: the model's assertion is that no function it contains is the required enumeration. Cantor's theorem remains valid inside the model. The model need not be transitive or have the actual standard natural numbers for this explanation; the essential issue is the restriction of internal quantifiers to its own domain.

For the pure orders, yes. Both structures satisfy the theory of dense linear orders without endpoints. By quantifier elimination for dense linear orders without endpoints, each formula is equivalent to a quantifier-free order formula. Inclusion of the rationals into the reals preserves and reflects all such formulas, hence is elementary:

With a common named unit, yes. In general an elementary substructure remains elementary when elements already in the substructure are named by new constants. A formula using the new constant is just an old-language formula with that common element as a parameter. Since $1\in \mathbb{Q}$, this applies directly.

With the real constant interpreted by $\pi$, no choice inside the rationals works for inclusion. A substructure embedding must preserve every constant. The inclusion would send a rational interpretation $q$ to that same real $q$, whereas the target constant is $\pi \notin \mathbb{Q}$. Thus the expanded rational structure is not even a substructure of the expanded real one.

This last failure concerns the specified inclusion. There is an abstract elementary embedding carrying a chosen rational $q$ to $\pi$: the increasing map $r\mapsto r+\pi -q$ has that property, and its image is a dense order without endpoints inside the reals. Quantifier elimination makes the embedding elementary, but its image is a translated copy of the rationals rather than the original rational subset.

This University of Oxford Part C paper covers Gödel's Incompleteness Theorems in section A and Model theory in section B, cross-listed for Mathematics, Mathematics and Computer Science, and Mathematics and Philosophy. ^[ref] The archive contains the complete editable five-page transcription. Bounded official-source searches found no advertised answers for this exact paper. A2(c) is answered with a counterexample to its literal semantic hypothesis and a proof of the intended canonical case. The vector-space comparison keeps infinitude of the underlying set distinct from infinite dimension.

Write $\square A$ for the arithmetical sentence asserting $S$-provability of $A$. If $S⊢G$, the first derivability condition gives $S⊢\square G$. The stipulated fixed-point equivalence also gives $S⊢\neg \square G$. This contradicts consistency. Conversely an inconsistent classical theory proves every sentence, including $G$. ThusOnly the direction from an actual proof to its formalized provability is used here. There is no inference from a theorem $\square G$ to a theorem $G$, and no assumption that every theorem of $S$ is true.

The Hilbert-Bernays-Löb derivability conditions are: if $S⊢A$ then $S⊢\square A$; $S⊢\square (A\to B)\to (\square A\to \square B)$; and $S⊢\square A\to \square \square A$. The first is an external rule about provability; the latter two are internal theorems. Standard numerical correctness and the stipulated ${\Sigma }_1$ form accompany the predicate in this question. These conditions do not include reflection $\square A\to A$.

Choose a fixed refutable sentence $\perp$ and identify ${\mathrm{Con}}_S$ with $\neg \square \perp$. Different fixed refutable choices have provably equivalent consistency sentences, because $S$ proves their equivalence to a contradiction. From $\perp \to G$, necessitation and distribution give $\square \perp \to \square G$. Since $G\to \neg \square G$, this yields $G\to {\mathrm{Con}}_S$.

For the converse, necessitate $G\to \neg \square G$ and distribute to get $\square G\to \square \neg \square G$. Positive introspection also gives $\square G\to \square \square G$. The two boxed contradictories imply $\square \perp$ by formalized propositional reasoning. Thus $\square G\to \square \perp$, and contraposition gives ${\mathrm{Con}}_S\to \neg \square G\to G$. ConsequentlyFinally the deduction theorem says that $S+G$ is inconsistent exactly when $S⊢\neg G$. The internal equivalence identifies $S+G$ and $S+{\mathrm{Con}}_S$ in their deductive consequences. Hence $S⊬\neg G$ exactly when $S+{\mathrm{Con}}_S$ is consistent. Consistency of $S$ alone need not ensure this stronger consistency condition.

For consistency of a negated-consistency extension, put $A=S+\neg {\mathrm{Con}}_S$. The arithmetized deduction theorem, together with double-negation elimination and formalized proof transformations, givesFrom the preceding proof, $S⊢{\square }_{S}G\to {\square }_S\perp$. Necessitating the equivalence between $G$ and ${\mathrm{Con}}_S$ and using distribution therefore gives $S⊢{\square }_S{\mathrm{Con}}_S\to {\square }_S\perp$. Its contrapositive isThis is an internal conditional statement. It does not assert that $S$ proves its own consistency or permits the consistency premise to be discarded.

For unrestricted consistency self-strengthening is inconsistent, again take $A=S+\neg {\mathrm{Con}}_S$. In $S^{++}$ the axiom ${\mathrm{Con}}_S$ and the preceding implication prove ${\mathrm{Con}}_A$. The additional rule then proves ${\mathrm{Con}}_{A+{\mathrm{Con}}_A}$.