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

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?

• I may be wildly off the mark here, but isn't the universal quantification of a $\Pi_1$ sentence still a $\Pi_1$ sentence? Aug 30, 2020 at 14:34
• @Nagase I'm not sure what you mean. It could be missing something entirely trivial for sure! My problem is this: I can leverage the lemma to get things like $\text{Prov}(\ulcorner 777 < K(31415)\urcorner) \to 777 < K(31415)$, or whatever, but how do I get the universal? I cannot plug $K(x) \leq y$ as $\varphi$ into the lemma, since it's not a sentence. Does that make any sense?
– Jori
Aug 30, 2020 at 14:44
• Actually, I now think the issue is simpler: $y < K(x)$ is, according to Kikuchi, the negation of a $\Sigma_1$ formula, so we have $\mathsf{PA} \vdash \mathsf{CON(PA)} \rightarrow (\mathsf{Prov}(\ulcorner y < K(x) \urcorner) \rightarrow y < K(x))$ by the lemma. But then, it's a rule of logic that, if $x, y$ are not free in the antecedent, we may apply universal generalization to the consequent. So we're done. Aug 30, 2020 at 15:07
• @Nagase Sure, but $y < K(x)$ is not a sentence, so the lemma wouldn't apply, right?
– Jori
Aug 30, 2020 at 15:13
• @Nagase Hey, maybe you're interested in this question: math.stackexchange.com/q/3822291/79127 . I've put up a nice bounty :)
– Jori
Sep 14, 2020 at 11:50

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 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 and de-nesting function-symbols. (For example, $$x·y $$≡ ∃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.

• Thanks your help so far, but unfortunately I don't understand your explanation yet. The "specialized lemma", to be absolutely precise, is $\text{PA} \vdash \varphi \to \square_\text{PA} \varphi$ for $\Sigma_1$-sentences $\varphi$. How does that give you $\text{PA} + \varphi \vdash \square_\text{PA} \forall x \varphi(x)$?
– Jori
Aug 30, 2020 at 19:47
• @Jori: Thanks for pointing out my error. I have changed my mind about it being provable from the specialized version, but I cannot be sure about my belief. I also included a reference in case you want one. Aug 31, 2020 at 7:49
• Why does $\mathbf{PA} \vdash t = u \to \bar{t} = \bar{u}$ mean? Are $t, u$ variables or constants? If the latter, I don't think an inductive proof like this can work, because you will have to deal with situations where $t, u$ are variables (it's a correct atomic formula). In either case I don't understand what you mean with $\bar{t}, \bar{u}$.
– Jori
Sep 3, 2020 at 18:13
• @Jori: "$\underline{t}$" means the result of substituting the free variables in $t$ with numerals encoding their values, which is definable over PA in the same way that "$⬜φ$" is. For example, if $k,m$ are variables then within PA the definable string $\underline{k+m}$ is "$\underline{k}+\underline{m}$". For example, PA proves that ( PA proves "$\underline{k}+\underline{m} = \underline{k+m}$" ) by induction and so PA proves ( if $k+m=n$ then PA proves "$\underline{k+m}=\underline{n}$" ) as claimed. This generalizes to arbitrary terms by induction on the term construction. Sep 3, 2020 at 19:01
• I'm not completely positive yet whether I understand you. Let's take $t = x + y$ and $u = y + x$, then concretely what PA-formulas represent $x+y = y+x \to \overline{x+y} = \overline{y+x}$, and what about $x+y = y+x \to \square(x+y = y+x)$? What are those theorems that you say PA proves?
– Jori
Sep 3, 2020 at 20:21

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

• It seems your "e.g. here" is missing a link. But can I just check with you, your version is equivalent to mine (for formulae), right? Mine implies yours because $Σ_1True$ is itself $Σ_1$. Yours implies mine because for any $Σ_1$-formula $φ$, PA proves that if $φ$ then $Σ_1True(\ulcorner φ\urcorner)$. Correct? Aug 31, 2020 at 8:24
• Anyway, do you know of a theory $T$ extending $PA^-$ such that $T$ proves itself $Σ_1$-complete for sentences but not arbitrary formulae? If there is, it would explain why I feel that we cannot easily get the formula version from the sentence version. But if not, then is there a simple trick to bootstrap, or is there a reason it is not easy to do so? Aug 31, 2020 at 8:24
• Hmm did you get my comments? Sep 1, 2020 at 12:09
• Noah, I think you missed a link at "See e.g. here." Also, "Within 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" seems to be phrased confusingly.
– Jori
Sep 3, 2020 at 0:03
• More importantly, is there a relatively easy way to get from the theorem on sentences Kikuchi gives to the much more general theorem you list? Or is the proof of the latter altogether different?
– Jori
Sep 3, 2020 at 0:04