On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying to >>>>>>> tell
to topic poster in one of my previous posts. Prolog in it's bare >>>>>>> form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use Coq >>>>>>> theorem prover, I've never used it by myself, but it looks like
one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I >>>>>> think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper
proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it is
a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not provable
or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G
must be true, proving it in F', but not in F, thus F is incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them semantically invalid.
In his undefinability proof: (only two pages long) https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher level is called the "the metatheory". (see link).
since in this interpretation the sentence x, which contains no specific term of the metatheory, is its o\vn correlate, the proof of the sentence x given in the metatheory can automatically be carried over into the theory itself: the sentence x which isundecidable in the original theory becomes a decidable sentence in the enriched theory.
We can then show that we can make a G' in F' with the same property,
and thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert G
into the statement G says that G is unprovable, but we can in F', thus
the statement in F' is that G says that G in unprovable in F, and that
statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying to
tell
to topic poster in one of my previous posts. Prolog in it's bare form >>>>>> is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use Coq >>>>>> theorem prover, I've never used it by myself, but it looks like
one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I >>>>> think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper proof >>> assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable then
that makes Gödel totally wrong. G is not Gödel's theorem, it is a key
element of his theorem.
Incomplete T means that there exists a φ such that φ is not provable
or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in, thus
F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G must
be true, proving it in F', but not in F, thus F is incomplete.
We can then show that we can make a G' in F' with the same property, and
thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert G
into the statement G says that G is unprovable, but we can in F', thus
the statement in F' is that G says that G in unprovable in F, and that statement is provable in F'
You don't seem to be able to handle the concept of layers of logic systems.
On 5/4/22 10:30 PM, olcott wrote:
On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying >>>>>>>> to tell
to topic poster in one of my previous posts. Prolog in it's bare >>>>>>>> form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use >>>>>>>> Coq
theorem prover, I've never used it by myself, but it looks like >>>>>>>> one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I >>>>>>> think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper >>>>> proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it is >>>> a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not provable >>>> or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G
must be true, proving it in F', but not in F, thus F is incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them
semantically invalid.
In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher level
is called the "the metatheory". (see link).
So we can prove G in the Metatheory, so it is True in the Theory too.
since in this interpretation the sentence x, which contains no
specific term of the metatheory, is its o\vn correlate, the proof of
the sentence x given in the metatheory can automatically be carried
over into the theory itself: the sentence x which is undecidable in
the original theory becomes a decidable sentence in the enriched theory.
But if G is true in the Theory, it is BY DEFINITION not provable in the Theory, so the space of the Theory is shown to have a True Statement
which is not provable, thus the system of the Theory in Incomplete.
We can then show that we can make a G' in F' with the same property,
and thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert G
into the statement G says that G is unprovable, but we can in F',
thus the statement in F' is that G says that G in unprovable in F,
and that statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 5/4/2022 9:46 PM, Richard Damon wrote:
On 5/4/22 10:30 PM, olcott wrote:
On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying >>>>>>>>> to tell
to topic poster in one of my previous posts. Prolog in it's
bare form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to >>>>>>>>> use Coq
theorem prover, I've never used it by myself, but it looks like >>>>>>>>> one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq
(though I
think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper >>>>>> proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it
is a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not
provable or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G
must be true, proving it in F', but not in F, thus F is incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them
semantically invalid.
In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher level
is called the "the metatheory". (see link).
So we can prove G in the Metatheory, so it is True in the Theory too.
In the same way that having a cat in your attic is proof that your car
is leaking oil.
since in this interpretation the sentence x, which contains no
specific term of the metatheory, is its o\vn correlate, the proof of
the sentence x given in the metatheory can automatically be carried
over into the theory itself: the sentence x which is undecidable in
the original theory becomes a decidable sentence in the enriched theory.
But if G is true in the Theory, it is BY DEFINITION not provable in
the Theory, so the space of the Theory is shown to have a True
Statement which is not provable, thus the system of the Theory in
Incomplete.
It really has never made any sense how people can't understand that self-contradictory expressions of language are necessary semantically invalid. Back in 1974 mankind has had almost 2000 years to think about
the Liar Paradox and no one had a clue what the issue was.
Any unprovable expression of any formal or natural language is simply
untrue and nothing more.
We can then show that we can make a G' in F' with the same property,
and thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert
G into the statement G says that G is unprovable, but we can in F',
thus the statement in F' is that G says that G in unprovable in F,
and that statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 5/4/2022 9:46 PM, Richard Damon wrote:
But if G is true in the Theory, it is BY DEFINITION not provable in
the Theory, so the space of the Theory is shown to have a True
Statement which is not provable, thus the system of the Theory in
Incomplete.
G is self-contradictory on the theory and non self-contradictory in the meta-theory.
On 5/4/22 10:30 PM, olcott wrote:
On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying >>>>>>>> to tell
to topic poster in one of my previous posts. Prolog in it's bare >>>>>>>> form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to use >>>>>>>> Coq
theorem prover, I've never used it by myself, but it looks like >>>>>>>> one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq (though I >>>>>>> think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper >>>>> proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it is >>>> a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not provable >>>> or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G
must be true, proving it in F', but not in F, thus F is incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them
semantically invalid.
In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher level
is called the "the metatheory". (see link).
So we can prove G in the Metatheory,
so it is True in the Theory too.
since in this interpretation the sentence x, which contains no
specific term of the metatheory, is its o\vn correlate, the proof of
the sentence x given in the metatheory can automatically be carried
over into the theory itself: the sentence x which is undecidable in
the original theory becomes a decidable sentence in the enriched theory.
But if G is true in the Theory, it is BY DEFINITION not provable in the Theory, so the space of the Theory is shown to have a True Statement
which is not provable, thus the system of the Theory in Incomplete.
We can then show that we can make a G' in F' with the same property,
and thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert G
into the statement G says that G is unprovable, but we can in F',
thus the statement in F' is that G says that G in unprovable in F,
and that statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 2022-05-05 11:57, olcott wrote:
On 5/4/2022 9:46 PM, Richard Damon wrote:
But if G is true in the Theory, it is BY DEFINITION not provable in
the Theory, so the space of the Theory is shown to have a True
Statement which is not provable, thus the system of the Theory in
Incomplete.
G is self-contradictory on the theory and non self-contradictory in
the meta-theory.
G is not self-contradictory in either the theory or the meta-theory.
The Liar Paradox and G are not the same sentence. You keep treating them
as if they were based solely on Gödel's claim that there is a close relationship between them. But saying two things are closely related
does not mean they are the same.
G asserts a claim about arithmetic. It asserts nothing about itself.
André
On 5/4/2022 9:46 PM, Richard Damon wrote:
On 5/4/22 10:30 PM, olcott wrote:
On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying >>>>>>>>> to tell
to topic poster in one of my previous posts. Prolog in it's
bare form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to >>>>>>>>> use Coq
theorem prover, I've never used it by myself, but it looks like >>>>>>>>> one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq
(though I
think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a proper >>>>>> proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it
is a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not
provable or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers to
itself, it does it in a way that F can't handle, so in F, G doesn't
refer to itself but just "some statement", but in a 'more advanced'
version of F, say F', we can see that relationship, and show that G
must be true, proving it in F', but not in F, thus F is incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them
semantically invalid.
In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher level
is called the "the metatheory". (see link).
So we can prove G in the Metatheory,
Yes.
so it is True in the Theory too.
Not at all.
In the theory p is self-contradictory thus not a truth bearer.
In the meta-theory p is NOT self-contradictory.
since in this interpretation the sentence x, which contains no
specific term of the metatheory, is its o\vn correlate, the proof of
the sentence x given in the metatheory can automatically be carried
over into the theory itself: the sentence x which is undecidable in
the original theory becomes a decidable sentence in the enriched theory.
But if G is true in the Theory, it is BY DEFINITION not provable in
the Theory, so the space of the Theory is shown to have a True
Statement which is not provable, thus the system of the Theory in
Incomplete.
G is self-contradictory on the theory and non self-contradictory in the meta-theory.
We can then show that we can make a G' in F' with the same property,
and thus show that there exists a system F'' where we can prove G'.
This is why you simplification doesn't work. In F, we can't convert
G into the statement G says that G is unprovable, but we can in F',
thus the statement in F' is that G says that G in unprovable in F,
and that statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the Liar
Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 5/5/22 1:57 PM, olcott wrote:
On 5/4/2022 9:46 PM, Richard Damon wrote:
On 5/4/22 10:30 PM, olcott wrote:
On 5/3/2022 7:05 AM, Richard Damon wrote:
On 5/2/22 11:01 PM, olcott wrote:
On 5/2/2022 9:21 PM, Ben wrote:
olcott <polcott2@gmail.com> writes:
On 5/2/2022 6:43 PM, Ben wrote:
Aleksy Grabowski <hurufu@gmail.com> writes:
Thanks for confirmation, that's what exactly what I was trying >>>>>>>>>> to tell
to topic poster in one of my previous posts. Prolog in it's >>>>>>>>>> bare form
is a bad theorem solver. It wasn't designed a such.
If you want to deal with such problems maybe it is better to >>>>>>>>>> use Coq
theorem prover, I've never used it by myself, but it looks >>>>>>>>>> like one of
the best proving assistants out there.
And indeed there is a fully formalised proof of GIT in Coq
(though I
think it's the slightly tighter Gödel-Rosser version).
It is true that G is not provable.
G is provable. Proofs abound. I was pointing out one in a
proper proof
assistant, Coq.
It is OK that you are not a math guy.
If you were a math guy you would understand that if G is provable
then that makes Gödel totally wrong. G is not Gödel's theorem, it >>>>>> is a key element of his theorem.
Incomplete T means that there exists a φ such that φ is not
provable or refutable in formal system T.
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
No, G IS provable, just not in the system F that G is described in,
thus F is Incomplete by your definition above.
Part of the key of the Godel proof is that while G sort of refers
to itself, it does it in a way that F can't handle, so in F, G
doesn't refer to itself but just "some statement", but in a 'more
advanced' version of F, say F', we can see that relationship, and
show that G must be true, proving it in F', but not in F, thus F is
incomplete.
Tarski's hierarchy of languages.
It only works at a higher level language because the expression of
language at the next level is not self-contradictory.
All epistemological antinomies are self-contradictory making them
semantically invalid.
In his undefinability proof: (only two pages long)
https://liarparadox.org/Tarski_275_276.pdf
He defines these two levels as "the theory" and the next higher
level is called the "the metatheory". (see link).
So we can prove G in the Metatheory,
Yes.
so it is True in the Theory too.
Not at all.
In the theory p is self-contradictory thus not a truth bearer.
In the meta-theory p is NOT self-contradictory.
How do you get that.
In the Theory, you can't even tell that G references itself, but is just
a statement about mathematics.
since in this interpretation the sentence x, which contains no
specific term of the metatheory, is its o\vn correlate, the proof of
the sentence x given in the metatheory can automatically be carried
over into the theory itself: the sentence x which is undecidable in
the original theory becomes a decidable sentence in the enriched
theory.
But if G is true in the Theory, it is BY DEFINITION not provable in
the Theory, so the space of the Theory is shown to have a True
Statement which is not provable, thus the system of the Theory in
Incomplete.
G is self-contradictory on the theory and non self-contradictory in
the meta-theory.
No, because in the theory, G doesn't even reference itself, so it can't
be self-contradictory.
I think you don't even know what G is, but have only read the clift
notes edition that actually explain it in the meta-theory.
We can then show that we can make a G' in F' with the same
property, and thus show that there exists a system F'' where we can
prove G'.
This is why you simplification doesn't work. In F, we can't convert
G into the statement G says that G is unprovable, but we can in F',
thus the statement in F' is that G says that G in unprovable in F,
and that statement is provable in F'
Likewise for the liar Paradox. Apparently Tarski could prove the
Liar Paradox in his meta-theory.
You don't seem to be able to handle the concept of layers of logic
systems.
On 5/5/2022 9:24 PM, Richard Damon wrote:
On 5/5/22 1:57 PM, olcott wrote:
G is self-contradictory on the theory and non self-contradictory in
the meta-theory.
No, because in the theory, G doesn't even reference itself, so it
can't be self-contradictory.
Gödel says:
...We are therefore confronted with a proposition which asserts its own unprovability.
I think you don't even know what G is, but have only read the clift
notes edition that actually explain it in the meta-theory.
On 5/5/22 10:37 PM, olcott wrote:
On 5/5/2022 9:24 PM, Richard Damon wrote:
On 5/5/22 1:57 PM, olcott wrote:
G is self-contradictory on the theory and non self-contradictory in
the meta-theory.
No, because in the theory, G doesn't even reference itself, so it
can't be self-contradictory.
Gödel says:
...We are therefore confronted with a proposition which asserts its
own unprovability.
Which is Godel making a comment about G, and not a statement in G itself.
G does not directly mention itself in the Theory.
I think you don't even know what G is, but have only read the clift
notes edition that actually explain it in the meta-theory.
So this comment of mine is now proven.
And you have prooved to be a Liar and an idiot, as you abolutely don't
know what you are talking about.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 297 |
| Nodes: | 16 (0 / 16) |
| Uptime: | 117:24:30 |
| Calls: | 6,662 |
| Files: | 12,209 |
| Messages: | 5,334,237 |