Refuting Gödel's 1931 Incompleteness Theorem in one sentence

[PeteOlcott]

Every expression of language that would otherwise be classified as undecidable
is instead decided to be untrue.

Does untrue mean the same as false?

No it does not. It conflates together false with semantically incorrect.

[Univalence]

Every expression of language that would otherwise be classified as undecidable
is instead decided to be untrue.

Does untrue mean the same as false?

No it does not. It conflates together false with semantically incorrect.

Pete, apparently your system encodes semantics. You said True means Boolean.True. Does Untrue mean Boolean.False or is it a distinct (3rd) category?

[PeteOlcott]

Does untrue mean the same as false?

No it does not. It conflates together false with semantically incorrect.

Pete, apparently your system encodes semantics. You said True means Boolean.True. Does Untrue mean Boolean.False or is it a distinct (3rd) category?

It is just like conventional formal systems and formal proofs except
Axioms are stipulated to be true, thus forcing all theorems to be true,
and everything else that is neither a theorem nor an axiom to be untrue.

When true is defined as deductively sound conclusions:
(1) True is ALWAYS defined. (thus refuting Tarski)
(2) Everything ELSE is defined as untrue. (Thus eliminating undecidability).

[Univalence]

No it does not. It conflates together false with semantically incorrect.

Pete, apparently your system encodes semantics. You said True means Boolean.True. Does Untrue mean Boolean.False or is it a distinct (3rd) category?

It is just like convectional formal systems and formal proofs except
Axioms are stipulated to be true, thus forcing all theorems to be true,
and everything else that is neither a theorem nor an axiom to be untrue.

When true is defined as deductively sound conclusions:
(1) True is ALWAYS defined. (thus refuting Tarski)
(2) Everything ELSE is defined as untrue. (Thus eliminating undecidability).

You aren’t hearing me.

Is “untrue” represented by Boolean.False in your system?

When YOU use the phrases “untrue” and Boolean.False do YOU mean the same thing?

[PeteOlcott]

Pete, apparently your system encodes semantics. You said True means Boolean.True. Does Untrue mean Boolean.False or is it a distinct (3rd) category?

It is just like convectional formal systems and formal proofs except
Axioms are stipulated to be true, thus forcing all theorems to be true,
and everything else that is neither a theorem nor an axiom to be untrue.

When true is defined as deductively sound conclusions:
(1) True is ALWAYS defined. (thus refuting Tarski)
(2) Everything ELSE is defined as untrue. (Thus eliminating undecidability).

You aren’t hearing me.

Is “untrue” represented by Boolean.False in your system?

When YOU use the phrases “untrue” and Boolean.False do YOU mean the same thing?

Think of it as a software system:

class Expression
{
std::string Expression
int Truth_Value; // initalized to -1 meaning Empty
};

Provable from axioms changes Truth_Value to 1, else its left empty.
Refutable from axioms changes Truth_Value to 0, else its left empty.

[Univalence]

It is just like convectional formal systems and formal proofs except
Axioms are stipulated to be true, thus forcing all theorems to be true,
and everything else that is neither a theorem nor an axiom to be untrue.

When true is defined as deductively sound conclusions:
(1) True is ALWAYS defined. (thus refuting Tarski)
(2) Everything ELSE is defined as untrue. (Thus eliminating undecidability).

You aren’t hearing me.

Is “untrue” represented by Boolean.False in your system?

When YOU use the phrases “untrue” and Boolean.False do YOU mean the same thing?

Think of it as a software system:

class Expression
{
std::string Expression
int Truth_Value; // initalized to -1 meaning Empty
};

Provable from axioms changes Truth_Value to 1, else its left empty.
Refutable from axioms changes Truth_Value to 0, else its left empty.

Pete. You fucked up. This is a Type error.

By initialising Truth_Value to "-1" you have a trinary NOT binary truth-value. But all of your axioms are Booleans!
This is a partial function.

English(True) ⇔ int(1) ⇔ Boolean.True
English(False) ⇔ int(0) ⇔ Boolean.False
English(untrue) ⇔ int(-1) ⇔ ?????????

Can you say UNDECIDABLE.

[PeteOlcott]

You aren’t hearing me.

Is “untrue” represented by Boolean.False in your system?

When YOU use the phrases “untrue” and Boolean.False do YOU mean the same thing?

Think of it as a software system:

class Expression
{
std::string Expression
int Truth_Value; // initalized to -1 meaning Empty
};

Provable from axioms changes Truth_Value to 1, else its left empty.
Refutable from axioms changes Truth_Value to 0, else its left empty.

Pete. You fucked up. This is a Type error.

By initialising Truth_Value to "-1" you have a trinary NOT binary truth-value. But all of your axioms are Booleans!
This is a partial function.

English(True) ⇔ int(1) ⇔ Boolean.True
English(False) ⇔ int(0) ⇔ Boolean.False
English(untrue) ⇔ int(-1) ⇔ ?????????

Can you say UNDECIDABLE.

The problem is that the English words are applied incorrectly.
When we say that a problem is undecidable we don't mean that a solution exists and it
cannot be decided which one to select. What we really mean is that neither of the two
Boolean values is the correct answer.

When we run into these problems that have no correct answer we call the system
incomplete because it cannot select the correct answer when no correct answer exists.

Here is a multiple choice question: 2 + 3 = ?
(1) 7
(b) 3
(c) 17
(d) 4

The way that we apply this in math is we conclude that your mind must
be incomplete because it cannot choose the correct answer from {a,b,c,d}
the above problem is undecidable.

[Univalence]

Think of it as a software system:

class Expression
{
std::string Expression
int Truth_Value; // initalized to -1 meaning Empty
};

Provable from axioms changes Truth_Value to 1, else its left empty.
Refutable from axioms changes Truth_Value to 0, else its left empty.

Pete. You fucked up. This is a Type error.

By initialising Truth_Value to "-1" you have a trinary NOT binary truth-value. But all of your axioms are Booleans!
This is a partial function.

English(True) ⇔ int(1) ⇔ Boolean.True
English(False) ⇔ int(0) ⇔ Boolean.False
English(untrue) ⇔ int(-1) ⇔ ?????????

Can you say UNDECIDABLE.

The problem is that the English words are applied incorrectly.
When we say that a problem is undecidable we don't mean that a solution exists and it
cannot be decided which one to select. What we really mean is that neither of the two
Boolean values is the correct answer.

When we run into these problems that have no correct answer we call the system
incomplete because it cannot select the correct answer when no correct answer exists.

Here is a multiple choice question: 2 + 3 = ?
(1) 7
(b) 3
(c) 17
(d) 4

The way that we apply this in math is we conclude that your mind must
be incomplete because it cannot choose the correct answer from {a,b,c,d}
the above problem is undecidable.

Pete, massaging the definition of “undecidable” until it fits your “proof” is not a solution to the halting problem.

The example above is decidable. The answer is the implicit “e) none of the above”.

Code: Select all

expression = 2 + 3
options = [7, 3, 17, 4]
try:
  result = options.index(expression)
  print(result)
except ValueError:
  print(“None of the above. Actual answer:”, expression)

Undecidable means “I am still computing the answer. Stand by.”

Anyway. I tried. I have given you a day of my life to show you your mistake.

It is as far as I am willing to go.

[PeteOlcott]

Pete. You fucked up. This is a Type error.

By initialising Truth_Value to "-1" you have a trinary NOT binary truth-value. But all of your axioms are Booleans!
This is a partial function.

English(True) ⇔ int(1) ⇔ Boolean.True
English(False) ⇔ int(0) ⇔ Boolean.False
English(untrue) ⇔ int(-1) ⇔ ?????????

Can you say UNDECIDABLE.

The problem is that the English words are applied incorrectly.
When we say that a problem is undecidable we don't mean that a solution exists and it
cannot be decided which one to select. What we really mean is that neither of the two
Boolean values is the correct answer.

When we run into these problems that have no correct answer we call the system
incomplete because it cannot select the correct answer when no correct answer exists.

Here is a multiple choice question: 2 + 3 = ?
(1) 7
(b) 3
(c) 17
(d) 4

The way that we apply this in math is we conclude that your mind must
be incomplete because it cannot choose the correct answer from {a,b,c,d}
the above problem is undecidable.

Pete, massaging the definition of “undecidable” until it fits your “proof” is not a solution to the halting problem.

The example above is decidable. The answer is the implicit “e) none of the above”.

In order to make a clear example I had to make it less than perfectly accurate.
The perfectly accurate example is the Liar Paradox, yet it is far from clear.
Is this sentence true or false: "This sentence is not true".
(The correct answer is neither).

The difference between literally undecidable logic sentences and literally incorrect
logic sentences is that the former is merely lacking decision criteria such as WFF
with free variables, whereas the latter has the decision criteria yet both True and False
are the wrong answer.

You are so much in the habit of thinking about these things in the conventional way
that you cannot see that I am obviously correct.

[Univalence]

The difference between literally undecidable logic sentences and literally incorrect
logic sentences.

You are literally incapable of understanding why you can't tell the difference between the two until you evaluate them.

You are tripping over grammar, when recursion/self-reference/partial evaluation is the essence of computation.
If you "solve" the liars' paradox - you lose computation.

The Liars' paradox is equivalent to the Halting problem. You are trying to trivialise it down to a grammatical error.

You are so much in the habit of thinking about these things in the conventional way
that you cannot see that I am obviously correct.

Yeah! I am in the habit of valuing the utility of language over its grammatical correctness. You silly Grammar Nazi.

Your "unconventional way" sure sounds a lot like Logocentrism.

As a pragmatist I don’t give a damn about silly philosophical notions such as Truth - all I care about is utility.

And if “lying” works - then great!

[PeteOlcott]

The difference between literally undecidable logic sentences and literally incorrect
logic sentences.

You are literally incapable of understanding why you can't tell the difference between the two until you evaluate them.

You are tripping over grammar, when recursion/self-reference/partial evaluation is the essence of computation.
If you "solve" the liars' paradox - you lose computation.

The Liars' paradox is equivalent to the Halting problem. You are trying to trivialise it down to a grammatical error.

You are so much in the habit of thinking about these things in the conventional way
that you cannot see that I am obviously correct.

Yeah! I am in the habit of valuing the utility of language over its grammatical correctness. You silly Grammar Nazi.

Your "unconventional way" sure sounds a lot like Logocentrism.

As a pragmatist I don’t give a damn about silly philosophical notions such as Truth - all I care about is utility.

And if “lying” works - then great!

I worked directly with the author of this SEP article: Panu Raatikainen:
https://uta-fi.academia.edu/PanuRaatikainen

https://plato.stanford.edu/entries/goed ... mpleteness
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

To derive this formalization of his above simplified essence of the conclusion
of the 1931 Incompleteness Theorem

This was his version:
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ~G)))
He uses L(F) to indicate the Language of F, I call this Closed_WFF(F)

Then I dropped the Robinson Arithmetic or greater qualification because
I knew that if no G exists in any formal system then no G exists in any
subset of this empty set.

∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
So when we understand that the above expression is the correct formalization
of the essence of the conclusion of the 1931 Incompleteness Theorem

I will pause here do see if you understand that.

[PeteOlcott]

The difference between literally undecidable logic sentences and literally incorrect
logic sentences.

You are literally incapable of understanding why you can't tell the difference between the two until you evaluate them.

You are tripping over grammar, when recursion/self-reference/partial evaluation is the essence of computation.
If you "solve" the liars' paradox - you lose computation.

The Liars' paradox is equivalent to the Halting problem. You are trying to trivialise it down to a grammatical error.

You are so much in the habit of thinking about these things in the conventional way
that you cannot see that I am obviously correct.

Yeah! I am in the habit of valuing the utility of language over its grammatical correctness. You silly Grammar Nazi.

Your "unconventional way" sure sounds a lot like Logocentrism.

As a pragmatist I don’t give a damn about silly philosophical notions such as Truth - all I care about is utility.

And if “lying” works - then great!

I worked directly with the author of this SEP article: Panu Raatikainen:
https://uta-fi.academia.edu/PanuRaatikainen

https://plato.stanford.edu/entries/goed ... mpleteness
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

To derive this formalization of his above simplified essence of the conclusion
of the 1931 Incompleteness Theorem

This was his version:
∀F (F ∈ Formal_Systems ∧ Q ⊆ F) → ∃G ∈ L(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
He uses L(F) to indicate the Language of F, I call this Closed_WFF(F)

Then I dropped the Robinson Arithmetic or greater qualification because
I knew that if no G exists in any formal system then no G exists in any
subset of this empty set.

∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
So when we understand that the above expression is the correct formalization
of the essence of the conclusion of the 1931 Incompleteness Theorem...

I will pause here do see if you understand that.

[Univalence]

I will pause here do see if you understand that.

It seems to be written in some ancient language.
I can't even parse it, let alone understand it.

It's 2019. Have you tried a Proof assistant?

Then I don't have to ask you (over and over again) to give me the implementations of for things like ↔, → and ⊬, Closed_WFF() etc...

[PeteOlcott]

I will pause here do see if you understand that.

It seems to be written in some ancient formal language.
I can't even parse it, let alone understand it.

It's 2019. Have you tried a Proof assistant?

Ah I see. You don't understand me simply because you don't know predicate logic well enough.

This is a cut-and-paste verbatim quote of his first email reply to me:
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))

This version merely uses more conventional symbols
∀F (F ∈ Formal_Systems ∧ Q ⊆ F) → ∃G ∈ L(F) (G ↔ (F ⊬ G))

This version adds unprovability of ¬G as indicated by a later email reply
∀F (F ∈ Formal_Systems ∧ Q ⊆ F) → ∃G ∈ L(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

In English this says:
There exists a formal system F and a closed WFF G of F such that G
is materially equivalent to its own unprovability and irrefutability.

[Univalence]

Ah I see. You don't understand me simply because you don't know predicate logic well enough.

And you don't understand me because you don't understand Univalent mathematics well enough.

https://en.wikipedia.org/wiki/Univalent_foundations

Univalent foundations depart from the use of classical predicate logic as the underlying formal deduction system, replacing it, at the moment, with a version of Martin-Löf type theory.

The Times They are A changin'