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?

  • $\begingroup$ I may be wildly off the mark here, but isn't the universal quantification of a $\Pi_1$ sentence still a $\Pi_1$ sentence? $\endgroup$
    – Nagase
    Aug 30, 2020 at 14:34
  • $\begingroup$ @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? $\endgroup$
    – Jori
    Aug 30, 2020 at 14:44
  • $\begingroup$ 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. $\endgroup$
    – Nagase
    Aug 30, 2020 at 15:07
  • $\begingroup$ @Nagase Sure, but $y < K(x)$ is not a sentence, so the lemma wouldn't apply, right? $\endgroup$
    – Jori
    Aug 30, 2020 at 15:13
  • $\begingroup$ @Nagase Hey, maybe you're interested in this question: math.stackexchange.com/q/3822291/79127 . I've put up a nice bounty :) $\endgroup$
    – Jori
    Sep 14, 2020 at 11:50

2 Answers 2


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.

  • $\begingroup$ 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)$? $\endgroup$
    – Jori
    Aug 30, 2020 at 19:47
  • $\begingroup$ @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. $\endgroup$
    – user21820
    Aug 31, 2020 at 7:49
  • $\begingroup$ 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}$. $\endgroup$
    – Jori
    Sep 3, 2020 at 18:13
  • $\begingroup$ @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. $\endgroup$
    – user21820
    Sep 3, 2020 at 19:01
  • $\begingroup$ 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? $\endgroup$
    – 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."

  • 1
    $\begingroup$ 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? $\endgroup$
    – user21820
    Aug 31, 2020 at 8:24
  • 1
    $\begingroup$ 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? $\endgroup$
    – user21820
    Aug 31, 2020 at 8:24
  • $\begingroup$ Hmm did you get my comments? $\endgroup$
    – user21820
    Sep 1, 2020 at 12:09
  • $\begingroup$ 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. $\endgroup$
    – Jori
    Sep 3, 2020 at 0:03
  • $\begingroup$ 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? $\endgroup$
    – Jori
    Sep 3, 2020 at 0:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.