= Solution
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 $\operatorname{neg}(u)$ for the code of the <negation> of the <logical formula> coded by $u$.
Suppose $PA\vdash 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$. Thus
$$
Q(\bar n,\bar m)\wedge(\forall z\le\bar m)\neg Q(\overline{\operatorname{neg}(n)},z)
$$
is a true <bounded arithmetic sentence>. <Bounded completeness of an arithmetic theory> proves it in PA, and existential introduction gives $PA\vdash\operatorname{Pr}_{PA}^*(\bar n)$.
Conversely suppose $PA\vdash\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{\operatorname{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$. Therefore
$$
\boxed{PA\vdash\neg\operatorname{Pr}_{PA}^*(\bar n).}
$$
The 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>.
Back to article page
