= Solution
<Omega-consistency> forbids a <logical formula> $B(x)$ of any complexity for which $S\vdash\exists xB(x)$ and $S\vdash\neg B(\bar n)$ for every standard $n$. The difference from <one-consistency> is that the matrix is unrestricted. It implies <first-order consistency>.
For a complete <first-order consistent> classical <first-order theory>, theorem membership obeys the ordinary Boolean <truth tables>. For example, it proves a <conjunction> exactly when it proves both conjuncts; completeness and <first-order consistency> also make theoremhood of a <negation> the complement of theoremhood of the <first-order sentence>. <Omega-consistency> additionally gives the witness property
$$
S\vdash\exists xB(x)\quad\Longleftrightarrow\quad
S\vdash B(\bar n)\text{ for some standard }n.
$$
The reverse implication is existential introduction. For the forward implication, if no standard instance were provable, completeness would give a <formal proof> of each negated instance, violating <omega-consistency>. This works also after replacing additional <free variables> by numerals.
Now induct on <logical formulas> with their remaining <free variables> replaced by standard numerals. At the atomic level, the equivalence between theoremhood and standard truth follows from <bounded completeness of an arithmetic theory> and bounded <soundness of an arithmetic theory> from (b). The Boolean steps use the truth-table facts just proved. The existential step uses the witness property and the <induction> hypothesis on its matrix; <universal quantification> follows by <negation>. Hence
$$
\boxed{S\vdash X\quad\Longleftrightarrow\quad\mathbb N\models X}
$$
for every <first-order sentence> $X$. Completeness ensures it decides each <first-order sentence>, and this equivalence ensures every decision is correct.
Back to article page
