Comment by dwohnitmok

Comment by dwohnitmok 3 days ago

21 replies

View on Hacker News

Your comment to JoJoModding in Math Stackexchange is incorrect.

"That's because there are nonstandard models of PA which contain infinite natural numbers. So PA may be able to prove that it produces a proof, but can't prove that the proof is of finite length. And therefore it might not be a valid proof."

If PA proves "PA proves X" then PA can prove X. This is because the key observation is not that there are nonstandard models, but rather that the standard natural numbers model PA.

Therefore if PA proves "PA proves X", then there is in fact a standard, finite natural number that corresponds to the encoded proof of "PA proves X". That finite natural number can be used then to construct a proof of X in PA.

dwohnitmok 3 days ago

I haven't had the time to go through your argument in more detail, but it's important to note (because the natural language version of what you've presented is ambiguous) that you haven't shown "PA proves 'Provable(forall n, G(n))'" in which case it would be the case that in fact "PA proves 'forall n, G(n)'", but rather "PA proves 'forall n, Provable(G(n))'".

My logic is very rusty at this point, but if someone could give me an argument that you cannot move the 'Provable' outside the 'forall', I would really appreciate that, without making reference to Goodstein sequences. In other words, that in general for propositions 'P' it is not true that proving "forall n, Provable(P(n))" implies you can prove "Provable(forall n, P(n))".

Reply View 0 replies
btilly 3 days ago

> If PA proves "PA proves X" then PA can prove X.

Not true.

From PA we can construct a function that can search all possible proofs that can be constructed in PA. In fact I outlined one way to do this at the end of my answer.

With this function, we can construct a function will-return that analyzes whether a given function, with a given input, will return. This is kind of like an attempted solution to the Halting Problem. We know that it doesn't always work. But we also know that it works a lot of the time.

From will-return we can create a function opposite-return that tries to return if a given function with a given input would not, and doesn't return if that function would. This construction is identical to the one in the standard proof of the Halting Problem.

Now we consider (opposite-return opposite-return opposite-return). (Actually you need a step to expand the argument into this recursive form. I've left that out, but that is identical to the one in the standard proof of the Halting problem.)

PA can prove the following:

- PA proves that if PA can prove that opposite-return returns, then it doesn't. - PA proves that if PA can prove that opposite-return doesn't return, then it does. - PA proves that if it can prove everything that it proves that it can prove, then PA must have a proof of one of the two previous statements. - Therefore PA proves that if it can prove everything that it proves that it can prove, then PA is inconsistent.

This is a form of Gödel's second incompleteness theorem.

And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves".

Reply View 13 replies
  • ComplexSystems 2 days ago

    I am not sure I follow and it is possible I may not be on the same wavelength, but here is another thought.

    For any sentence S, if first-order PA (or any first-order theory) proves S, then that means that S holds true in every model of that theory, via the completeness (not incompleteness) theorem.

    The statement "PA proves x" is equivalent to saying "there exists a natural number N which is a Gödel number encoding a proof of x." The letter "x", here, is a natural number that is assumed to encode some sentence we want to prove, that is, x = #S for some sentence S.

    The above is a predicate with one existential quantifier: Provable(x) = there exists N such that IsProof(N, x) holds true, where IsProof says that N is the Gödel number of a valid proof ending in x.

    If PA proves "Provable(x)", that means that the predicate "Provable(x)" holds in every model of PA. This means every model of PA would have some natural number N that satisfies IsProof(N, x). Of course, this number can vary from model to model.

    However: the standard model, which has only standard natural numbers, is also another model of PA. So if PA proves "Provable(x)," and Provable(x) thus holds in every model, it must also hold in the standard model of PA. This means that there must be a regular, standard, finite natural number N_st that encodes a proof of x.

    Since the standard model is an initial segment of every other model of PA, then every other model includes the standard model and all the standard natural numbers. Thus, if PA proves Provable(x), then the standard number N_st must exist in all models.

    So we cannot have a situation where PA proves Provable(x) but all proofs of x must be nonstandard and infinite in length. This would mean no such proof exists in the standard model of PA - but then, via completeness, PA would not be able to prove "Provable(x)".

    Reply View 3 replies
    • btilly 2 days ago

      For every n, the function will return a function, that PA proves has a proof in PA.

      Suppose that we're in a nonstandard model. For all standard n, there really will be a proof. For nonstandard n, there may or may not actually be a proof.

      And so PA cannot prove from the fact that it proved the existence of a proof, that PA actually proves it.

      Reply View 2 replies
      • ComplexSystems 2 days ago

        That is very different though. You are now saying that for all n, PA proves that it has a proof the Goodstein sequence terminates for that n. But that is very different from the earlier claim:

        "And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves"."

        It seems that for each standard n, PA proves that the Goodstein sequence terminates for that n. If also proves that it proves that the Goodstein sequence terminates for all n, and so on. But this is very different from saying "PA proves that it proves the sentence 'for all n, the corresponding Goodstein sequence terminates,'" which is what I thought you were saying.

        Reply View 1 reply
        • btilly 2 days ago

          No, it is not different from the earlier claim. If you think that it is, then you were misreading me.

          My earlier claim is that for each n, "PA proves that it proves that G(n) terminates". But in logic there is an important distinction to be made between "PA proves" and "PA proves that it proves". From the second, you cannot conclude the first. You must actually present the proof, and then verify it.

          And the reason is this. It is true that, for all standard n, "PA proves that it proves" implies that "PA proves". But for nonstandard n it does not. Since PA cannot itself distinguish standard n from nonstandard n, PA cannot follow that implication to a proof.

          (All of this is based on long conversations with my logic professor back in grad school. To the extent that I get it right, https://faculty-directory.dartmouth.edu/marcia-j-groszek deserves the credit. To the extent that I get it wrong, I deserve the blame.)

          Reply View 0 replies
  • tromp 3 days ago

    > > If PA proves "PA proves X" then PA can prove X.

    If we assume PA to be sound, then indeed everything it proves is true.

    > Not true.

    Now you're saying PA is unsound.

    But your article wasn't about PA proves "PA proves X", it was about "forall n : PA proves G(n)".

    For PA not to prove "forall n: G(n)", there is no soundness issue, only a ω-consistency issue.

    Reply View 7 replies
    • btilly 3 days ago

      I think we are saying the same thing.

      If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.

      If PA proves that it proves a statement, and then fails to prove it, PA is unsound.

      There exist collections of statements such that PA proves that it proves each statement, and PA does prove each statement, but PA does not prove the collection of statements.

      Our understanding of the last is helped by understanding that "PA proves that PA proves S" is logically not the same statement as, "PA proves S". Even though they always have the same truth value.

      Reply View 6 replies
      • ComplexSystems 2 days ago

        If PA proves that a number exists with some mathematical property - including being a Gödel number of a proof of something - then some number with that property must exist in every model, including the standard model. So there would have to be a standard number encoding a proof, and the proof that it encodes would have to be correct, assuming your Gödel numbering is.

        Reply View 3 replies
      • dwohnitmok 2 days ago

        > There exist collections of statements such that PA proves that it proves each statement, and PA does prove each statement, but PA does not prove the collection of statements.

        I think this is true (although I would like a significantly more succinct proof than one using Goodstein sequences as I mention here https://news.ycombinator.com/item?id=44277809), but regardless this is substantially weaker than your assertion that there are statements PA can prove that it can prove, but cannot itself prove.

        In particular I can prove that for all propositions P, PA proves P if and only if P proves "Provable(P)" (i.e. "P is provable in PA").

        Given PA proves P, take the finite proof of P in PA and do the usual Godel encoding to get a single number. That is a witness to the implicit existential statement behind "Provable(P)".

        In the other direction, given P proves "Provable(P)", take the natural number witness of the implicit existential statement. Because the standard natural numbers satisfy PA (this is basically equivalent to the assumption that PA is consistent), we know that this natural number is in fact a standard, finite natural number. Hence we can transform this natural number back to a proof of P in PA.

        This equivalence is precisely the reason why the provability relation (more accurately for our purposes stated as "provability in PA") "Provable" is valuable. If the equivalence didn't hold it would be very weird to call this relation "Provable".

        In particular, this means PA proves P if and only if P proves "Provable(Provable(P))" (and so on for as many nestings of Provable as you'd like).

        > If PA proves that it proves a statement, PA cannot conclude from that fact that it proves that statement.

        I kind of think I know what you mean by this, but definitely your conclusion is way too strong. In particular, it is true in a certain intuitive sense that PA cannot "use" the fact of "Provable(P)" to actually prove P. It is in a sense a coincidence that every P for which PA can prove P, PA can also prove "Provable(P)", since that equivalence is carried "outside" of PA. But that's not really anything to do with PA itself, but that's just rather the nature of any encoded representation.

        Even what tromp is saying is quite strange to me (in apparently implying that it's normal for PA to have an omega-consistency issue). It would be very strange to assert PA is omega-inconsistent. It is tantamount to saying PA is inconsistent, since stating that PA is omega-inconsistent is saying that the standard natural numbers are not a valid model of PA.

        Reply View 1 reply
        • tromp 2 days ago

          > Even what tromp is saying is quite strange to me

          Indeed I mis-spoke. While for all n, PA can prove P(n), it cannot prove "for all n: P(n)". I don't know if there is a name for this, but it's not an omega-inconsistency. It would only be omega-inconsistent to have PA contradict "for all n: P(n)", i.e. to prove "there exists an n: not P(n)".

          Reply View 0 replies
  • dwohnitmok 3 days ago

    > PA proves that if it can prove everything that it proves that it can prove, then PA must have a proof of one of the two previous statements.

    I don't believe this is true. I don't know what result you're using here, but I think you're mixing up "provable" and "true".

    In particular your line of reasoning violates Lob's Theorem, which is a corollary of the second incompleteness theorem.

    Reply View 0 replies
bubblyworld 2 days ago

The standard model is a model of PA only if PA is consistent, which it cannot prove unless it is inconsistent (Godel's theorem). So your proposed proof doesn't work in PA itself, which is the point of that comment, I believe.

Reply View 5 replies
  • dwohnitmok 2 days ago

    I believe my proof actually works in systems even weaker than PA (but the metatheory of how exactly to do the encoding in a first-order theory is a bit of a headache for me at the moment).

    In particular I'm not relying on the consistency of PA. If PA is inconsistent, "If PA proves 'PA proves X' then PA can prove X" also holds (trivially), because then PA can prove anything.

    Reply View 4 replies
    • bubblyworld 2 days ago

      Hmm, earlier you wrote:

      > This is because the key observation is not that there are nonstandard models, but rather that the standard natural numbers model PA.

      This fact (that the standard natural numbers model PA) implies that PA is consistent, so your argument is implicitly assuming that from the outset, right? If PA is consistent then this is not something that PA can prove, so I don't see how you could run your proof in PA itself. And certainly not how you could do it in a weaker theory. Logic is subtle though... so what am I missing?

      As far as I know what you're describing (namely that "Provable(X)" implies "X") is called the uniform reflection principle and added to PA is much stronger than PA alone.

      Reply View 3 replies
      • dwohnitmok 13 hours ago

        I'm not familiar with the uniform reflection principle. What does the actual first-order statement look like? Because the simplest version I can think of how to formalize this in PA, namely that PA proves "Provable(X) -> True(X)" (because you need an encoding if you're working in PA, "Provable(X) -> X" is simply not something you can write in the language of PA), is not possible to write in PA (so would be a category error) because of Tarski's undefinability of truth result.

        > so your argument is implicitly assuming that from the outset, right?

        No. My argument implicitly has a fork at the beginning.

        If PA is consistent, run the usual standard natural number argument I made.

        If PA is not consistent, then PA can prove everything.

        Hence the statement "If PA proves 'PA proves X' then PA can prove X." goes through either way. It does not depend on the consistency of PA.

        Reply View 2 replies