If proposition I'mUnprovable exists in foundations, then the

foundations are inconsistent, which was proved in the article linked

elsewhere in this discussion.

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?

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

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!

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.