Discussion:
Refuting Incompleteness and Undefinability Version(9) (simple English with citations)
Add Reply
peteolcott
2018-11-02 16:01:03 UTC
Reply
Permalink
∀LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)

Formalization followed by Simple English intuition
(1) ∀x ~True(x) ↔ ~Theorem(x) // x cannot be proven True from known facts.
(2) ∀x True(x) ↔ Theorem(x) // x can be proven True from known facts.
(3) ∀x False(x) ↔ Theorem(~x) // x can be proven False from known facts.

∀x (Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x))

Axiom An axiom is a proposition regarded as self-evidently true without proof. (Weisstein 2018).
An Axiom from math is comparable to an established fact in English. To anchor the notion of Math(Axiom) and English(Fact) we can think of both of these as expressions of language that have been defined to have the semantic property of Boolean True.

Rules-of-Inference show how to correctly transform some expressions of language into other expressions of language.

Theorems are expressions of language proven entirely on the basis of Axioms, and Rules-of-Inference. (Mendelson 2015: 28). When the above definition of Axiom is used as the basis Theorems can be construed as the conclusions of sound deductive inference.

Copyright 2018 by Pete Olcott

Mendelson, Elliott 2015 Introduction to Mathematical logic Sixth edition
1.4 An Axiom System for the Propositional Calculus page 28

Weisstein, Eric W. 2018 “Axiom.” From MathWorld–A Wolfram Web Resource. http://mathworld.wolfram.com/Axiom.html

The Notion of Truth in Natural and Formal Languages
https://www.researchgate.net/publication/323866366_The_Notion_of_Truth_in_Natural_and_Formal_Languages

http://LiarParadox.org/ constantly updated with latest revisions
peteolcott
2018-11-02 17:56:46 UTC
Reply
Permalink
Post by peteolcott
∀LP (LP ↔ ~⊢LP)
Oh dear. Every time you make a change, it just gets worse, not better.
1. ∀LP (LP <-> ~⊢LP) (starting assumption)
2. A <-> ~⊢A (∀ instantiation, 1, with A being any axiom)
3. A (axiom)
4. ⊢A (proof 1–3)
5. ~⊢A (<-> elimination, 2, 3)
6. ⊥ (contradiction, 4, 5)
Thus, ∀LP (LP ↔ ~⊢LP) ⊢ ⊥. So all you've done is construct a proposition that allows you to derive a contradiction. Not very useful.
Try again.
EFQ
If we hypothesize (consider the possibility) that these two expressions
of language accurately formalize the intuitive notions of True and False:
∀x True(x) ↔ ⊢x // x can be proven True from known facts.
∀x False(x) ↔ ⊢~x // x can be proven False from known facts.

Then in the following formalization of the Liar Paradox:
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"

LP is shown to be Semantically_Ill_Formed(LP) even though
Syntactically_WFF(LP) Because ~True(LP) ∧ ~False(LP).

https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
In mathematical logic, a sentence ... must be true or false.

∴ ~Logic_Sentence(LP), thus Semantically_Ill-Formed(LP).

Copyright 2018 Pete Olcott
Peter Percival
2018-11-02 18:25:21 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP)
Oh dear. Every time you make a change, it just gets worse, not better.
1. ∀LP (LP <-> ~⊢LP) (starting assumption)
2. A <-> ~⊢A               (∀ instantiation, 1, with A being any axiom)
3. A                               (axiom)
4. ⊢A                            (proof 1–3)
5. ~⊢A                          (<-> elimination, 2, 3)
6. ⊥                               (contradiction, 4, 5)
Thus, ∀LP (LP ↔ ~⊢LP) ⊢ ⊥. So all you've done is construct a
proposition that allows you to derive a contradiction. Not very useful.
Try again.
EFQ
If we hypothesize (consider the possibility) that these two expressions
∀x True(x)   ↔   ⊢x   // x can be proven True from known facts.
∀x False(x)  ↔   ⊢~x  // x can be proven False from known facts.
∀LP (LP ↔ ~⊢LP)  // "This sentence is not true"
LP is shown to be Semantically_Ill_Formed(LP) even though
What do you mean by semantically ill-formed? What lies to the right of
|- had better be well-formed, unless by |- you mean something quite
different from what is usually means. So if ∀LP (LP ↔ ~⊢LP) means
anything at all, LP had better be meaningful too.
Post by peteolcott
Syntactically_WFF(LP) Because ~True(LP) ∧ ~False(LP).
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
In mathematical logic, a sentence ... must be true or false.
∴ ~Logic_Sentence(LP), thus Semantically_Ill-Formed(LP).
Copyright 2018 Pete Olcott
peteolcott
2018-11-02 18:42:42 UTC
Reply
Permalink
Post by peteolcott
If we hypothesize (consider the possibility) that these two expressions
∀x True(x) ↔ ⊢x // x can be proven True from known facts.
∀x False(x) ↔ ⊢~x // x can be proven False from known facts.
This is just your usual relabelling of ⊢ as "True()", which is pointless. ⊢ already has a label. It doesn't need a second label, and relabelling it as "True()" certainly doesn't mean that ⊢ becomes actual truth. Labels don't have magic powers.
Post by peteolcott
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"
I don't know what you're trying to do with this, but as it is formalized now, it says that every single proposition is materially equivalent to a statement of its own unprovability. When interpreted in a model, this means that every true proposition is unprovable (and vice versa) and every false proposition is provable (and vice versa). You essentially just defined all of truth as the negation of provability.
Why on earth would you want to do that?
And what does this have to do with the liar's paradox, which is about one specific proposition, not all propositions? Why do you think universal quantification over all propositions is at all useful here?
EFQ
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic) --
In mathematical logic, a sentence ... must be true or false. --

From the above we know this:
∀x (~Logic_Sentence(x) ↔ (~True(x) ∧ ~False(x))

If we consider the hypothetical possibility of this:
∀x (True(x) ↔ ⊢x)
∀x (False(x) ↔ ⊢~x)

"This sentence is not true" formalized:
∀LP (LP ↔ ~⊢LP) then satisfies this: ~Logic_Sentence(x)

Its not too hard if one actually considers possibilities.
Dean Keith Simonton, PhD contacted me last night in response to my email.
He is a very famous researcher of the nature of creative genius.

A key aspect of blind variation and selective retention (BVSR),
is having a mind wide open to possibilities and thus not closed
by conventional wisdom.

A mind closed by conventional wisdom prematurely trims off branches
of the search tree before possible solutions have been exhaustively
examined.

Copyright 2018 Pete Olcott
peteolcott
2018-11-02 19:45:03 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
If we hypothesize (consider the possibility) that these two expressions
∀x True(x) ↔ ⊢x // x can be proven True from known facts.
∀x False(x) ↔ ⊢~x // x can be proven False from known facts.
This is just your usual relabelling of ⊢ as "True()", which is pointless. ⊢ already has a label. It doesn't need a second label, and relabelling it as "True()" certainly doesn't mean that ⊢ becomes actual truth. Labels don't have magic powers.
Post by peteolcott
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"
I don't know what you're trying to do with this, but as it is formalized now, it says that every single proposition is materially equivalent to a statement of its own unprovability. When interpreted in a model, this means that every true proposition is unprovable (and vice versa) and every false proposition is provable (and vice versa). You essentially just defined all of truth as the negation of provability.
Why on earth would you want to do that?
And what does this have to do with the liar's paradox, which is about one specific proposition, not all propositions? Why do you think universal quantification over all propositions is at all useful here?
[snip irrelevancies]
Post by peteolcott
∀LP (LP ↔ ~⊢LP)
I don't know why you think the most direct formalization of "this sentence is not true" should end up as "for every proposition, truth is logically equivalent to unprovability".
The above poor paraphrase indicates that your mind has become so closed
that you are now forming your rebuttals before even reading my words.

Here is an accurate paraphrase of my formalization:
For all LP, LP is logically equivalent to ~True(LP)
For all LP, LP is logically equivalent to ~Theorem(LP)
For all LP, LP is logically equivalent to ~⊢LP

You are correct that the universal quantifier is not apt.
"this sentence is not true" would be more aptly formalized as:
∃x (x ↔ ~True(x))
∃x (x ↔ ~Theorem(x))
∃x (x ↔ ~⊢x )

There exists an x such that x is logically equivalent to ~True(x)
There exists an x such that x is logically equivalent to ~Theorem(x)
There exists an x such that x is logically equivalent to ~⊢x

Every expression x of formal language that only asserts its own untruth is ~Logic_Sentence(x).

Every expression x of English that only asserts its own untruth is ~Declarative_Sentence(x).

Every expression x of formal language that only asserts its own unprovability is ~Logic_Sentence(x).

Copyright 2018 Pete Olcott
DKleinecke
2018-11-02 20:00:03 UTC
Reply
Permalink
Post by peteolcott
Every expression x of English that only asserts its own untruth is ~Declarative_Sentence(x).
Please use a consistent nomenclature. In the last post
I looked at Declarative_Sentence was a set. Now it
appears to be a Boolean-valued function.
Peter Percival
2018-11-02 20:40:52 UTC
Reply
Permalink
Post by peteolcott
You are correct that the universal quantifier is not apt.
∃x (x ↔ ~True(x))
∃x (x ↔ ~Theorem(x))
∃x (x ↔ ~⊢x )
The second formula above is true (though poorly expressed): there are
things which are true but are not theorems (i.e., theorems of particular
calculi, to write of theorems generically hardly makes sense). The
reason why it's true (supposing it to be transformed into something
properly expressed) lies in Gödel's first incompleteness theorem, a
theorem that you deny.

None of your formulae express "this sentence is..." for the "this..."
operator you need a logic with definite descriptions. Mendelson, end of
section 2.9.
peteolcott
2018-11-03 04:03:35 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP)
I don't know why you think the most direct formalization of "this sentence is not true" should end up as "for every proposition, truth is logically equivalent to unprovability".
The above poor paraphrase
Because of the high quality of your reviews, I always make sure to provide
a precisely accurate response even if I have to reread them after I have responded.
Upon further review your "error" may have been nothing more than using a simpler
term so that communication would be more effective.

"it says that every single proposition is materially equivalent to a statement of its own unprovability."

The only thing that you got wrong is the distinction between Provability and Theoremhood.

Since my reasoning applies to both Provability and Theoremhood your error is not significant.
It probably just seemed too unconventional and weird to say untheoremhood instead of unprovability.

I have to keep quoting this because "valid" has a distinctly different meaning
within the context of symbolic logic:
Validity and Soundness https://www.iep.utm.edu/val-snd/
A deductive argument is said to be valid if and only if it takes a form that makes it
impossible for the premises to be true and the conclusion nevertheless to be false.
Otherwise, a deductive argument is said to be invalid.

A deductive argument is sound if and only if it is both valid, and all of its premises
are actually true. Otherwise, a deductive argument is unsound.

The following shows the mapping between (syntax/provability) and
(semantics/logical deduction) without any separate set of notational conventions:
An argument is provable (valid) Γ ⊢ X even if its premises are false.
An argument is a theorem (sound) ⊢X only if it has no (false) premises
Post by peteolcott
For all LP, LP is logically equivalent to ~⊢LP
How do you think they're different?
Post by peteolcott
You are correct that the universal quantifier is not apt.
∃x (x ↔ ~True(x))
∃x (x ↔ ~Theorem(x))
∃x (x ↔ ~⊢x )
Nope, this still doesn't do what you want. The second and third version will be true if there is some proposition somewhere that is true but not provable, which is exactly what Gödel says.
Paraphrase of your prior words:
"it says that THERE EXISTS a proposition is materially equivalent to a statement of its own unprovability."

https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom
(G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
simplified to

(G) F ⊢ GF ↔ ~ProvF(GF)
simplified to

G ↔ ~Provable(G)
add existential quantifier

∃G (G ↔ ~Provable(G))
Paraphrase of your prior words:
"it says that THERE EXISTS a proposition is materially equivalent to a statement of its own unprovability."

If G was Provable this contradicts its assertion: G is not Provable.
If ~G was Provable this contradicts its assertion: G is Provable
∴ ~Logic_Sentence(G)

Copyright 2018 Pete Olcott

Once we strip off the tiny bit of remaining extraneous complexity from
the (Raatikainen fall2018) enormous simplifications, we simply have the
above refutable expression of formal language.

(Raatikainen fall2018)
Raatikainen, Panu, "Gödel's Incompleteness Theorems", The Stanford
Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.),
URL = <https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/>.
Nothing in your formalization captures the notion of "this sentence", which is a crucial part of the liar's paradox (the other crucial part if a truth predicate, which isn't just a relabelling of ⊢). You need self-reference, which doesn't exist in standard logic, so you can't just do your usual combination of a random mess of existing logical symbols and hope it leads to self-reference.
EFQ
You need self-reference, which doesn't exist in standard logic,
Post by peteolcott
∀LP (LP ↔ ~⊢LP)
I don't know why you think the most direct formalization of "this sentence is not true" should end up as
"for every proposition, truth is logically equivalent to unprovability".
peteolcott
2018-11-03 05:41:06 UTC
Reply
Permalink
Post by peteolcott
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"
I don't know what you're trying to do with this, but as it is formalized now, it says that every single proposition is materially equivalent to a statement of its own unprovability.
You just said that this: ∀LP (LP ↔ ~⊢LP) means this:
"every single proposition is materially equivalent to a statement of its own unprovability."

Which means that this:
∃G (G ↔ ~Provable(G)) says this:
"there exists a proposition that is materially equivalent to a statement of its own unprovability."

I used ~Provable(G) instead of ~(Γ ⊢ G) because it is less clumsy and
(according to Mendelson) ~⊢G actually says ~Theorem(G) instead of ~Provable(G).

Copyright 2018 Pete Olcott
Peter Percival
2018-11-03 11:01:03 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP)  // "This sentence is not true"
I don't know what you're trying to do with this, but as it is
formalized now, it says that every single proposition is materially
equivalent to a statement of its own unprovability.
"every single proposition is materially equivalent to a statement of its
own unprovability."
"there exists a proposition that is materially equivalent to a statement
of its own unprovability."
I used ~Provable(G) instead of ~(Γ ⊢ G) because it is less clumsy and
Clearly they are different. Γ ⊢ G says that G is provable from Γ.
Provable(G) says [I'm guessing somewhat because it's your notation] G is
provable.

Do you not get that "This sentence" in

"This sentence is not true"

refers to the displayed sentence? Your versions don't refer to themselves.
Post by peteolcott
(according to Mendelson) ~⊢G actually says ~Theorem(G) instead of ~Provable(G).
Copyright 2018 Pete Olcott
Arnaud Fournet
2018-11-03 22:38:49 UTC
Reply
Permalink
Post by Peter Percival
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP)  // "This sentence is not true"
I don't know what you're trying to do with this, but as it is
formalized now, it says that every single proposition is materially
equivalent to a statement of its own unprovability.
"every single proposition is materially equivalent to a statement of its
own unprovability."
"there exists a proposition that is materially equivalent to a statement
of its own unprovability."
I used ~Provable(G) instead of ~(Γ ⊢ G) because it is less clumsy and
Clearly they are different. Γ ⊢ G says that G is provable from Γ.
Provable(G) says [I'm guessing somewhat because it's your notation] G is
provable.
Do you not get that "This sentence" in
"This sentence is not true"
refers to the displayed sentence? Your versions don't refer to themselves.
Post by peteolcott
(according to Mendelson) ~⊢G actually says ~Theorem(G) instead of ~Provable(G).
Copyright 2018 Pete Olcott
Please, avoid propagating this garbage on sci.lang
thanks.
peteolcott
2018-11-04 04:08:26 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"
I don't know what you're trying to do with this, but as it is formalized now, it says that every single proposition is materially equivalent to a statement of its own unprovability.
"every single proposition is materially equivalent to a statement of its own unprovability."
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
Correct. But it doesn't mean that particular proposition is the one it claims exists, because it has no self-reference. It just says that such a proposition exists, somewhere. Therefore, it is not a formalization of the Gödel sentence.
It is quite a different thing for a proposition to say that a Gödel sentence exists rather than saying that it is itself a Gödel sentence.
Do you not know the difference between "some sentence is false" and "this sentence is false"?
EFQ
Post by peteolcott
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
Is refuted below:

∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))

Proved(G) means the satisfaction of: (Γ ⊢ G)
thus the satisfaction of ∃Γ ⊆ F ~(Γ ⊢ G)
If G was Provable in F this contradicts its assertion: G is not Provable in F

Disproved(G) means the satisfaction of: (Γ ⊢ ~G)
thus the satisfaction of ∀Γ ⊆ F (Γ ⊢ G)
If ~G was Provable in F this contradicts its assertion: G is Provable in F
peteolcott
2018-11-04 04:59:22 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
∀LP (LP ↔ ~⊢LP) // "This sentence is not true"
I don't know what you're trying to do with this, but as it is formalized now, it says that every single proposition is materially equivalent to a statement of its own unprovability.
"every single proposition is materially equivalent to a statement of its own unprovability."
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
Correct. But it doesn't mean that particular proposition is the one it claims exists, because it has no self-reference. It just says that such a proposition exists, somewhere. Therefore, it is not a formalization of the Gödel sentence.
It is quite a different thing for a proposition to say that a Gödel sentence exists rather than saying that it is itself a Gödel sentence.
Yes it is. When we wrap the Gödel sentence in an existential quantifier we find that no such sentence exists.
Post by peteolcott
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
If G was Provable this contradicts its assertion: G is not Provable.
If ~G was Provable this contradicts its assertion: G is Provable
Therefore G is neither Provable nor Refutable.

∃F ∈ Formal_Systems
(
∃G (G ↔ ~Provable(G))
If G was Provable this contradicts its assertion: G is not Provable.
∴ ~∃G that satisfies: (G ↔ ~Provable(G)) the Gödel sentence does not exist in any formal system.
)


Copyright 2018 Pete Olcott
peteolcott
2018-11-04 05:50:21 UTC
Reply
Permalink
Post by peteolcott
It is quite a different thing for a proposition to say that a Gödel sentence exists rather than saying that it is itself a Gödel sentence.
Yes it is. When we wrap the Gödel sentence in an existential quantifier we find that no such sentence exists.
I don't know which "we" you're talking about. The Gödel sentence most certainly exists for anyone who understands the proof.
Post by peteolcott
Post by peteolcott
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
If G was Provable
.... in L.
But there is a proof of G in the metalanguage M. Indeed, you just proved it in M yourself. Where do you think your statement "If G was provable..." occurs? It's certainly not in L.
EFQ
I thought you wanted to avoid the more complex version(11)

∀F ∈ Formal_Systems
(
∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
Is not satisfied ∴ ~∃G ∈ F
There is no such Gödel sentence in any formal system.
)

Copyright 2018 Pete Olcott
Arnaud Fournet
2018-11-04 06:13:42 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
It is quite a different thing for a proposition to say that a Gödel sentence exists rather than saying that it is itself a Gödel sentence.
Yes it is. When we wrap the Gödel sentence in an existential quantifier we find that no such sentence exists.
I don't know which "we" you're talking about. The Gödel sentence most certainly exists for anyone who understands the proof.
Post by peteolcott
Post by peteolcott
"there exists a proposition that is materially equivalent to a statement of its own unprovability."
If G was Provable
.... in L.
But there is a proof of G in the metalanguage M. Indeed, you just proved it in M yourself. Where do you think your statement "If G was provable..." occurs? It's certainly not in L.
EFQ
I thought you wanted to avoid the more complex version(11)
∀F ∈ Formal_Systems
(
∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
Is not satisfied ∴ ~∃G ∈ F
There is no such Gödel sentence in any formal system.
)
Copyright 2018 Pete Olcott
Please, avoid propagating this garbage on sci.lang
thanks.
peteolcott
2018-11-05 16:03:23 UTC
Reply
Permalink
See my recent proof Version(13) where I had a world class expert coach me..
Your "world class expert" didn't fix the crucial error you keep making, described above: your faulty interpretation of what kind of provability a Gödel sentence is talking about.
L(F) means the language of formal system F.
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)
It is not talking about some sort of generic, universal provability, just provability in one specific formal language: the language G is in. G does not say that it cannot be proven in any system at all, only that it cannot be proven in ONE SPECIFIC SYSTEM.
When you reinterpret G to mean something else, you are no longer talking about a Gödel sentence, and thus, no longer talking about Gödel incompleteness.
EFQ
When I reformulate their reformulation:
∃F ∈ Formal_Systems ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
We see that no such G exists in any formal system.

Copyright Pete Olcott
peteolcott
2018-11-05 17:05:24 UTC
Reply
Permalink
See my recent proof Version(13) where I had a world class expert coach me..
Your "world class expert" didn't fix the crucial error you keep making, described above: your faulty interpretation of what kind of provability a Gödel sentence is talking about.
L(F) means the language of formal system F.
∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))
Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)
It is not talking about some sort of generic, universal provability, just provability in one specific formal language: the language G is in. G does not say that it cannot be proven in any system at all, only that it cannot be proven in ONE SPECIFIC SYSTEM.
When you reinterpret G to mean something else, you are no longer talking about a Gödel sentence, and thus, no longer talking about Gödel incompleteness.
.... you are no longer talking about Gödel.
How many times do you need to be told? Changing the assumptions and definitions used in a theorem means you are no longer talking about the original theorem.
EFQ
Their reformulation of my original formulation were both was based
on a correct simplification of the original Incompleteness Theorem.

As long as any simplification of the original theorem sufficiently
captures the essence of this original theorem, any refutation of this
simplification applies equally to the original theorem by analogy.

∃F ∈ Formal_Systems (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
Since G is neither Provable nor Refutable in F, G forms a Gödel sentence in F.

∃F ∈ Formal_Systems ⊇ Q (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
Since ~∃G in any F that is a superset of Robinson Arithmetic every Gödel sentence is refuted.

Copyright 2018 Pete Olcott

Loading...