How to universalize $\text{Prov}(\ulcorner y < K(x)\urcorner) \to y < K(x)$ in a paper of Kikuchi

Question

In Kikuchi's paper Kolmogorov complexity and the second incompleteness theorem he defines for $\Sigma_1$ binary predicates $R(x, y)$ the condition

$$ \Gamma_{1}(R) \Leftrightarrow \forall x\forall y(R(x, y) \to y < K(x)), $$

where $K(x)$ is the Kolmogorov complexity of $x$. He also mentions a lemma:

For any $\Sigma_1$-sentence in the language of arithmetic:

$PA \vdash \text{Con}(\text{PA}) \to (\text{Prov}(\ulcorner\neg\phi\urcorner) \to \neg\phi)$

Then he states that $\text{PA} \vdash \text{Con}(\text{PA}) \to \Gamma_{1}(\text{Prov}(\ulcorner y < K(x)\urcorner))$ follows immediately from the fact that $y < K(x)$ is the negation of a $\Sigma_{1}$ formula and the previous lemma.

I can see why we obviously get from the lemma each individual instance of $\text{Prov}(\ulcorner y < K(x)\urcorner) \to y < K(x)$ with $x, y$ replaced by natural numbers, but I don't see how to universalize this to the claim $\forall x \forall y (\text{Prov}(\ulcorner y < K(x)\urcorner) \to y < K(x))$, which is what we're after. The above lemma applies to individual sentences only.

What am I missing?

Answer 1

It seems that the text is using the lemma (arithmetized $Σ_1$-completeness of PA) for $Σ_1$-formulae rather than just sentences. Originally, I had thought that the generalized version could be easily proven from the specialized one, but I made a careless mistake. Now I believe that it cannot be proven in such a way. $ \def\pa{\text{PA}} \def\prov{\text{Prov}} \def\prf{\text{Proof}} \def\code#1{\ulcorner#1\urcorner} \def\num#1{\underline{#1}} \def\vv{\vec{v}} $

First I shall give the generalized theorem and an outline of its proof. I shall use the provability modal operator where $⬜φ$ is some sentence that says "$φ$ is provable after its free variables have each been substituted by a numeral encoding its value". For example $⬜( \ ∀x{<}k\ ( \ x·x<k·x \ ) \ )$ expands to $\prov(\code{ ∀x{<}\num{k}\ ( \ x·x<\num{k}·x \ ) })$.

Theorem: Take any $Σ_1$-formula $φ$ with free variables $\vv$. Then $\pa ⊢ ∀\vv\ ( \ φ→⬜φ \ )$.

Proof: (Work with a deductive system for FOL that permits proving formulae with free variables, which are implicitly universally quantified.) Let $ψ$ be a formula equivalent to $φ$ that is in prenex normal form with only bounded universal quantifiers and with matrix in disjunctive normal form. We can assume that every literal in $ψ$ is "$x+y=z$" or "$x·y=z$" for some variables/numerals $x,y,z$, by trichotomy and using $x<y ≡ ∃d\ ( \ x+d+1=y \ )$ and de-nesting function-symbols. (For example, $x·y<z·z$ $≡ ∃a,b,c,d\ ( \ x·y=a ∧ a+1=b ∧ z·z=c ∧ a+d=c \ )$.) Then it suffices to show that $\pa ⊢ ψ→⬜ψ$, because $\pa ⊢ φ→ψ$ and $\pa ⊢ ⬜( \ ψ→φ \ )$. Note that:
  (1) $\pa ⊢ x+y=z → ⬜( \ x+y=z \ )$, for any variables/numerals $x,y,z$. [By induction.]
  (2) $\pa ⊢ x·y=z → ⬜( \ x·y=z \ )$, for any variables/numerals $x,y,z$. [By induction.]
  (3) $\pa ⊢ ⬜α∧⬜β → ⬜( \ α∧β \ )$, for any formulae $α,β$.
  (4) $\pa ⊢ ⬜α∨⬜β → ⬜( \ α∨β \ )$, for any formulae $α,β$.
  (5) $\pa ⊢ ∃x\ ( \ ⬜α \ ) → ⬜( \ ∃x\ ( \ α \ ) \ )$, for any formula $α$ and variable $x$.
      [Because $\pa ⊢ (⬜α)[x{:=}c] → ⬜( \ α[x{:=}c] \ )$.]
  (6) $\pa ⊢ ∀x{<}t\ ( \ ⬜α \ ) → ⬜( \ ∀x{<}t\ ( \ α \ ) \ )$, for any formula $α$ and variable $x$ and term $t$.
      [By induction with respect to $t$, since $\pa ⊢ ∀x{<}t\ ( \ α \ ) ∧ α[x{:=}t] ↔ ∀x{<}t{+}1\ ( \ α \ )$.]
By induction on the logical structure of $ψ$, using (1) and (2) on the literals in the matrix of $ψ$ and then (3) to (6) repeatedly, we obtain the desired claim.

In case you want a reference for the generalized lemma, I managed to find it in Rautenberg's "A Concise Introduction to Mathematical Logic" in Theorem 2.1 under Section 7.2 on "The Provable $Σ_1$-Completeness". Rautenberg did not clearly indicate disparity between the generalized and the specialized versions, but I feel that there is no easy way to bootstrap, because the induction I used in the above proof has parameters arising from those free variables.

Answer 2

I believe you're right, that the argument given isn't correct. However, it's wrong for a right reason (?) - the lemma itself can be substantially strengthened.

I'll phrase it this way:

$\mathsf{PA}$ proves that $\mathsf{PA}$ is $\Sigma_1$-complete. That is, $\mathsf{PA}\vdash$ "For every $x$, if $x$ is a code for a $\Sigma_1$ sentence then $\Sigma_1True(x)\implies Prove_{\mathsf{PA}}(x)$."

We can massage this a bit to get the following:

$\mathsf{PA}$ proves "If $\mathsf{PA}$ is consistent and $x$ is a code for a true $\Sigma_1$ sentence, then $\neg Prov_{\mathsf{PA}}(Neg(x))$."

Here "$Neg$" is the usual formula defining the map $\ulcorner\varphi\urcorner\mapsto\ulcorner\neg\varphi\urcorner$. (For simplicity I'm treating a defined function as a new function symbol; it would be more proper to write "$\forall y(Neg(x,y)\implies \neg Prov_{\mathsf{PA}}(y))$," but that's annoying and doesn't actually add clarity.)

Now there's one final trick: the substitution operation $Sub(x,y,z)$. This is the usual formula defining the map $(\ulcorner\varphi\urcorner, n)\mapsto\ulcorner\varphi(\underline{n})\urcorner$. Within $\mathsf{PA}$ we have that if $x$ is a code for a $\Sigma_1$ formula and $Sub(x,y)$ then $y$ is a code for a $\Sigma_1$ sentence. This gives us:

$\mathsf{PA}$ proves "If $\mathsf{PA}$ is consistent, $x$ is a code for a $\Sigma_1$ formula, and $y$ is such that $\Sigma_1True(Sub(x,y))$, then $\neg Prov_\mathsf{PA}(Neg(Sub(x,y)))$."

And when unwound this gets us (a bit more than) what we want: that $\mathsf{PA}$ proves "If $\mathsf{PA}$ is consistent then for every $x$ which is a $\Sigma_1$ formula code, each substitution instance of $x$ which $\mathsf{PA}$ disproves is in fact false."