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.

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.

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.

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$.

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.

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.

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

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.

An ${\aleph }_0$-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 $M$, 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 $M$: 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 $M_0\models T$ and apply this construction repeatedly to obtain $M_0\preccurlyeq M_1\preccurlyeq \cdots$, with each successor realizing all types over finite subsets of its predecessor. The elementary-chain theorem makes $M_{\omega }={\bigcup }_n{M}_n$ a model of $T$ with every stage elementary in it. A finite parameter set $A\subseteq M_{\omega }$ lies in some $M_n$. Every type over $A$ consistent with $M_{\omega }$ is consistent with $M_n$, since the expanded complete theories at those parameters agree by elementarity. It is realized in $M_{n+1}$, hence in the union. Therefore an ${\aleph }_0$-saturated model always exists, possibly with uncountable cardinality.

A model is prime if it has an elementary embedding into every model of $T$. A model is atomic if every finite tuple realizes an isolated complete type over the empty set.

If $A$ is prime, the downward Löwenheim-Skolem theorem gives a countable model $M$ of $T$, and an elementary embedding $A\to M$ makes $A$ countable. If a tuple of $A$ realized a nonisolated type, the omitting types theorem would give a model of $T$ omitting that type. The prime embedding into it would preserve the tuple's full type and realize the omitted type, a contradiction. Thus a prime model is countable and atomic.

Conversely enumerate a countable atomic model as $a_0,a_1,\dots$, and take any $B\models T$. Build finite partial elementary maps into $B$. Suppose the current tuple $\bar{a}$ maps to $\bar{b}$. Choose a formula $\theta (\bar{x},y)$ isolating the type of $(\bar{a},a_n)$. The assertion $\exists y\theta (\bar{a},y)$ holds in $A$, so its counterpart holds at $\bar{b}$ in $B$ by partial elementarity. Choose a witness $b_n$. Since $\theta$ isolates the entire extended tuple type, the extended map is elementary on its finite domain; its equality formulas ensure distinct Elements remain distinct. The union is a total elementary embedding $A\to B$. The empty initial tuple works because $T$ is complete. Hence

A complete $n$-type over $T$ is a maximal set $p(\bar{x})$ of formulas in $n$ variables consistent with $T$; 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 $\theta (\bar{x})$ consistent with $T$ implies every member of the type modulo $T$; then $\theta$ 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.

The cardinality of a vector space is central: here “infinite” must continue to refer to the underlying set. Over a countably infinite field, every nonzero finite-dimensional space is already infinite. Thus the model class now consists of all nonzero $K$-vector spaces, not only infinite-dimensional ones.

Since independence of a pair is not definable over an infinite field, for (i), independence of a single vector is still $x\ne 0$, but independence of tuples of length at least two is not definable by one formula in this one-sorted language. Quantifier elimination follows from the linear-equation argument in the preceding part for all these infinite domains. Any candidate two-variable formula therefore involves only finitely many linear equations. Take an independent pair, and compare it with $(x,{\lambda }_{a}x)$, where $x\ne 0$ and $a\in K$ avoids the finitely many ratios making one of those nontrivial equations vanish. Both pairs satisfy the same listed atomic formulas, contradicting a proposed definition of independence. Longer tuple independence would define pair independence by existentially completing a pair inside an infinite-dimensional model, giving the same obstruction.

For (ii), the vector-space axiom schema together with $\exists x(x\ne 0)$ axiomatizes the infinite underlying spaces. For (iii), there is again no universal axiomatization, because the zero subspace is a substructure.

For finite axiomatizability with infinitely many scalar symbols, in (iv) there is no finite axiomatization in the full language: any finite axiom set mentions only finitely many scalar symbols. In a nonzero vector space alter an unused nonzero ${\lambda }_a$ to send zero to a nonzero vector, retaining all mentioned interpretations. The finite sentences keep their truth values, but a vector-space axiom is now false. Relative to the already imposed vector-space axioms, the extra condition is finitely axiomatized by the single nonzero-vector sentence. These absolute and relative answers must be distinguished.

For (v), the one-variable algebra still has two atoms and four Elements. In two variables the isolated atoms are $(0,0)$ and the countably many rank-one directions, represented by $x\ne 0,y={\lambda }_{a}x$ and by $x=0,y\ne 0$. There is also a nonisolated complete type of an independent pair. A formula using finitely many linear equations either picks finitely many isolated atoms, or contains that independent type and all but finitely many isolated atoms. Therefore $F_2/E_2(T)$ is the finite-cofinite Boolean algebra on a countably infinite set of atoms, with the independent type the extra nonisolated point in its Stone space. In particular this algebra is countably infinite, rather than the full power set of its atoms.

For (vi), dimension can be $1,2,3,\dots$ or ${\aleph }_0$ while the domain is countable, producing pairwise nonisomorphic countable models. Thus $T$ is not countably categorical. For an uncountable $\kappa$, a vector space over this countable field has cardinality $\kappa$ exactly when its dimension is $\kappa$, since in general a nonzero space has size $\max (|K|,\dim V)$ when that maximum is infinite. Basis bijections then give categoricity in every uncountable cardinal. Quantifier elimination also shows that these different positive dimensions are elementarily equivalent; independence of an arbitrarily long tuple is not being silently treated as definable over this infinite field.