4 ms·

If proposition I'mUnprovable exists in foundations, then the foundations are inconsistent, which was proved in the article linked elsewhere in this discussion

If proposition I'mUnprovable exists in foundations, then the foundations are inconsistent, which was proved in the article linked elsewhere in this discussion.

rssoconnor 5y ago
Does the proposition I linked to exist? Can you see it? Is it not a well-formed proposition in the language of number theory? How about this proposition: "∀x. ∀y. x + y = y + x". Does it exist? Is it not a well-formed proposition in the language of number theory?
- ProfHewitt 5y ago
  Did you not get the point? If [Gödel 1931] proposition I'mUnprovable exists in foundations, then foundations are inconsistent. See https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
  - rssoconnor 5y ago
    I'm sorry that no I don't get the point. You keep talking about [Gödel 1931] proposition I'mUnprovable, but today is 2021 not 1931, and I'm talking about a specific proposition that I've linked to which is, what appears to me to be a clearly well defined first-order logical proposition involving classical logic, zero, successor, plus and times. I want to know if you object to the existence of that formula that you can see on your screen with your own eyes, and if you do object to it why you do. Because I contend that that formula is of exactly the same character as Goedel's statement, with the difference being that with a computer, and modern encoding functions, we can actually strip away all the definitions and compute the fixed point and literally print it out onto your screen. It is right there in front of your eyes. Look at it! Yet you keep on insisting that fixpoints don't exist despite the fact that I have pointed you directly to a formula that has been specifically computed to satisfy a logical fixed point equation. It's like saying that there cannot be a fixed point of the function f(x) := 3x-10 by waiving your hands and claiming functions don't have fixed point because numbers need to be ordered. But that is daft. All you have to do is compute f(5) = 3*5-10 = 5 to see that 5 is a fixed point of f. Take a look at this. The proposition 0=0 is a fixed point of phi(X) = ¬(¬X). Just do the logical deduction to see 0=0 ⇔ ¬(¬ 0=0) is a true arithmetic statement. See even fixed points for propositions sometimes exist!
    - deleted 5y ago
      [deleted]
    - ProfHewitt 5y ago
      Orders on propositions were introduced by Bertrand Russell to prevent inconsistencies in foundations of mathematics. Strong types prevent construction of I’mUnprovable using the following recursive definition: I’mUnprovable:Proposition<i>≡⊬I’mUnprovable Note that (⊬I’mUnprovable):Proposition<i+1> in the right- hand side of the definition because I’mUnprovable is a propositional variable in the right-hand side. Consequently, I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1> which is a contradiction. The crucial issue with the proofs in [Gödel 1931] is that the Gödel number of a proposition does not capture its order. Because of orders of propositions, the Diagonal Lemma [Gödel 1931] fails to construct the proposition I’mUnprovable.

If proposition I'mUnprovable exists in foundations, then the foundations are inconsistent, which was proved in the article linked elsewhere in this discussion.

rssoconnor 5y ago

Does the proposition I linked to exist? Can you see it? Is it not a well-formed proposition in the language of number theory? How about this proposition: "∀x. ∀y. x + y = y + x". Does it exist? Is it not a well-formed proposition in the language of number theory?

ProfHewitt 5y ago
Did you not get the point? If [Gödel 1931] proposition I'mUnprovable exists in foundations, then foundations are inconsistent. See https://papers.ssrn.com/abstract=3603021 https://papers.ssrn.com/abstract=3603021
- rssoconnor 5y ago
  I'm sorry that no I don't get the point. You keep talking about [Gödel 1931] proposition I'mUnprovable, but today is 2021 not 1931, and I'm talking about a specific proposition that I've linked to which is, what appears to me to be a clearly well defined first-order logical proposition involving classical logic, zero, successor, plus and times. I want to know if you object to the existence of that formula that you can see on your screen with your own eyes, and if you do object to it why you do. Because I contend that that formula is of exactly the same character as Goedel's statement, with the difference being that with a computer, and modern encoding functions, we can actually strip away all the definitions and compute the fixed point and literally print it out onto your screen. It is right there in front of your eyes. Look at it! Yet you keep on insisting that fixpoints don't exist despite the fact that I have pointed you directly to a formula that has been specifically computed to satisfy a logical fixed point equation. It's like saying that there cannot be a fixed point of the function f(x) := 3x-10 by waiving your hands and claiming functions don't have fixed point because numbers need to be ordered. But that is daft. All you have to do is compute f(5) = 3*5-10 = 5 to see that 5 is a fixed point of f. Take a look at this. The proposition 0=0 is a fixed point of phi(X) = ¬(¬X). Just do the logical deduction to see 0=0 ⇔ ¬(¬ 0=0) is a true arithmetic statement. See even fixed points for propositions sometimes exist!
  - deleted 5y ago
    [deleted]
  - ProfHewitt 5y ago
    Orders on propositions were introduced by Bertrand Russell to prevent inconsistencies in foundations of mathematics. Strong types prevent construction of I’mUnprovable using the following recursive definition: I’mUnprovable:Proposition<i>≡⊬I’mUnprovable Note that (⊬I’mUnprovable):Proposition<i+1> in the right- hand side of the definition because I’mUnprovable is a propositional variable in the right-hand side. Consequently, I’mUnprovable:Proposition<i>⇒I’mUnprovable:Proposition<i+1> which is a contradiction. The crucial issue with the proofs in [Gödel 1931] is that the Gödel number of a proposition does not capture its order. Because of orders of propositions, the Diagonal Lemma [Gödel 1931] fails to construct the proposition I’mUnprovable.