G asserts its own unprovability in F

[Agent Smith]

Everything is in my first post.
I explained it in simpler less technical terms for you.

It looks like I'll have do a second pass over the OP.

Food for thought: What does G actually say? I know this looks as though it's time for me ta resign, but can you expand and elaborate on G.

Three ways of saying G:
G := (F ⊬ G)
G asserts its own unprovability in F.
G asserts that there is no sequence of inference steps in F that derive G.

The proof of G requires a sequence of inferences steps in F that proves there is no such sequence of inference steps in F.

I'm not all that gifted in the brains department, but I'm not convinced that's what G is. Go back to the liar sentence is what I'd like ta suggest.

[PeteOlcott]

It looks like I'll have do a second pass over the OP.

Food for thought: What does G actually say? I know this looks as though it's time for me ta resign, but can you expand and elaborate on G.

Three ways of saying G:
G := (F ⊬ G)
G asserts its own unprovability in F.
G asserts that there is no sequence of inference steps in F that derive G.

The proof of G requires a sequence of inferences steps in F that proves there is no such sequence of inference steps in F.

I'm not all that gifted in the brains department, but I'm not convinced that's what G is. Go back to the liar sentence is what I'd like ta suggest.

LP := ¬True(LP)
"This sentence is not true."

[Skepdick]

Three ways of saying G:
G := (F ⊬ G)
G asserts its own unprovability in F.
G asserts that there is no sequence of inference steps in F that derive G.

The proof of G requires a sequence of inferences steps in F that proves there is no such sequence of inference steps in F.

I'm not all that gifted in the brains department, but I'm not convinced that's what G is. Go back to the liar sentence is what I'd like ta suggest.

LP := ¬True(LP)
"This sentence is not true."

":=" is the assignment operator (a.k.a let) which is subject to the semantics of your programming language.

For example this should surprise you!

a := False
f := not a
a := True
f = ???
f: = not a
f = ???

Compute the result in your head before reading further.

Code: Select all

λ> let a = False
a :: Bool
λ> let f = not a
f :: Bool
λ> let a = True
a :: Bool
λ> f
True
it :: Bool
λ> let f = not a
f :: Bool
λ> f
False
it :: Bool

[Agent Smith]

Three ways of saying G:
G := (F ⊬ G)
G asserts its own unprovability in F.
G asserts that there is no sequence of inference steps in F that derive G.

The proof of G requires a sequence of inferences steps in F that proves there is no such sequence of inference steps in F.

I'm not all that gifted in the brains department, but I'm not convinced that's what G is. Go back to the liar sentence is what I'd like ta suggest.

LP := ¬True(LP)
"This sentence is not true."

Now compare the liar sentence to the Gödel sentence. We used to do it in school.

[PeteOlcott]

I'm not all that gifted in the brains department, but I'm not convinced that's what G is. Go back to the liar sentence is what I'd like ta suggest.

LP := ¬True(LP)
"This sentence is not true."

Now compare the liar sentence to the Gödel sentence. We used to do it in school.

"This sentence is not true"
If we assume that it is true that makes it not true. // contradiction
If we assume that it is not true that makes it true. // contradiction

G = This sentence cannot be proven in F
G asserts its own unprovability in F.

Proving G in F requires: a sequence of inferences steps in F that proves there is no such sequence of inference steps in F. // a contradiction

We can see THAT G cannot be proved in F and WHY G cannot be proved in F.

The truth is that G cannot be proved in F because there is something wrong with G. When Gödel said the reason is that there is something wrong with F Gödel was wrong.

[Skepdick]

"This sentence is not true"
If we assume that it is true that makes it not true. // contradiction
If we assume that it is not true that makes it true. // contradiction

Well, what are the semantics of the not(x) operator?

What if Booleans are open under negation?
not(True) could be 7.
not(False) could be -351

Code: Select all

λ> not True
7
it :: Int
(0.01 secs, 91,248 bytes)
λ> not False
-351
it :: Int
(0.01 secs, 91,232 bytes)
λ> :t not
not :: Bool -> Int

What if not is surjective?

Code: Select all

λ> not True
0
it :: Int
(0.01 secs, 81,248 bytes)
λ> not False
0
it :: Int
(0.01 secs, 78,232 bytes)
λ> not True == not False
True
it :: Bool
(0.01 secs, 81,408 bytes)

[PeteOlcott]

It turns out that the only reason that Gödel’s G is not provable in F is that G is contradictory in F.

When Gödel’s G asserts that it is unprovable in F it is asserting that there is no sequence of inference steps in F that derives G.

A proof of G in F requires a sequence of inference steps in F that proves there is no such sequence of inference steps in F, a contradiction.

This is like René Descartes saying: “I think therefore thoughts do not exist”

The reason why G cannot be proved in F is that the proof of G in F is contradictory in F, thus Gödel was wrong when he said the reason is that F is incomplete. No formal system is ever supposed to be able to prove a contradiction.

Now we can see both THAT G cannot be proved in F and perhaps for the first time see WHY G cannot be proved in F. The “incompleteness” conclusion has been refuted.

To be honest we would have to rename Gödel’s “incompleteness” theorem to Olcott’s “can’t prove a contradiction” theorem.

[Skepdick]

It turns out that the only reason that Gödel’s G is not provable in F is that G is contradictory in F.

When Gödel’s G asserts that it is unprovable in F it is asserting that there is no sequence of inference steps in F that derives G.

A proof of G in F requires a sequence of inference steps in F that proves there is no such sequence of inference steps in F, a contradiction.

This is like René Descartes saying: “I think therefore thoughts do not exist”

The reason why G cannot be proved in F is that the proof of G in F is contradictory in F, thus Gödel was wrong when he said the reason is that F is incomplete. No formal system is ever supposed to be able to prove a contradiction.

Now we can see both THAT G cannot be proved in F and perhaps for the first time see WHY G cannot be proved in F. The “incompleteness” conclusion has been refuted.

To be honest we would have to rename Gödel’s “incompleteness” theorem to Olcott’s “can’t prove a contradiction” theorem.

This record seems stuck.

Of course you can prove a contradiction. Any inconsistent system can do that, such as the untyped lambda calculus.

In fact it is a necessary condtion for a system to prove a contradiction in order to prove that system's inconsistency property.
Obviously. Because any system which CAN'T prove a contradiction is NOT inconsistent!

[PeteOlcott]

I propose that it is impossible to correctly provide any sequence of inference steps in F that proves in F that there is no such sequence of inference steps in F.

I also propose that formal systems are not required to prove contradictions, thus the inability of a formal system to prove a contradiction is not any short-coming of this formal system.

[Skepdick]

I propose that it is impossible to correctly provide any sequence of inference steps in F that proves in F that there is no such sequence of inference steps in F.

No shit! An object can’t prove its own non-existence.

I also propose that formal systems are not required to prove contradictions, thus the inability of a formal system to prove a contradiction is not any short-coming of this formal system.

[Redacted]

A formal system is not require to prove contradictions.
An inconsistent formal system is required to prove contradictions.

Any formal system which can’t prove contradictions is NOT inconsistent.


[Edited by iMod]

[PeteOlcott]

I propose that it is impossible to correctly provide any sequence of inference steps in F that proves in F that there is no such sequence of inference steps in F.

No shit! An object can’t prove its own non-existence.

Thus it is dead obvious that the reason that G cannot be proved in F is that G is waaaay screwed up not that there is anything at all wrong with F so the conclusion of Gödel "incompleteness" theorem is dead wrong thus nullifying his whole proof.

[Agent Smith]

LP := ¬True(LP)
"This sentence is not true."

Now compare the liar sentence to the Gödel sentence. We used to do it in school.

"This sentence is not true"
If we assume that it is true that makes it not true. // contradiction
If we assume that it is not true that makes it true. // contradiction

G = This sentence cannot be proven in F
G asserts its own unprovability in F.

Proving G in F requires: a sequence of inferences steps in F that proves there is no such sequence of inference steps in F. // a contradiction

We can see THAT G cannot be proved in F and WHY G cannot be proved in F.

The truth is that G cannot be proved in F because there is something wrong with G. When Gödel said the reason is that there is something wrong with F Gödel was wrong.

Gracias. My suggestion for what it's worth would be to continue unpacking G. A proposition, including the Gödel sentence, is inferentially rich.

[PeteOlcott]

Now compare the liar sentence to the Gödel sentence. We used to do it in school.

"This sentence is not true"
If we assume that it is true that makes it not true. // contradiction
If we assume that it is not true that makes it true. // contradiction

G = This sentence cannot be proven in F
G asserts its own unprovability in F.

Proving G in F requires: a sequence of inferences steps in F that proves there is no such sequence of inference steps in F. // a contradiction

We can see THAT G cannot be proved in F and WHY G cannot be proved in F.

The truth is that G cannot be proved in F because there is something wrong with G. When Gödel said the reason is that there is something wrong with F Gödel was wrong.

Gracias. My suggestion for what it's worth would be to continue unpacking G. A proposition, including the Gödel sentence, is inferentially rich.

Anyone already knowing the subject already knows that Gödel's G essentially
asserts that it is unprovable in F. Gödel's himself sums up this sentence as

"We are therefore confronted with a proposition which asserts its own unprovability." 15 (Gödel 1931:39-41)

The only last detail of this that most people are unaware of is that the only
reason why G is unprovable in F is that the proof of G is contradictory in F,
not that there is anything wrong with F as Gödel's proof concludes.

When we "unpack" G in the usual way all that we get is forty pages connected
math formulas prove that a certain positive integer is not derived by these
forty pages of formulas.

Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems

[Agent Smith]

"This sentence is not true"
If we assume that it is true that makes it not true. // contradiction
If we assume that it is not true that makes it true. // contradiction

G = This sentence cannot be proven in F
G asserts its own unprovability in F.

Proving G in F requires: a sequence of inferences steps in F that proves there is no such sequence of inference steps in F. // a contradiction

We can see THAT G cannot be proved in F and WHY G cannot be proved in F.

The truth is that G cannot be proved in F because there is something wrong with G. When Gödel said the reason is that there is something wrong with F Gödel was wrong.

Gracias. My suggestion for what it's worth would be to continue unpacking G. A proposition, including the Gödel sentence, is inferentially rich.

Anyone already knowing the subject already knows that Gödel's G essentially
asserts that it is unprovable in F. Gödel's himself sums up this sentence as

"We are therefore confronted with a proposition which asserts its own unprovability." 15 (Gödel 1931:39-41)

The only last detail of this that most people are unaware of is that the only
reason why G is unprovable in F is that the proof of G is contradictory in F,
not that there is anything wrong with F as Gödel's proof concludes.

When we "unpack" G in the usual way all that we get is forty pages connected
math formulas prove that a certain positive integer is not derived by these
forty pages of formulas.

Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems

I see yer point. Nice! I wonder if Gödel's theorems can be, you know, generalized to all of epistemology? No matter how good a "model" is, there'll always be at least one proposition that is undecidable in that model.

A is unprovable in M

A is a proposition, M is the model (corresponding to F)

[PeteOlcott]

Gracias. My suggestion for what it's worth would be to continue unpacking G. A proposition, including the Gödel sentence, is inferentially rich.

Anyone already knowing the subject already knows that Gödel's G essentially
asserts that it is unprovable in F. Gödel's himself sums up this sentence as

"We are therefore confronted with a proposition which asserts its own unprovability." 15 (Gödel 1931:39-41)

The only last detail of this that most people are unaware of is that the only
reason why G is unprovable in F is that the proof of G is contradictory in F,
not that there is anything wrong with F as Gödel's proof concludes.

When we "unpack" G in the usual way all that we get is forty pages connected
math formulas prove that a certain positive integer is not derived by these
forty pages of formulas.

Gödel, Kurt 1931.
On Formally Undecidable Propositions of Principia Mathematica And Related Systems

I see yer point. Nice! I wonder if Gödel's theorems can be, you know, generalized to all of epistemology? No matter how good a "model" is, there'll always be at least one proposition that is undecidable in that model.

A is unprovable in M

A is a proposition, M is the model (corresponding to F)

When we define a formal system having expressions of language that are derived as the semantic consequence of other expressions of language that have been stipulated to be true, incompleteness and undecidability cannot exist within this system.