orders on propositions play in maintaining the consistency
of foundations.
Neglecting to include the order of a proposition in in its
Gödel number makes it possible to mistakenly conclude that
the proposition I'mUnprovable exists as a fixed point of a
recursive definition.
See the following for details:
Each proposition is assigned to an increasing prime power, and the increasing list of primes has total order, such that swapping propositions yields a distinct Gödel number.
Gödel number but did not include the order of the proposition.
then they have the same Gödel numbers.
Unfortunately, Gödel number of a proposition leaves out the order of the proposition :-(
same characters in the same order.
His claim is that the proposition "This proposition is not provable", formalized as "P equivalent to P is not provable" is not well formed in a typed logic, as "P"'s type is first-order, while "P is not provable"'s type is second-order. Therefore, his claim is that the proposition is simply not well-typed and therefore not interesting. Godel's proofs were discussing an untyped logic, but according to Hewitt that is not an accurate representation of mathematics.
I don't think anyone in the space agrees with him, though, as far as I could tell from some cursory reading.
mathematics with orders on propositions.
The [Gödel 1931] proposition I'mUnprovable is certainly of
historical interest and may perhaps be of philosophical
interest.
However, including the proposition I'mUnprovable in
foundations makes the foundations inconsistent.
(Of course there can theoretically be bugs in a computer verified proof. If there are bugs in the verifier. But if 4 independent proof assistants verify a proof of a theorem, this is extremely unlikely.)
All of the computer-verified proofs of existence of [Gödel
1931] proposition I'mUnprovable left out the order of
proposition in its Gödel number :-(