Petr Olcott wrote:
....
> This is a file that only reads and outputs text lines, thus provides the
> skeleton for my Simplest TM interpreter. I almost always have some code
> that I can cut-and-paste this from. I couldn't find it so I had to
> create this from scratch.
>
> I count this as my starting point for my Simplest TM interpreter. I want
> to see if I can get the entire project completed in less that four
> hours, including detailed design, coding and debugging and not including
> user documentation. So far I made great progress on the detailed design
> in two minutes.

This is also a good starting point for a POSIX compatible operating
system kernel, you should post it to comp.minix (this previous sentence
is a pun).

Any decent programmer should be able to design and code a TM in C
(I've done it in almost all languages I know about, btw) in less than
four hours. Well. Under the condition that she/he understands what a
TM is. Unfortunately, Peter, you don't.

> It is based on the design of this system yet much simpler:
> http://www.lns.mit.edu/~dsw/turing/turing.html

You didn't spot why your post can be taken for a joke? Really?

What kind of brain damage do you suffer of?

On 5/3/2022 5:40 PM, Python wrote:
> Petr Olcott wrote:
> ...
>> This is a file that only reads and outputs text lines, thus provides
>> the skeleton for my Simplest TM interpreter. I almost always have some
>> code that I can cut-and-paste this from. I couldn't find it so I had
>> to create this from scratch.
>>
>> I count this as my starting point for my Simplest TM interpreter. I
>> want to see if I can get the entire project completed in less that
>> four hours, including detailed design, coding and debugging and not
>> including user documentation. So far I made great progress on the
>> detailed design in two minutes.
>
> This is also a good starting point for a POSIX compatible operating
> system kernel, you should post it to comp.minix (this previous sentence
> is a pun).
>
> Any decent programmer should be able to design and code a TM in C
> (I've done it in almost all languages I know about, btw) in less than
> four hours. Well. Under the condition that she/he understands what a
> TM is. Unfortunately, Peter, you don't.
>

I proved that I have the complete specification shown below.
The entire architecture of a TM is specified in the first three
paragraphs.

I did have to decide for myself where to put the tape initialization in
the TM description file. The system below requires this to be manually
entered on the command line. That is why I decided to write this myself.

>> It is based on the design of this system yet much simpler:
>> http://www.lns.mit.edu/~dsw/turing/turing.html
>
> You didn't spot why your post can be taken for a joke? Really?
>
> What kind of brain damage do you suffer of?
>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/3/22 11:06 AM, olcott wrote:
> On 5/3/2022 3:46 AM, Aleksy Grabowski wrote:
>> On 5/3/22 01:43, Ben wrote:
>>> Aleksy Grabowski <hurufu@gmail.com> writes:
>>>
>>>>> IF you are defining that your logic system is limited to what
>>>>> Prolog can "Prove", that is fine. Just realize that you have just
>>>>> defined that your
>>>>> logic system can't handle a lot of the real problems in the world,
>>>>> and in particular, it is very limited in the mathematics it can
>>>>> handle.
>>>>> I am pretty sure that Prolog is NOT up to handling the logic needed to
>>>>> handle the mathematics needed to express Godel's G, or the Halting
>>>>> Problem.
>>>>> Thus, your "Proof" that these Theorems are "Wrong" is incorrect, you
>>>>> have only proven that your limited logic system can't reach them in
>>>>> expressibility.
>>>>
>>>> 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).
>>>
>>
>> Just for a reference here is the link to that proof:
>> http://r6.ca/Goedel/goedel1.html
>>
>> Sadly I can't understand it and comment on it, so I just leave it as is.
>>
>
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>
> Incomplete T means that there exists a φ such that φ is not provable or
> refutable in formal system T.
>
> It is true that Gödel's G meets this definition of incompleteness. The
> problem is that the mathematical definition of incompleteness doesn't
> screen out semantically incorrect expressions of language, it simply
> assumes they the do not exist.
>
> This is very very easy to fix:
>
> ∀T ∈ formal_systems
> ∀φ ∈ expression_of_language_T
> (Incorrect(φ) ↔ ((T ⊬ φ) ∧ (T ⊬ ¬φ)))

So, you are just trying to define that anything that would create
incompleteness is an "incorrect" statement.

Have you been able to prove that such a system is actually useful?

Since we don't know if a given expression is actually provable until we
prove it (or prove the converse), you have basicaaly said we can't use
expressions we don't know the answer to, so we can't actually grow the
field.

>
> The above screens out expressions of language that are not logic
> sentences / truth bearers.
>
> https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)#:~:text=In%20mathematical%20logic%2C%20a%20sentence,must%20be%20true%20or%20false.
>

Except you aren't fitering out things that aren't "Truth Bearers", you
are filtering out everthing that hasn't been proven.

IF you adopt the axiom that Truth is Provable, you will find that you
can't express much of mathematics without becoming inconsistent.

If you can live without that, go ahead, most of us aren't.

of course, you seem to not be able to see inconsistantcies, so maybe
youy don't mind your logic being inconsistent, it does have the
advantage that you can prove whatever you want, as long as you ignore
the proofs of the things you don't want by just claiming you have alread
proved to opposite first.

>
> Prolog detects [and rejects] pathological self reference in the Gödel
> sentence
> https://www.researchgate.net/publication/350789898_Prolog_detects_and_rejects_pathological_self_reference_in_the_Godel_sentence
>
>

On 5/3/2022 2:22 PM, André G. Isaak wrote:
> On 2022-05-03 13:12, olcott wrote:
>
>> When T is the entire body of analytic knowledge and φ is the liar
>> paradox, the official mathematical definition of incompleteness
>> determines that the entire body of analytic knowledge is incomplete.
>
> G is not a formalization of The Liar. There is no such formalization in
> the systems Gödel considers.
>
> The Liar results in inconsistency whereas G results in incompleteness.

Not according to the mathematical definition of incompleteness
Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).

Anything and everything that is neither provable nor refutable in some
formal system proves that this formal system IS INCOMPLETE as long as φ
is an expession of language of T.

> This is a major difference between G and The Liar which is why you need
> to stop conflating the two. The Liar only exists in natural language,

That is not true, I think Tarski's way of formalizing the Liar Paradox
may be the best. He describes exactly how it would be formalized and
provides the exactly syntax for formalizing it. I will derive this and
post it sometime soon. I will keep working on this until I am sure that
I have it correctly.

> not in mathematics.
>
> André
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/3/22 10:53 PM, olcott wrote:
> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>> On 2022-05-03 13:12, olcott wrote:
>>
>>> When T is the entire body of analytic knowledge and φ is the liar
>>> paradox, the official mathematical definition of incompleteness
>>> determines that the entire body of analytic knowledge is incomplete.
>>
>> G is not a formalization of The Liar. There is no such formalization
>> in the systems Gödel considers.
>>
>> The Liar results in inconsistency whereas G results in incompleteness.
>
> Not according to the mathematical definition of incompleteness
> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>
> Anything and everything that is neither provable nor refutable in some
> formal system proves that this formal system IS INCOMPLETE as long as φ
> is an expession of language of T.

Your missing that he is meaning that if the Liar is TRUE, it shows the
logic system to be inconsistent.

While G being true just proves that the system is Incomplete.

(G not being False in a system shows that the system is Inconsistent, as
it says we can prove a false statement in the system)

>
>> This is a major difference between G and The Liar which is why you
>> need to stop conflating the two. The Liar only exists in natural
>> language,
>
> That is not true, I think Tarski's way of formalizing the Liar Paradox
> may be the best. He describes exactly how it would be formalized and
> provides the exactly syntax for formalizing it. I will derive this and
> post it sometime soon. I will keep working on this until I am sure that
> I have it correctly.
>
>> not in mathematics.
>>
>> André
>>
>
>

On 5/3/2022 3:03 PM, André G. Isaak wrote:
> On 2022-05-03 12:59, olcott wrote:
>> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>>> On 2022-05-03 11:33, olcott wrote:
>>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>>> On 2022-05-03 11:05, olcott wrote:
>>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>
>>> <snippage>
>>>
>>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>>> explanation.
>>>>>>>
>>>>>>
>>>>>> When G is not provable in PA, how is it shown to be true?
>>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>>
>>>>> Here you're simply begging the question by assuming your own
>>>>> conclusion: that being true and being provable are the same.
>>>>
>>>> This is not any mere assumption.
>>>>
>>>> The only way that any analytic expressions of language are correctly
>>>> determined to be true is:
>>>
>>> 'True' and 'Correctly determined to be true' mean different things.
>>>
>>
>> Yes that seems to be correct.
>> On the other hand calling an expression of language true that has not
>> be 'Correctly determined to be true' is an error.
>
> But calling it a "non-truth bearer" simply because it has not been
> determined to be true would equally be an error.
>

That if correct. If is is impossibly true or false then it is not a
truth bearer.

> And it can be shown (i.e. correctly determined) that G is true, just not
> within the system for which it was constructed.
>

unprovable in the system entails untrue in the system.

>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>> (a) They are defined to be true.
>>>> (b) They are derived from applying truth preserving operations to
>>>> (a) or (b). Prolog knows this on the basis of its facts and rules.
>>>> Facts are (a) and rules are (b). This is also known as sound
>>>> deductive inference.
>>>
>>> These are YOUR assumptions. They have not been demonstrated. And they
>>> are not consistent with the way in which the rest of the world talks
>>> about truth. You are talking about provability, not truth.
>>>
>>
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>>
>>>>> The whole point of Gödel's proof is that they cannot be the same
>>>>> (at least not for non-trivial systems).
>>>>>
>>>>
>>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>>> What is the precise basis for assessing that G is true? please
>>>> provide ALL the steps.
>>>
>>> "True" and "Known to be true" are entirely different things.
>>>
>>
>> Yes, however:
>> If G is claimed to be true then this assertion must be supported by:
>> 'Correctly determined to be true' otherwise the assessment of its
>> truth is no more than a wild guess.
>
> As I said, it can be shown in a higher order system.

Sure, yet it is only true in this system which also makes it provable in
that system.

> But even if it could not be, if we can show that G can only be true in
> cases where it is not provable in T, then there are only two possible
> conclusions:
>

It can't be true in T and unprovable in T.

> Either G is true and unprovable in T, in which case T is incomplete.
> Or G is false and provable in T, in which case T is inconsistent.
>

If G is provable in U then it is true in U.
If G is unprovable in T then it is untrue in T.
G is unprovable in T because it is semantically incorrect.

> Which is exactly what Gödel's theorem states: A system can be consistent
> or it can be complete but it cannot be both. An incomplete system is
> still useful. An inconsistent system is not. Ergo he phrases this as an
> consistent system must be incomplete [with the usual caveats about
> meeting some minimum threshold of expressive power].
>
>>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>>> places)
>>>
>>
>> (2748 + 87)^3 = 22,785,532,875
>> What are you sorting with Srt()?
>
> That was obviously a type. Sqrt().
>
>>> That equation is true but it is unlikely anyone knew this to be true
>>> until now since I very much doubt anyone had previously considered
>>> that specific equation. That's doesn't mean it wasn't true all along.
>>> Just that no one knew it was true.
>>>
>>> There are all sorts of cases where we know one thing without knowing
>>> all things. I can know with certainty that (A ∨ B) is true meaning
>>> that I know that *at least* one of A or B must be true while still
>>> not knowing the truth value of either. These sorts of things occur
>>> all the time.
>>>
>>
>> That is not true. If A and B are syntactically correct expressions of
>> a formal language yet neither one is semantically correct then we have
>> the same case as the Liar Paradox not being a truth bearer, thus (A ∨
>> B) is neither true nor false.
>
> But your whole notion of 'semantically correct' is recognized by no one
> but you and is antithetical to the entire notion of a formal system. And
> what I describe above is a situation which *very* commonly arises in
> proofs. They're called proofs by dilemma and take the form:
>
> A → C
> B → C
> (A ∨ B)
>
> Therefore C
>
> We draw a conclusion from A or B without knowing the truth value of
> either. This strategy, for example, was used by Euclid in his proof that
> no largest prime exists.
>
> If you declare A and B to be 'non-truth bearers' simply because you
> don't know whether they are true or false, then this and many other
> proofs completely fall apart.

It is not because they have unknown truth values.

>
>>> And not being provable in PA and not being provable are also two
>>> different things.
>>>
>>
>> I know that. Yet not being provable in PA also means that G cannot be
>> derived in PA by applying truth preserving operations to the axioms Z
>> of PA or other expressions Y derived from Z or Y.
>>
>> If G is correctly determined to be true then there must be some
>> process detailing the steps of how it is 'Correctly determined to be
>> true'.
>
> Just not in PA.

OK great this is great progress!

>> Lacking these steps one cannot correctly assert that G is true, only
>> that G might possibly be true.
>>
>>>>> The question is not whether it is true but whether it is a truth
>>>>> *bearer*.
>>>>>
>>>>> You make the claim that The Liar is not a truth bearer (a plausible
>>>>> claim depending on one's definitions).
>>>>>
>>>>> You then jump to the conclusion that G is not a truth bearer based
>>>>> on your assertion that it is "equivalent" to The Liar. But it is
>>>>> *NOT* equivalent. It merely bears a close relationship. But you
>>>>> refuse to actually consider what the nature of that relationship;
>>>>> there are both similiarites and differences.
>>>>>
>>>>
>>>> Precise equivalence is defined by this:
>>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>>
>>>> The Liar Paradox can be neither proven nor refuted where T is the
>>>> entire body of analytic knowledge and φ is LP.
>>>
>>> The Liar Paradox is a self-contradiction. The Gödel sentence is not.
>>
>> Until you understand that G can only be correctly asserted to be true
>> in X if G is provable in X. G may be true in X without a proof in X,
>> yet it cannot be correctly asserted to be true in X without such a proof.
>
> This is your confusion, not mine. We can assert that G is not provable
> and that ¬G is also not provable without asserting anything at all about
> whether G is true and still conclude that X is incomplete.

On 5/3/2022 10:12 PM, Richard Damon wrote:
> On 5/3/22 10:53 PM, olcott wrote:
>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>> On 2022-05-03 13:12, olcott wrote:
>>>
>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>> paradox, the official mathematical definition of incompleteness
>>>> determines that the entire body of analytic knowledge is incomplete.
>>>
>>> G is not a formalization of The Liar. There is no such formalization
>>> in the systems Gödel considers.
>>>
>>> The Liar results in inconsistency whereas G results in incompleteness.
>>
>> Not according to the mathematical definition of incompleteness
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> Anything and everything that is neither provable nor refutable in some
>> formal system proves that this formal system IS INCOMPLETE as long as
>> φ is an expession of language of T.
>
> Your missing that he is meaning that if the Liar is TRUE, it shows the
> logic system to be inconsistent.
>

No the LP is semantically incorrect.

> While G being true just proves that the system is Incomplete.
>

Someone here (I think its Andre) now seems to understand that if G is
not provable in F then it is not true in F. If G is true it can only be
true in an other different formal system than F. Tarski says this as
theory and meta-theory.

> (G not being False in a system shows that the system is Inconsistent, as
> it says we can prove a false statement in the system)

G is semantically incorrect thus logically incoherent.

>
>>
>>> This is a major difference between G and The Liar which is why you
>>> need to stop conflating the two. The Liar only exists in natural
>>> language,
>>
>> That is not true, I think Tarski's way of formalizing the Liar Paradox
>> may be the best. He describes exactly how it would be formalized and
>> provides the exactly syntax for formalizing it. I will derive this and
>> post it sometime soon. I will keep working on this until I am sure
>> that I have it correctly.
>>
>>> not in mathematics.
>>>
>>> André
>>>
>>
>>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 2022-05-03 21:24, olcott wrote:
> On 5/3/2022 3:03 PM, André G. Isaak wrote:
>> On 2022-05-03 12:59, olcott wrote:
>>> On 5/3/2022 1:23 PM, André G. Isaak wrote:
>>>> On 2022-05-03 11:33, olcott wrote:
>>>>> On 5/3/2022 12:17 PM, André G. Isaak wrote:
>>>>>> On 2022-05-03 11:05, olcott wrote:
>>>>>>> On 5/3/2022 11:52 AM, André G. Isaak wrote:
>>>>
>>>> <snippage>
>>>>
>>>>>>>> G is very clearly a truth-bearer. Go back and reread my original
>>>>>>>> explanation.
>>>>>>>>
>>>>>>>
>>>>>>> When G is not provable in PA, how is it shown to be true?
>>>>>>> If it is not shown to be true in PA then we have the strawman error.
>>>>>>
>>>>>> Here you're simply begging the question by assuming your own
>>>>>> conclusion: that being true and being provable are the same.
>>>>>
>>>>> This is not any mere assumption.
>>>>>
>>>>> The only way that any analytic expressions of language are
>>>>> correctly determined to be true is:
>>>>
>>>> 'True' and 'Correctly determined to be true' mean different things.
>>>>
>>>
>>> Yes that seems to be correct.
>>> On the other hand calling an expression of language true that has not
>>> be 'Correctly determined to be true' is an error.
>>
>> But calling it a "non-truth bearer" simply because it has not been
>> determined to be true would equally be an error.
>>
>
> That if correct. If is is impossibly true or false then it is not a
> truth bearer.

Neither 'impossibly true' nor 'impossibly false' are meaningful English.
I really wish you would stop using this adverb as if it somehow made
sense. It doesn't.

G is definitely a truth bearer. It states that a specific polynomial
equation has at least one integer solution. Any statement of that form
is either true or false. It is not possible for it to be both. It is not
possible for it to be neither.

>> And it can be shown (i.e. correctly determined) that G is true, just
>> not within the system for which it was constructed.
>>
>
> unprovable in the system entails untrue in the system.

Maybe you should read the actual proof. We proof in some higher order
system T' that G is unprovable in T and that G is true in T.

>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>>
>>>>> (a) They are defined to be true.
>>>>> (b) They are derived from applying truth preserving operations to
>>>>> (a) or (b). Prolog knows this on the basis of its facts and rules.
>>>>> Facts are (a) and rules are (b). This is also known as sound
>>>>> deductive inference.
>>>>
>>>> These are YOUR assumptions. They have not been demonstrated. And
>>>> they are not consistent with the way in which the rest of the world
>>>> talks about truth. You are talking about provability, not truth.
>>>>
>>>
>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>>
>>>>>> The whole point of Gödel's proof is that they cannot be the same
>>>>>> (at least not for non-trivial systems).
>>>>>>
>>>>>
>>>>> When G is not provable in PA, how is it shown to be true (wild guess)?
>>>>> What is the precise basis for assessing that G is true? please
>>>>> provide ALL the steps.
>>>>
>>>> "True" and "Known to be true" are entirely different things.
>>>>
>>>
>>> Yes, however:
>>> If G is claimed to be true then this assertion must be supported by:
>>> 'Correctly determined to be true' otherwise the assessment of its
>>> truth is no more than a wild guess.
>>
>> As I said, it can be shown in a higher order system.
>
> Sure, yet it is only true in this system which also makes it provable in
> that system.

Again, try reading the actual proof. I mean the math part, not the text
part.

>> But even if it could not be, if we can show that G can only be true in
>> cases where it is not provable in T, then there are only two possible
>> conclusions:
>>
>
> It can't be true in T and unprovable in T.

Yes. It can. That is the entire point of the proof which you have not
actually read. The problem is that you seem to have a personal
definition of 'true' which essentially is the same as 'provable'. Yes,
it can't be both provable in T and unprovable in T, but that's a truism.
Not Gödel's theorem.

>> Either G is true and unprovable in T, in which case T is incomplete.
>> Or G is false and provable in T, in which case T is inconsistent.
>>
>
> If G is provable in U then it is true in U.
> If G is unprovable in T then it is untrue in T.
> G is unprovable in T because it is semantically incorrect.

No one besides you recognizes this whole 'semantic incorrectness'
notion. Until you can get people to accept that there is such a thing,
there is no point bringing it up.

>> Which is exactly what Gödel's theorem states: A system can be
>> consistent or it can be complete but it cannot be both. An incomplete
>> system is still useful. An inconsistent system is not. Ergo he phrases
>> this as an consistent system must be incomplete [with the usual
>> caveats about meeting some minimum threshold of expressive power].
>>
>>>> Consider the equation Srt((2748 + 87)^3) = 150,948.776 (to 3 decimal
>>>> places)
>>>>
>>>
>>> (2748 + 87)^3 = 22,785,532,875
>>> What are you sorting with Srt()?
>>
>> That was obviously a type. Sqrt().
>>
>>>> That equation is true but it is unlikely anyone knew this to be true
>>>> until now since I very much doubt anyone had previously considered
>>>> that specific equation. That's doesn't mean it wasn't true all
>>>> along. Just that no one knew it was true.
>>>>
>>>> There are all sorts of cases where we know one thing without knowing
>>>> all things. I can know with certainty that (A ∨ B) is true meaning
>>>> that I know that *at least* one of A or B must be true while still
>>>> not knowing the truth value of either. These sorts of things occur
>>>> all the time.
>>>>
>>>
>>> That is not true. If A and B are syntactically correct expressions of
>>> a formal language yet neither one is semantically correct then we
>>> have the same case as the Liar Paradox not being a truth bearer, thus
>>> (A ∨ B) is neither true nor false.
>>
>> But your whole notion of 'semantically correct' is recognized by no
>> one but you and is antithetical to the entire notion of a formal
>> system. And what I describe above is a situation which *very* commonly
>> arises in proofs. They're called proofs by dilemma and take the form:
>>
>> A → C
>> B → C
>> (A ∨ B)
>>
>> Therefore C
>>
>> We draw a conclusion from A or B without knowing the truth value of
>> either. This strategy, for example, was used by Euclid in his proof
>> that no largest prime exists.
>>
>> If you declare A and B to be 'non-truth bearers' simply because you
>> don't know whether they are true or false, then this and many other
>> proofs completely fall apart.
>
> It is not because they have unknown truth values.

So then what is it? In the case of The Liar I am willing to accept your
claim that it is not a truth-bearer on the grounds that The Liar
effectively has no actual content apart from its own self-referential
claim. That's about the only case I can see it being legitimate to refer
to a declarative sentence as a non-truth bearer (under standard
definitions, truth-bearer and declarative sentence are simply synonyms).

Gödel's G is not like that. It is not self-referential and it does have
actual content.

On 2022-05-03 21:12, Richard Damon wrote:
> On 5/3/22 10:53 PM, olcott wrote:
>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>> On 2022-05-03 13:12, olcott wrote:
>>>
>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>> paradox, the official mathematical definition of incompleteness
>>>> determines that the entire body of analytic knowledge is incomplete.
>>>
>>> G is not a formalization of The Liar. There is no such formalization
>>> in the systems Gödel considers.
>>>
>>> The Liar results in inconsistency whereas G results in incompleteness.
>>
>> Not according to the mathematical definition of incompleteness
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>
>> Anything and everything that is neither provable nor refutable in some
>> formal system proves that this formal system IS INCOMPLETE as long as
>> φ is an expession of language of T.
>
> Your missing that he is meaning that if the Liar is TRUE, it shows the
> logic system to be inconsistent.

Actually, it doesn't matter whether it is true or false.

What's relevant here is that it is trivially easy to prove The Liar
using a simple reductio ad absurdum. Unfortunately, it is equally
trivially easy to prove ¬(The Liar) using a reductio of the same form.

That's very different from G, where no proof exists of either G or of ¬G.

The Liar leads to inconsistency.
The sentence 'This sentence is true' would be a natural language example
which leads to incompleteness.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/3/2022 11:06 PM, André G. Isaak wrote:
> On 2022-05-03 21:12, Richard Damon wrote:
>> On 5/3/22 10:53 PM, olcott wrote:
>>> On 5/3/2022 2:22 PM, André G. Isaak wrote:
>>>> On 2022-05-03 13:12, olcott wrote:
>>>>
>>>>> When T is the entire body of analytic knowledge and φ is the liar
>>>>> paradox, the official mathematical definition of incompleteness
>>>>> determines that the entire body of analytic knowledge is incomplete.
>>>>
>>>> G is not a formalization of The Liar. There is no such formalization
>>>> in the systems Gödel considers.
>>>>
>>>> The Liar results in inconsistency whereas G results in incompleteness.
>>>
>>> Not according to the mathematical definition of incompleteness
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>>
>>> Anything and everything that is neither provable nor refutable in
>>> some formal system proves that this formal system IS INCOMPLETE as
>>> long as φ is an expession of language of T.
>>
>> Your missing that he is meaning that if the Liar is TRUE, it shows the
>> logic system to be inconsistent.
>
> Actually, it doesn't matter whether it is true or false.
>
> What's relevant here is that it is trivially easy to prove The Liar
> using a simple reductio ad absurdum. Unfortunately, it is equally
> trivially easy to prove ¬(The Liar) using a reductio of the same form.
>

Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
The Liar Paradox plugs right in to this
making it equivalent to Gödel's G.

> That's very different from G, where no proof exists of either G or of ¬G.
>
> The Liar leads to inconsistency.
> The sentence 'This sentence is true' would be a natural language example
> which leads to incompleteness.
>
> André
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 2022-05-04 04:06:43 +0000, André G. Isaak said:

> That's very different from G, where no proof exists of either G or of ¬G.

However, (G ∨ ¬G) is provable in PA.

Mikko

On 5/3/22 11:24 PM, olcott wrote:
>
> unprovable in the system entails untrue in the system.

Your fundamental error!

Unless the system has define Truth to require provable, which
mathematics hasn't, this is an error, as it isn't a fundamental error.

There are many things that we know have a truth value, but are not
provable or refutable.

And one big effect of your statement is that you effectively disallow
the reasoning about a statement unless you happen to know if it is true
or not. Your logic system precludes thinking about the unknown.

As an aside, it also means you your are declairing that the Bible, that
you like to quote out of is untrue, as is God, because they are not
actually provable in any accepted logic system. This means that by your
own definition, you are now a liar, as you have made assertions based on
a known untrue statement.

Actually, your problem is you don't think your idea out far enough to se
their actually consequences, because your mind is just to simple to
understand things this complicated.

On 2022-05-04 00:17, olcott wrote:

> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
> The Liar Paradox plugs right in to this

How exactly does it 'plug right into the above'? As I just said, LP *is*
provable. ¬LP is also provable.

That's what it means to be a contradiction.

André

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/4/2022 1:49 AM, Mikko wrote:
> On 2022-05-04 04:06:43 +0000, André G. Isaak said:
>
>> That's very different from G, where no proof exists of either G or of ¬G.
>
> However, (G ∨ ¬G) is provable in PA.
>
> Mikko
>

Incomplete(PA) ↔ ∃G ((PA ⊬ G) ∧ (PA ⊬ ¬G)).
Then Gödel is wrong.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/4/2022 9:02 AM, André G. Isaak wrote:
> On 2022-05-04 00:17, olcott wrote:
>
>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>> The Liar Paradox plugs right in to this
>
> How exactly does it 'plug right into the above'? As I just said, LP *is*
> provable. ¬LP is also provable.
>
> That's what it means to be a contradiction.
>
> André
>

LP exactly meets the mathematical definition of incompleteness, this
will not be clear until after I correctly formalize it and specify the
formal system to which it belongs. Tarski seems to provide the best head
start on formalizing the LP.

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/4/22 3:01 PM, olcott wrote:
> On 5/4/2022 9:02 AM, André G. Isaak wrote:
>> On 2022-05-04 00:17, olcott wrote:
>>
>>> Incomplete(T) ↔ ∃φ ((T ⊬ φ) ∧ (T ⊬ ¬φ)).
>>> The Liar Paradox plugs right in to this
>>
>> How exactly does it 'plug right into the above'? As I just said, LP
>> *is* provable. ¬LP is also provable.
>>
>> That's what it means to be a contradiction.
>>
>> André
>>
>
> LP exactly meets the mathematical definition of incompleteness, this
> will not be clear until after I correctly formalize it and specify the
> formal system to which it belongs. Tarski seems to provide the best head
> start on formalizing the LP.
>

No, because it doesn't meet the requirements to be a φ

As you have mentioned elsewhere, the statement of the Liar Paradox isn't
a Truth Beared, which is part of the requirements built into what φ
needs to be.

Note, your statement of Incompleteness is incomplete without the
defintion of what the various terms mean.

This seems to be a common problem with you, you remove the conditions
and defintions from statements and the misuse them.

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).

> 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.
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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.
>>>
>>
>>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

On 5/4/22 11:02 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, 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.

Nope, shows you don't understand the proof. Have you actually read it,
or just the 'cliff notes' version. You know, the one with the actual

>
>>> 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.

Except that G isn't self-contradictory. The actual G makes a statement
of a mathematical problem and asks if it has a solution. That sort of
statement is ALWAYS a Truth Bearer.

I think your problem is you don't even uderstand that power and limits
of semantics.

>
> Any unprovable expression of any formal or natural language is simply
> untrue and nothing more.

Nope. Truth does not mean Provable. An Unproven statement (or even
unprovable statement) might still be True, it just can't be KNOWN. You
confuse truth with knowledge, maybe because you have too much ego and
think your knowledge defines what is.

By your statement, the Bible is untrue, and you are thus a Liar for
making statements based on it being true.

We can't beleive the words of a Liar, so we shouldn't beleive you when
you claim Truth implies Provable.

Yes, you can build a logic system that defines that, in that system, a
statement is only a Truth Bearer is it is provable or refutable, but
such a system can not handle our mathematics (at least not and stay
consistent).

All you are doing is showing you don't understand how logic actually works.

>
>>>
>>>
>>>> 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,

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.
>>>
>>
>>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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é

--
To email remove 'invalid' & replace 'gm' with well known Google mail
service.

On 5/5/2022 1:06 PM, André G. Isaak wrote:
> 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é
>

From the quote below:
We are therefore confronted with a proposition which asserts its own
unprovability.

Gödel says:
The analogy between this result and Richard’s antinomy leaps to the eye;
there is also a close relationship with the “liar” antinomy,14 since the
undecidable proposition [R(q); q] states precisely that q belongs to K,
i.e. according to (1), that [R(q); q] is not provable. We are therefore
confronted with a proposition which asserts its own unprovability.

Tarski proof is based on this exact same thing in its first step:
https://liarparadox.org/Tarski_275_276.pdf

(1) x ⋶ Pr if and only if p
where the symbol 'p' represents the whole sentence x
and Pr means Provable

This is a Tarski was of saying:
"a proposition which asserts its own unprovability."

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer

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:
>> 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 Tarski's theory p <is> the formalized liar paradox.

> 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.
>

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.

>>
>>>>
>>>>
>>>>> 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.
>>>>>
>>>>
>>>>
>>>
>>
>>
>

--
Copyright 2022 Pete Olcott "Talent hits a target no one else can hit;
Genius hits a target no one else can see." Arthur Schopenhauer