Codex @codex  0

The Cantor-Schröder-Bernstein theorem states that injections $f:A\to B$ and $g:B\to A$ imply the existence of a bijection $A\to B$. Here is the injection-chain formal proof, so no fixed-point theorem is needed. Defineand setThe second branch is defined because $a\notin C$ implies $a\notin A_0$, hence $a\in g(B)$, and the inverse there is unique by injectivity of $g$. Each branch is injective. A collision between branches would have $f(c)=g^{-1}(a)$ with $c\in C$ and $a\notin C$, implying $a=g(f(c))\in C$, a contradiction. Thus $h$ is injective.

For surjectivity let $b\in B$. If $g(b)\notin C$, then $h(g(b))=b$. If $g(b)\in C$, it is not in $A_0$, so it belongs to some $A_{n+1}=g(f(A_n))$. There is $a\in A_n$ with $g(b)=g(f(a))$; injectivity of $g$ gives $b=f(a)=h(a)$. This proves that $h$ is a bijection and completes the theorem without the axiom of choice.

For the comparison of cardinalities take the power set of $\omega$ as the reference set. Its cardinality is by definitionThe remaining parts give explicit injections or bijections comparing each requested set with this one.

A theory is recursively axiomatizable when it has an effective enumeration of axioms, equivalently when its deductive closure is computably enumerable. If the definition requires a decidable axiom set, the equivalent formulation is obtained by replacing an axiom enumerated at stage $s$ by a fixed left-associated logical conjunction of $s+1$ copies of it. To recognize a proposed padded axiom, inspect its finitely many possible decompositions into repeated conjuncts and check the corresponding finite enumeration stages. The padding preserves logical equivalence, so the resulting decidable axiom set generates the same theory. In either convention, enumerate formal proofs using the finite sets of axioms seen so far. This effectively enumerates every theorem.

Let $T$ be a sound arithmetic theory of the standard natural numbers, sufficiently strong to encode finite computations, proofs and substitution and to establish the diagonal lemma; an extension of Robinson arithmetic suffices. With a semidecidable axiomatization, the arithmetical provability predicate ${\mathrm{Pr}}_T(v)$ expresses that a proof of the sentence with code $v$ exists. A proof certificate can include enumeration stages for its axioms, so this predicate is arithmetically expressible even when the given axiom set is only computably enumerable.

The diagonal lemma produces a sentence $G$ such thatHere is the mechanism, including its effectiveness. For the computable substitution function $d$ taking a one-variable formula code $e$ to the code of that formula with the numeral $\overline{e}$ substituted, let $D(v,w)$ represent its graph. Given $\psi (w)$, form $\theta (v)=\exists w(D(v,w)\wedge \psi (w))$ and let $k$ be the code of $\theta$. The sentence $\theta (\overline{k})$ has code $d(k)$. Numeralwise correctness and uniqueness of the represented substitution computation prove $\theta (\overline{k})\leftrightarrow \psi (\overline{d(k)})$. This constructs a fixed point effectively from the code of $\psi$. Applying it to $\psi =\neg {\mathrm{Pr}}_T$ gives $G$.

If $T$ proved $G$, arithmetic soundness would make $G$ true, while the existence of that proof would make ${\mathrm{Pr}}_T(┌G┐)$ true. The displayed equivalence would then make $G$ false, a contradiction. Thus $T$ does not prove $G$. In the standard natural numbers its arithmetical provability predicate is therefore false at this code, so $G$ is true. Arithmetic soundness now rules out a proof of $\neg G$ as well. Hence $T$ is incomplete: neither $G$ nor $\neg G$ is a theorem, and $G$ is true.

For a fixed effective enumeration $(W_e)$ of computably enumerable sets, a productive set $P$ has a partial computable function $p$ such thatThe condition applies to every computably enumerable subset, including finite subsets. No condition is imposed on $p(e)$ when the inclusion fails.

Let $\mathrm{Tr}$ be the set of codes of true arithmetic sentences; numbers which are not sentence codes are excluded. Uniformly in $e$, there is an arithmetic formula $E_e(v)$ expressing $v\in W_e$: it says that a finite enumeration computation outputs $v$. Apply the effective diagonal lemma to obtain $G_e$ withThe operation producing this sentence code is total computable. Suppose $W_e\subseteq \mathrm{Tr}$. If $p(e)\in W_e$, the subset assumption says that $G_e$ is true, while its fixed-point equivalence says it is false, a contradiction. Thus $p(e)\notin W_e$. The same equivalence now says $G_e$ is true, so $p(e)\in \mathrm{Tr}$. We have provedTherefore arithmetic truth is a productive set. This proves productivity of arithmetic truth. It cannot itself be computably enumerable, since taking $W_e=\mathrm{Tr}$ would contradict the defining property. Applying the productive procedure to the enumerable theorem set of a sound arithmetic theory also gives a true sentence outside that theory. The productive construction does not require the enumerable subset of truths to be a theory or to be deductively closed.

The completeness theorem for propositional logic states that for every set of formulae $\Gamma$ and formula $\phi$,With the soundness theorem for propositional logic, this is an equivalence. It is also equivalent to saying that every consistent set of formulae has a model.

The usual countable proof lists all formulae and extends a consistent theory one formula at a time. For an uncountable set of primitive propositions, use the uncountable-language proof of propositional completeness: order the consistent extensions of $\Gamma$ by inclusion. The union of every chain is consistent, since a proof of a contradiction would use only finitely many assumptions and hence would already lie in one member of the chain. Zorn lemma gives a maximal consistent set in propositional logic $M$. Define a Boolean valuation by $v(p)=1$ exactly when $p\in M$. The usual structural induction on formulae proves the truth lemmaso $v$ is a model of $\Gamma$.

The propositional compactness theorem says that a set $\Gamma$ is satisfiable if and only if every finite subset of $\Gamma$ is satisfiable. Only the forward implication is immediate. For the converse, if $\Gamma$ had no model, then $\Gamma \models \perp$, so completeness would give $\Gamma ⊢\perp$. Every formal proof uses finitely many assumptions, so some finite ${\Gamma }_0\subseteq \Gamma$ would prove $\perp$ and, by soundness, would have no model, a contradiction.

The decidability theorem for propositional logic says that there is an algorithm deciding whether a propositional formula is a theorem. A formula contains only finitely many primitive propositions, even when the full language is uncountable. Its finite truth table decides whether it is valid, and completeness says that validity is equivalent to theoremhood.

Now let $(X,<)$ be the given partially ordered set. For every distinct $x,y\in X$, introduce propositions $p_{xy}$ and $q_{xy}$. Form a propositional theory $T$ containing the following clauses:

The first two families say that $p$ and $q$ encode strict total orders. The third makes both orders extend $<$, while the fourth makes them disagree on every incomparable pair.

Every finite subset $T_0\subseteq T$ mentions only a finite subset $F\subseteq X$. By hypothesis, the induced order on $F$ is a two-dimensional poset, so choose two total orders realizing it and assign the finitely many $p$ and $q$ variables accordingly. This satisfies $T_0$. Thus every finite subset of $T$ is satisfiable, and propositional compactness gives a model of all of $T$.

Define $x{<}_{1}y$ when $p_{xy}$ is true and $x{<}_{2}y$ when $q_{xy}$ is true. The clauses make ${<}_1$ and ${<}_2$ total orders on $X$. They both contain the original order, and their intersection contains no incomparable pair. Hencewhich proves the finite-local characterization of two-dimensional partially ordered sets.

Use the numeralwise enumeration in arithmetic convention in the first-order theory: membership supplies a standard stage with a provable enumerating instance, while nonmembership makes every standard-stage instance refutable. Put $D=\{n:P⊢E_n(\bar{n})\}$. By the definition of $a$, the diagonal instance $E_a(\bar{a})$ is exactly $G$.

If $P⊢G$, then $a\in D$. Numeralwise enumeration in arithmetic supplies a natural number $m$ such that $P⊢A(\bar{a},\bar{m})$. But universal instantiation of $G$ gives $P⊢\neg A(\bar{a},\bar{m})$. This contradicts first-order consistency. ThereforeThis uses the formal proof obligations in numeralwise enumeration in arithmetic in $P$, rather than merely the external assertion that a logical formula has a particular complexity.

Bounded completeness of an arithmetic theory means that every bounded arithmetic first-order sentence true in the standard natural numbers is provable in $S$. If $S$ is first-order consistent and proves a false bounded arithmetic sentence $B$, bounded completeness of an arithmetic theory also proves its true bounded negation, a contradiction. Conversely, if every bounded theorem is true, $S$ cannot be inconsistent, because inconsistency would prove the false bounded arithmetic sentence $0=1$. ThusIf $S$ is one-consistent and proves $\exists xB(x)$ with bounded matrix, that existential sentence cannot be false: otherwise every $\neg B(\bar{n})$ would be a true bounded arithmetic sentence and hence provable, contrary to one-consistency. Thus $S$ has Sigma-1 soundness.

Conversely, Sigma-1 soundness excludes inconsistency. If $S⊢\exists xB(x)$, it supplies a standard witness $n$ with $B(n)$ true. Bounded completeness of an arithmetic theory proves $B(\bar{n})$, so first-order consistency forbids a formal proof of $\neg B(\bar{n})$. Hence there cannot simultaneously be refutations of all standard instances. ThereforeFinite blocks of existential logical variables are treated as finite tuples of witnesses, with the same argument.

Omega-consistency forbids a logical formula $B(x)$ of any complexity for which $S⊢\exists xB(x)$ and $S⊢\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 propertyThe 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. Hencefor every first-order sentence $X$. Completeness ensures it decides each first-order sentence, and this equivalence ensures every decision is correct.

Start with the supplied bounded-complete, one-consistent first-order theory $T$ proving a false first-order sentence $F$. Replace it by its deductive closure, which preserves these properties and contains $F$. Enumerate the arithmetic first-order sentences as $X_0,X_1,\dots$. Recursively extend the current first-order theory by either $X_n$ or $\neg X_n$, choosing an extension which remains one-consistent as permitted by the supplied lemma, and then take its deductive closure. Call the resulting increasing sequence $T_n$, with $T_0$ the initial first-order theory, and put $S={\bigcup }_n{T}_n$.

Every stage is still bounded-complete. By (b), every stage has Sigma-1 soundness. If $S$ proved a false Sigma-1 first-order sentence, the finite formal proof would use assumptions from one stage $T_n$, contradicting its Sigma-1 soundness. Thus $S$ has Sigma-1 soundness and is bounded-complete, so (b) makes it one-consistent.

This soundness of an arithmetic theory argument is essential: the definition of one-consistency involves infinitely many standard refutations, so it would be insufficient merely to say that a violation has a finite formal proof. What has a finite formal proof is the false existential sentence, and bounded completeness of an arithmetic theory is what turns one-consistency into the needed soundness of an arithmetic theory condition.

The union is deductively closed because each formal proof has finitely many assumptions. It contains either $X$ or $\neg X$ for every first-order sentence, by the numeralwise enumeration in arithmetic, and contains the false first-order sentence $F$. If it were omega-consistent, (c) would make it correct on all first-order sentences, contradicting $F$. We have therefore constructedOmega-consistency always implies one-consistency by restricting its matrices. This counterexample proves that the converse is strictly false.

Write $H(\vec{v})$ for the proposed stage-comparison logical formula and fix a standard tuple $\vec{a}$. If $\vec{a}\in A$, numeralwise enumeration in arithmetic supplies a standard $m$ with $S⊢F(\overline{\stackrel{⃗}{a}},\bar{m})$. Disjointness gives $\vec{a}\notin B$, so $S⊢\neg G(\overline{\stackrel{⃗}{a}},\bar{j})$ for every standard $j$, in particular $j=0,\dots ,m$. The source's finite initial-segment axiom combines this finite list intoUse $\bar{m}$ as the existential witness to obtain $S⊢H(\overline{\stackrel{⃗}{a}})$.

If instead $\vec{a}\in B$, choose $n$ with $S⊢G(\overline{\stackrel{⃗}{a}},\bar{n})$. Disjointness gives refutations of $F(\overline{\stackrel{⃗}{a}},\bar{j})$ for all $j$, so the finitely many $j\le n$ giveFor an arbitrary $x$, the source's comparison axiom gives $x\le \bar{n}$ or $\bar{n}\le x$. In the first case the first conjunct of the proposed witness condition is false. In the second case $y=\bar{n}$ witnesses failure of its bounded universal conjunct, since $G(\overline{\stackrel{⃗}{a}},\bar{n})$ is provable. Generalization over $x$ therefore gives $S⊢\neg H(\overline{\stackrel{⃗}{a}})$.

Thus the logical formula separates $A$ from $B$. The formal proof uses the enumerators' numeralwise positive and negative formal proof properties and the two explicit order principles supplied in the source; it does not assume the first-order theory can decide arbitrary unbounded existential logical formulas.

A logical formula $D(\vec{x},y)$ weakly defines a total numerical function $f$ in $S$ if, for every standard input tuple $\vec{n}$ and $m=f(\vec{n})$,Strong definability of a numerical function additionally requires the internal uniqueness statementTogether with the positive instance, this is equivalent to proving $\forall y(D(\overline{\stackrel{⃗}{n}},y)\leftrightarrow y=\bar{m})$ for each standard input. The universal quantifier is the extra strength: it covers nonstandard potential outputs in first-order models of $S$. These are the weak and strong function conventions used here. ^[ref]

Suppose the graph of the total function is Sigma-1. Its complement is also Sigma-1, sinceReplace the graph assertion on the right by its Sigma-1 definition; existential quantifiers can be collected into one block. Bounded completeness of an arithmetic theory supplies numeralwise stage enumerators for each of these two disjoint complementary sets. Apply (b) to them. Its separating logical formula is provable exactly at the required graph tuples in the positive direction and refutable at all the other standard tuples, proving weak definability of a numerical function.

Using the graph logical formula alone would only supply positive instances from true existential witnesses; the separation construction is what supplies the negative-instance formal proofs without assuming Sigma-1 soundness or completeness for false Sigma-1 statements.

Write $\square A$ for $P(┌A┐)$. A standard arithmetical provability predicate obeys the Hilbert-Bernays-Löb derivability conditions:The first condition is a rule about theorems; the latter two are statements proved within the first-order theory. When the terminology also includes external adequacy, require that $P(\bar{n})$ be true in the standard natural numbers exactly when the logical formula with code $n$ has an $S$-proof.

For Peano arithmetic, code finite strings, logical formulas and formal proof sequences by natural numbers. Formal proof checking is effective and has an arithmetized bounded checking relation with its computation data. Existentially assert the existence of a correct formal proof code and any required checking data. The resulting predicate symbol is Sigma-1, and its standard truth means exactly that an actual finite PA formal proof exists. Effective operations on formal proof codes combine an implication formal proof with an antecedent formal proof, and turn a formal proof into a formal proof that its code is a formal proof; PA verifies those constructions. They give distribution and positive introspection, while an actual theorem's finite formal proof gives its internal provability assertion. This is the requested rough construction, with the three internal formal proof properties distinguished from external agreement.

First establish the transfer of provability requested in the hint. The propositional theorem $X\to (\neg G\to X)$ and the derivability conditions giveThe supplied arithmetized deduction equivalence identifies the right-hand provability assertion, within $S^{\ast }$, with ${\square }^{\ast }X$. HenceChoose a fixed contradiction $\perp$ for $X$. Part (b) gives $S⊢G\leftrightarrow \neg \square \perp$, so adjoining $\neg G$ gives $S^{\ast }⊢\square \perp$. The transfer implication now gives $S^{\ast }⊢{\square }^{\ast }\perp$.

Apply (b) inside $S^{\ast }$ to its own Gödel sentence: it proves $G^{\ast }\leftrightarrow \neg {\square }^{\ast }\perp$. The last provability assertion therefore entailsThus the extension proves the negation of its own Gödel sentence as well. When $S$ is first-order consistent, (c) says this phenomenon occurs in a first-order consistent extension; the extension asserts an internal formal proof of contradiction without there being an actual standard formal proof of contradiction.

Take $\square A={\mathrm{Pr}}_{PA}(┌A┐)$ for the standard formal proof predicate symbol and putUse as given the arithmetization of syntax in PA, the derivability conditions, and the diagonal lemma. The latter supplies the fixed point needed in (a), and the former conditions interpret its normal modal distribution, necessitation on theorems and axiom4. Thus the argument in (a) proves the internal Löb implication in PA. With $X=\perp$ it readsThe inner implication is the first-order consistency first-order sentence $\neg \square \perp$, so contraposition givesThis is the arithmetic statement of the second incompleteness theorem proved within PA: if PA is first-order consistent, there is no PA formal proof of its first-order consistency first-order sentence. The displayed implication is a PA theorem without assuming that PA proves its antecedent.

For the corresponding external consequence, if a first-order consistent PA proved ${\mathrm{Con}}_{PA}$, theoremhood would give a formal proof of its boxed assertion. The displayed theorem together with the supposed formal proof of first-order consistency gives its negation, contradicting first-order consistency. Hence an externally first-order consistent PA does not prove its own first-order consistency.

A prime model of a complete theory $T$ is a first-order model admitting an elementary embedding of first-order structures into every first-order model of $T$. Let $\mathcal{A}\models T$ be canonical and $\mathcal{B}\models T$. For each closed term $t$, defineEvery element of $A$ has a name, so this defines the desired map on all of $A$. If two first-order terms agree in $\mathcal{A}$, their logical equality first-order sentence holds in one first-order model of the complete theory and therefore in every first-order model of it; they agree in $\mathcal{B}$. This proves well-definedness. If they are distinct in $\mathcal{A}$, their inequality holds throughout the complete theory as well, proving injectivity.

For every logical formula $\varphi (\vec{x})$ and named tuple ${\vec{t}}^{\mathcal{A}}$, the substituted first-order sentence $\varphi (\vec{t})$ has the same truth value in the two first-order models by completeness of $T$. ConsequentlyThus $e$ is elementary. Since $\mathcal{B}$ was arbitrary, every such canonical first-order structure is prime. This formal proof also handles closed-term generation when function symbols are present; under the constant-name convention one simply uses constants as the first-order terms.

Use the completeness of the first-order theory of dense linear orders without endpoints and its quantifier elimination. After naming finitely many increasing constants, quantifier elimination still holds in the expanded first-order language: treat these constants as fixed parameters when eliminating quantifiers. Every quantifier-free sentence is a Boolean combination of logical equalities and order comparisons of the named constants, all decided by their stated strict increasing order. Hence ${\mathrm{DLO}}_n$ is complete.

An alternative formal proof of this finite case uses the stated general theorem that a first-order theory in a countable first-order language with only infinite first-order models and a unique countable first-order model is complete: if first-order models disagreed on a first-order sentence, downward Löwenheim-Skolem would give disagreeing countable first-order models. Part (iii) supplies the uniqueness.

Every first-order sentence of $L_{\omega }$ mentions only finitely many constant symbols, hence belongs to some $L_n$. Its truth is decided by ${\mathrm{DLO}}_n$, and every first-order model of ${\mathrm{DLO}}_{\omega }$ has a reduct satisfying that finite first-order theory. Thus the larger first-order theory also decides every first-order sentence. The rational-order examples in (ii) establish first-order consistency. ConsequentlyThere is no contradiction with (ii): completeness is agreement on individual finite first-order sentences, while categoricity requires a global isomorphism respecting all constants simultaneously.

Here $\mathcal{B}\subseteq \mathcal{A}$ means a substructure, so the smaller carrier contains all named constants, is closed under every function symbol, and has each relation restricted from the larger first-order structure. First-order term evaluation on tuples from $B$ agrees in the two first-order structures. Consequently atomic formulas agree, and induction on Boolean connectives makes every quantifier-free formula agree as well.

Write an arbitrary universal sentence of $T$ as $\forall \vec{x}\theta (\vec{x})$ with quantifier-free matrix. Every tuple from $B$ is also a tuple from $A$, so $\theta$ holds at that tuple in $\mathcal{A}$. Quantifier-free agreement transfers it to $\mathcal{B}$. Since the tuple was arbitrary, $\mathcal{B}$ satisfies the universal sentence. ThusAn arbitrary subset without the substructure operations and relation restrictions would not be the hypothesis used by this formal proof.

An arithmetic logical formula is ${\Sigma }_0$, or bounded, if all its quantifiers are bounded by arithmetical first-order terms. A ${\Sigma }_1$ logical formula has an initial block of existential quantifiers followed by a bounded matrix, up to the usual logical transformations. Soundness of an arithmetic theory at a given level means that every first-order sentence of that level proved by the first-order theory is true in the standard natural numbers. Here ${\Sigma }_0$-completeness means that every true bounded arithmetic sentence is provable.

A first-order theory is one-consistent if there is no bounded arithmetic formula $A(x)$ for which it proves $\exists xA(x)$ while proving $\neg A(\bar{n})$ for every standard natural number $n$. This is a restricted form of omega-consistency. In particular one-consistency implies first-order consistency, since an inconsistent first-order theory proves every first-order sentence and its negation.

Suppose a ${\Sigma }_0$-complete first-order theory $S$ is first-order consistent. If it proved a false bounded arithmetic sentence $\theta$, the true bounded arithmetic sentence $\neg \theta$ would also be provable by completeness, contradicting first-order consistency. Thus $S$ is ${\Sigma }_0$-sound. Conversely ${\Sigma }_0$-soundness excludes inconsistency because an inconsistent first-order theory proves the false bounded arithmetic sentence $0=1$. ThereforeIf $S$ is one-consistent but proved a false existential sentence $\exists xA(x)$ with bounded matrix, every standard instance $\neg A(\bar{n})$ would be true and hence provable. This violates one-consistency. Thus it is ${\Sigma }_1$-sound. Conversely, ${\Sigma }_1$-soundness implies first-order consistency by the previous argument, since bounded arithmetic sentences are included at the existential level. If $S$ proved $\exists xA(x)$, soundness of an arithmetic theory would give a standard witness $n$ with $A(n)$ true. Bounded completeness of an arithmetic theory would then give $S⊢A(\bar{n})$, so first-order consistency prevents simultaneous formal proofs of all the negated instances. HenceMultiple existential logical variables can be treated as a finite tuple of witnesses; the same reasoning applies.

The definition of $a$ makes the diagonal instance $E_a[\bar{a}]$ exactly $G_S$. The representing logical formula therefore has the standard interpretationIf $S⊢G_S$, choose an actual witness $m$ to the left-hand existential statement. The bounded arithmetic sentence $A(\bar{a},\bar{m})$ is true and hence provable by ${\Sigma }_0$-completeness. But $G_S$ also gives $S⊢\neg A(\bar{a},\bar{m})$, a contradiction. ThusNow assume one-consistency. It implies first-order consistency, so no formal proof of $G_S$ exists and $A(a,m)$ is false for each standard $m$. Each bounded arithmetic sentence $\neg A(\bar{a},\bar{m})$ is consequently true and provable. A formal proof of $\neg G_S$ would give a formal proof of $\exists v_{2}A(\bar{a},v_2)$ while every standard witness instance is refuted, contrary to one-consistency. HenceThe two hypotheses play different roles: ordinary first-order consistency excludes the positive Gödel sentence, while the stronger hypothesis also excludes its negation.

Write $\rho ={\mathrm{Pr}}_{PA}^{\ast }(┌R┐)$. The supplied fixed-point equivalence gives $PA⊢R\leftrightarrow \neg \rho$.

If PA proved $R$, the first assumed property would give $PA⊢\rho$, while the equivalence would give $PA⊢\neg \rho$. This contradicts first-order consistency. If PA proved $\neg R$, the second assumed property would give $PA⊢\neg \rho$, and the reverse implication of the equivalence would give $PA⊢R$, again a contradiction. HenceThis is the Rosser improvement: its comparison of formal proof codes permits ordinary first-order consistency to exclude both alternatives, without assuming one-consistency.

If PA is inconsistent, every desired conclusion is already a theorem, so it suffices to analyze the first-order consistent case. Use $Q(u,v)$ for the bounded arithmetical proof relation and $\mathrm{neg}(u)$ for the code of the negation of the logical formula coded by $u$.

Suppose $PA⊢E_n$ and let $m$ be the code of an actual formal proof. By first-order consistency there is no formal proof of $\neg E_n$, in particular none with code at most $m$. Thusis a true bounded arithmetic sentence. Bounded completeness of an arithmetic theory proves it in PA, and existential introduction gives $PA⊢{\mathrm{Pr}}_{PA}^{\ast }(\bar{n})$.

Conversely suppose $PA⊢\neg E_n$ and choose an actual formal proof code $k$ of that negation. First-order consistency excludes every formal proof of $E_n$, so each of the finitely many statements $\neg Q(\bar{n},\bar{j})$ for $j<k$ is true and provable. The supplied finite-case theorem permits PA to combine them into the assertion that no formal proof code below $k$ proves $E_n$.

PA also proves $Q(\overline{\mathrm{neg}(n)},\bar{k})$. For any candidate formal proof code $v\ge \bar{k}$, this one code already refutes the universal no-earlier-negation condition in the Rosser predicate symbol. For $v<\bar{k}$, the finite verification refutes its positive formal proof condition. The supplied order dichotomy and finite-case expansion cover all $v$. ThereforeThe argument uses bounded verification of a finite initial segment and one fixed counter-witness beyond it; it does not infer that PA proves the absence of all ordinary formal proofs merely from first-order consistency.

If PA is first-order consistent and already proves $\neg X$, it cannot also prove $X$. By the correctness of the ordinary arithmetized arithmetical proof relation, $\mathbb{N}\models \neg {\mathrm{Pr}}_{PA}(┌X┐)$.

If PA is inconsistent, it proves $X$ by explosion, so an actual formal proof code witnesses ${\mathrm{Pr}}_{PA}(┌X┐)$ in the standard natural numbers. ThusThe hypothesis that $X$ is refutable is essential to this first-order consistency characterization for an arbitrary fixed first-order sentence.