On 1/22/2024 5:51 AM, Mikko wrote:
> On 2024-01-22 00:46:31 +0000, olcott said:
>
>> On 1/21/2024 6:27 PM, Richard Damon wrote:
>>> On 1/21/24 6:17 PM, olcott wrote:
>>>> On 1/21/2024 5:00 PM, Richard Damon wrote:
>>>>> On 1/21/24 5:39 PM, olcott wrote:
>>>>>> On 1/21/2024 4:32 PM, Richard Damon wrote:
>>>>>>> On 1/21/24 4:55 PM, olcott wrote:
>>>>>>>> On 1/21/2024 3:52 PM, Richard Damon wrote:
>>>>>>>>> On 1/21/24 3:51 PM, olcott wrote:
>>>>>>>>>> On 1/21/2024 2:43 PM, Richard Damon wrote:
>>>>>>>>>>> On 1/21/24 3:15 PM, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 2:06 PM, Richard Damon wrote:
>>>>>>>>>>>>> On 1/21/24 2:22 PM, wij wrote:
>>>>>>>>>>>>>> I just found an article about the Halting Problem.
>>>>>>>>>>>>>> https://arxiv.org/pdf/1906.05340.pdf
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> In the conclusion section:
>>>>>>>>>>>>>> The idea of a universal halting test seems reasonable, but
>>>>>>>>>>>>>> cannot be
>>>>>>>>>>>>>> for-
>>>>>>>>>>>>>> malised as a consistent specification. It has no model and
>>>>>>>>>>>>>> does not
>>>>>>>>>>>>>> exist as
>>>>>>>>>>>>>> a conceptual object. Assuming its conceptual existence
>>>>>>>>>>>>>> leads to a
>>>>>>>>>>>>>> paradox.
>>>>>>>>>>>>>> The halting problem is universally used in university
>>>>>>>>>>>>>> courses on
>>>>>>>>>>>>>> Computer
>>>>>>>>>>>>>> Science to illustrate the limits of computation. Hehner
>>>>>>>>>>>>>> claims the
>>>>>>>>>>>>>> halting
>>>>>>>>>>>>>> problem is misconceived......
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> It looks like what olcott now is claiming. Am I missing
>>>>>>>>>>>>>> something?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> I think the problem he is seeing is that the property of
>>>>>>>>>>>>> "Halting" can not be uniformly determined in Finite Time.
>>>>>>>>>>>>>
>>>>>>>>>>>>> That is all that I can get from his statement of:
>>>>>>>>>>>>>
>>>>>>>>>>>>> The idea of a universal halting test seems reasonable, but
>>>>>>>>>>>>> cannot be formalised as a consistent specification.
>>>>>>>>>>>>>
>>>>>>>>>>>>> There certainly CAN be defined formal test that define
>>>>>>>>>>>>> Halting, the issue is that non-halting is defined by the
>>>>>>>>>>>>> non-existence of a number N for the number of steps needed
>>>>>>>>>>>>> to reach a final state.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Some people just don't like the fact that it can be
>>>>>>>>>>>>> absolutely provable what the answer is (and thus
>>>>>>>>>>>>> unknowable), even if we know from the definition, that it
>>>>>>>>>>>>> must be one or the other.
>>>>>>>>>>>>>
>>>>>>>>>>>>> This leads us to a great divide in logics. The classical
>>>>>>>>>>>>> branch accepts that some truth is only established by
>>>>>>>>>>>>> infinite chains of connections, and thus can not be proven
>>>>>>>>>>>>> with a finite proof, and thus is unknowable.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Others don't accept that, and require Truth to be only
>>>>>>>>>>>>> established by Finite chains. The problem then is, such
>>>>>>>>>>>>> logic system need to greatly limit the domain they attempt
>>>>>>>>>>>>> to cover, as otherwise you get into endless chains of
>>>>>>>>>>>>> asking if a question can be asked, at which point you need
>>>>>>>>>>>>> to ask if you can even ask about asking the questions. Only
>>>>>>>>>>>>> when the domain is restricted in a way that the answer MUST
>>>>>>>>>>>>> be determinable with finite work, can we break the cycle.
>>>>>>>>>>>>>
>>>>>>>>>>>>> For instance, if we limit ourselves to Finite State
>>>>>>>>>>>>> Machines (which could be Turing Machines with a fixed
>>>>>>>>>>>>> finite tape, or a classical program in a computer with
>>>>>>>>>>>>> limited memory) then we can be sure that the answer is
>>>>>>>>>>>>> determinable with a finite amount of work.
>>>>>>>>>>>>
>>>>>>>>>>>> Tarski did not understand that the Liar Paradox is not a
>>>>>>>>>>>> truth bearer
>>>>>>>>>>>> thus cannot possibly be true or false. His ignorance got him
>>>>>>>>>>>> so confused
>>>>>>>>>>>> that he thought that he proved that True(L,x) cannot be
>>>>>>>>>>>> defined because
>>>>>>>>>>>> True(Tarski_theory, LP) does not work.
>>>>>>>>>>>
>>>>>>>>>>> I'll ask one more time, exactly WHERE in the proof did he do
>>>>>>>>>>> this? He shows that if True(L, x) exists that the Liar
>>>>>>>>>>> Paradox is a true statement, but not what you say.
>>>>>>>>>>
>>>>>>>>>> "He shows that if True(L, x) exists that the Liar Paradox is a
>>>>>>>>>> true."
>>>>>>>>>>
>>>>>>>>>> That is a perfect paraphrase of my position of what he said.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Nope, you said that he assumed the Liars Paradox has a logic
>>>>>>>>> value.
>>>>>>>>>
>>>>>>>>> The assumption was just that True(L,x) existed.
>>>>>>>>>
>>>>>>>>
>>>>>>>> No that it only half of the assumption.
>>>>>>>> The other half is that True(tarski_theory, "this sentence is not
>>>>>>>> true")
>>>>>>>> must be true or false. That half was Tarksi's fatal flaw.
>>>>>>>>
>>>>>>>
>>>>>>> Where do you see that as an INPUT assumption, and not a result of
>>>>>>> a proof?
>>>>>>>
>>>>>>> LINE please.
>>>>>>
>>>>>> line (3)
>>>>>
>>>>> You mean the (3) on page 275?
>>>>>
>>>>> The one preeeded by: "from (1) and (2) we obtain immediately"
>>>>>
>>>>> Thus (3) isn't an assumption but a proven statement.
>>>>>
>>>>> Also (3) says x is not Provable if and only if x is not True
>>>>>
>>>>> (Which applies only for a particuar x that was derived in (1).
>>>>>
>>>>>
>>>>> Of course, you don't accept that statement, but you need to try to
>>>>> find the error in that logic (which I doubt exists)
>>>>>
>>>>> YOu are just showing how little you understand about how logic
>>>>> works. You can't seem to read these papers and understand them.
>>>>
>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>
>>>> Is like assuming that cows are dogs because it rejects
>>>> the way that an actual True(L, x) predicate works:
>>>> ∀x ∈ L (True(L,x) ≡ (L ⊢ x))
>>>>
>>>
>>> But that is a statement PROVEN from the previous,
>>
>> We erase lines (1) and (2) and replace line (3) with this
>> (3) x ∈ Provable if and only if x ∈ True.
>
> You cannot erase a line except in your own copy. Other copies still
> have the line.
>
> An erased proven statement is still proven.
>
> Mikko
>

On 1/22/2024 6:23 AM, Richard Damon wrote:
> On 1/21/24 11:37 PM, olcott wrote:
>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>> On 1/21/24 11:01 PM, olcott wrote:
>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not
>>>>>>>>>>>>>>> valid.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>>> it's unprovable. There are different ways to find out that
>>>>>>>>>>>>> it's unprovable, or different ways to understand that it's
>>>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>>
>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>
>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> But there are x that are unprovable in L because the chain to
>>>>>>>>>>> them is infinitely long, which makes them true but unprovale.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>
>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> WHy is it "erroneous", it is a simple statement previously proven.
>>>>>>>>>
>>>>>>>>
>>>>>>>> He proved that there are some things that we know
>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>> they are true?
>>>>>>>>
>>>>>>>
>>>>>>> No, he proved that there are some things that ARE true that we
>>>>>>> can not prove to be true.
>>>>>>>
>>>>>>
>>>>>> How the Hell is he going to do that on his basis
>>>>>> of the Liar Paradox?
>>>>>>
>>>>>
>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>
>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>> He get his line (1) directly from the Liar Paradox
>>>>
>>>> Below he shows how he transforms the Liar Paradox
>>>> x ∉ True if and only if p
>>>>
>>>> into his line (1) by replacing "Tr" (for True)
>>>> with 'Pr" (for provable) Here is his line
>>>> (1) x ∉ Provable if and only if p
>>>>
>>>> <page 275>
>>>>     In accordance with the first
>>>>     part of Th. I we can obtain the negation of one of the sentences
>>>>     in condition (α) of convention T of § 3 as a consequence of the
>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in this
>>>>     convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
>>>> </page 275>
>>>>
>>>> <page 248> Liar Paradox
>>>>     Should we succeed in constructing in the metalanguage
>>>>     a correct definition of truth, then
>>>>
>>>>     It would
>>>>     then be possible to reconstruct the antinomy of the liar in the
>>>>     metalanguage, by forming in the language itself a sentence x
>>>>     such that the sentence of the metalanguage which is correlated
>>>>     with x asserts that x is not a true sentence.
>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>> </page 248>
>>>>
>>>> Many people today are simply too stupid to understand
>>>> that the Liar Paradox is simply not a truth bearer
>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>
>>>> When Tarski assumes the Liar Paradox as a premise
>>>> this must be rejected and over-ruled.
>>>
>>> Where does he assume it as a premise?
>>>
>>
>> His line (1) is a premise.
>
> Then why does he say, "In other words, we can construct ... " just above
> it.
>
> (1) is a CONCLUSION from the previous paragraph.
>
> you clearly don't know much about logic.
>
>>
>>>>
>>>> (1) x ∉ Provable if and only if p
>>>> must be corrected to say
>>>> (1) x ∈ Provable if and only if p
>>>>
>>>
>>> What was actually wrong with (1). You haven't shown the error in logic.
>>
>> His line (1) <is> an adapted form of the actual Liar
>> Paradox as I have shown by the quotes above.
>
> NO, the liar paradox says NOTHING about "Provable".

On 1/22/24 19:44, olcott wrote:
> It turns out the the key error is Tarski's line (1)
> that began as the Liar Paradox
> (1) x ∉ True if and only if p
> and was transformed into this
> (1) x ∉ Provable if and only if p
>
> Intelligent people understand that the Liar Paradox is
> not a truth bearer, thus asking whether it is true or
> false is like asking whether a question is true or false.
> Is this sentence true or false: What time is it?
>
>

Stupid people who think they are intelligent understand that.

People who are actually intelligent understand that every logical
formula is a truth bearer.

On 1/22/24 19:39, olcott wrote:
> On 1/22/2024 4:17 AM, Mikko wrote:
>> On 2024-01-22 02:18:35 +0000, olcott said:
>>
>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>> On 1/22/24 02:43, olcott wrote:
>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>
>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>> pathologically self-referential, making his argument invalid?
>>>>>>>>>>>>
>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>
>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>
>>>>>>>>
>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects ALL
>>>>>>>> cycles, even if they don't cause logical issues (as I understand
>>>>>>>> it)
>>>>>>>
>>>>>>> As you fail to understand it.
>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>> automatically generated the directed graph of the
>>>>>>> evaluation sequence of any of its expressions.
>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>
>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>
>>>>>>
>>>>>> You are rebutting the infinite formulas such as
>>>>>> ¬True(¬True(¬True(...)))
>>>>>>
>>>>>> But this is already in the standard theory. Infinite formulas such
>>>>>> as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>
>>>>>> Olcott doesn't understand that diagonalization is not the same as
>>>>>> infinite recursion.
>>>>>
>>>>> Finally a reply that is not nonsense.
>>>>> Diagonalization only knows that for some reason or another
>>>>> x is unprovable in L.
>>>>
>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>> unprovable. There are different ways to find out that it's
>>>> unprovable, or different ways to understand that it's unprovable,
>>>> but not reasons why it's unprovable.
>>>
>>> If the reason that x is unprovable in L is that x
>>> is semantically incorrect in L then instead of saying
>>> that x is undecidable in L the decider rejects x
>>> as invalid input.
>>>
>>> This what Tarski should have done.
>>
>> In a formal theory nothing is semantically anything.
>
> That it the reason why formal theories get confused
> and make semantic errors that are invisible to them.

Nobody is talking about semantics except for you.
What is the formal truth value of x?

>
>> The semantics only
>> enter when the theory is interpreted. In a first order theory if x is
>> undecidable then it is true in some models and false in all others.
>> If neither x nor ¬x is provable you can add either one (but not both)
>> to the axioms of the theory and get another theory where x is decidable.
>>
>> Mikko
>>
>

On 1/22/2024 1:00 PM, immibis wrote:
> On 1/22/24 19:39, olcott wrote:
>> On 1/22/2024 4:17 AM, Mikko wrote:
>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>
>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>>> pathologically self-referential, making his argument invalid?
>>>>>>>>>>>>>
>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>
>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects ALL
>>>>>>>>> cycles, even if they don't cause logical issues (as I
>>>>>>>>> understand it)
>>>>>>>>
>>>>>>>> As you fail to understand it.
>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>> automatically generated the directed graph of the
>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>
>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>
>>>>>>>
>>>>>>> You are rebutting the infinite formulas such as
>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>
>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>
>>>>>>> Olcott doesn't understand that diagonalization is not the same as
>>>>>>> infinite recursion.
>>>>>>
>>>>>> Finally a reply that is not nonsense.
>>>>>> Diagonalization only knows that for some reason or another
>>>>>> x is unprovable in L.
>>>>>
>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>> unprovable. There are different ways to find out that it's
>>>>> unprovable, or different ways to understand that it's unprovable,
>>>>> but not reasons why it's unprovable.
>>>>
>>>> If the reason that x is unprovable in L is that x
>>>> is semantically incorrect in L then instead of saying
>>>> that x is undecidable in L the decider rejects x
>>>> as invalid input.
>>>>
>>>> This what Tarski should have done.
>>>
>>> In a formal theory nothing is semantically anything.
>>
>> That it the reason why formal theories get confused
>> and make semantic errors that are invisible to them.
>
> Nobody is talking about semantics except for you.
*That is their mistake*

> What is the formal truth value of x?

Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.

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

On 1/22/24 20:08, olcott wrote:
> On 1/22/2024 1:00 PM, immibis wrote:
>> On 1/22/24 19:39, olcott wrote:
>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>
>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>>>> pathologically self-referential, making his argument invalid?
>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>
>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>> understand it)
>>>>>>>>>
>>>>>>>>> As you fail to understand it.
>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>
>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>
>>>>>>>>
>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>
>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>
>>>>>>>> Olcott doesn't understand that diagonalization is not the same
>>>>>>>> as infinite recursion.
>>>>>>>
>>>>>>> Finally a reply that is not nonsense.
>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>> x is unprovable in L.
>>>>>>
>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>> unprovable. There are different ways to find out that it's
>>>>>> unprovable, or different ways to understand that it's unprovable,
>>>>>> but not reasons why it's unprovable.
>>>>>
>>>>> If the reason that x is unprovable in L is that x
>>>>> is semantically incorrect in L then instead of saying
>>>>> that x is undecidable in L the decider rejects x
>>>>> as invalid input.
>>>>>
>>>>> This what Tarski should have done.
>>>>
>>>> In a formal theory nothing is semantically anything.
>>>
>>> That it the reason why formal theories get confused
>>> and make semantic errors that are invisible to them.
>>
>> Nobody is talking about semantics except for you.
> *That is their mistake*
>
>> What is the formal truth value of x?
>
> Something that seems over your head is the self-contradictory
> sentences cannot possibly have a truth value.
>
>
Every logical formula has a truth value.

On 1/22/2024 1:16 PM, immibis wrote:
> On 1/22/24 20:08, olcott wrote:
>> On 1/22/2024 1:00 PM, immibis wrote:
>>> On 1/22/24 19:39, olcott wrote:
>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>
>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>>>>> pathologically self-referential, making his argument
>>>>>>>>>>>>>>> invalid?
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>>> understand it)
>>>>>>>>>>
>>>>>>>>>> As you fail to understand it.
>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>
>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>
>>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>>
>>>>>>>>> Olcott doesn't understand that diagonalization is not the same
>>>>>>>>> as infinite recursion.
>>>>>>>>
>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>> x is unprovable in L.
>>>>>>>
>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>> unprovable, or different ways to understand that it's unprovable,
>>>>>>> but not reasons why it's unprovable.
>>>>>>
>>>>>> If the reason that x is unprovable in L is that x
>>>>>> is semantically incorrect in L then instead of saying
>>>>>> that x is undecidable in L the decider rejects x
>>>>>> as invalid input.
>>>>>>
>>>>>> This what Tarski should have done.
>>>>>
>>>>> In a formal theory nothing is semantically anything.
>>>>
>>>> That it the reason why formal theories get confused
>>>> and make semantic errors that are invisible to them.
>>>
>>> Nobody is talking about semantics except for you.
>> *That is their mistake*
>>
>>> What is the formal truth value of x?
>>
>> Something that seems over your head is the self-contradictory
>> sentences cannot possibly have a truth value.
>>
>>
> Every logical formula has a truth value.

LP := ~True(LP)
specifies an infinite evaluation sequence as shown
in cycle of the directed graph of this sequence.
G := ~Provable(G) has the exact same issue.

That you don't comprehend these things is no rebuttal what-so-ever.

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

On 1/22/24 20:47, olcott wrote:
> On 1/22/2024 1:16 PM, immibis wrote:
>> On 1/22/24 20:08, olcott wrote:
>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>> On 1/22/24 19:39, olcott wrote:
>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>
>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>>>>>> pathologically self-referential, making his argument
>>>>>>>>>>>>>>>> invalid?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>>>> understand it)
>>>>>>>>>>>
>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>
>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>
>>>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>>>
>>>>>>>>>> Olcott doesn't understand that diagonalization is not the same
>>>>>>>>>> as infinite recursion.
>>>>>>>>>
>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>> x is unprovable in L.
>>>>>>>>
>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>
>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>> as invalid input.
>>>>>>>
>>>>>>> This what Tarski should have done.
>>>>>>
>>>>>> In a formal theory nothing is semantically anything.
>>>>>
>>>>> That it the reason why formal theories get confused
>>>>> and make semantic errors that are invisible to them.
>>>>
>>>> Nobody is talking about semantics except for you.
>>> *That is their mistake*
>>>
>>>> What is the formal truth value of x?
>>>
>>> Something that seems over your head is the self-contradictory
>>> sentences cannot possibly have a truth value.
>>>
>>>
>> Every logical formula has a truth value.
>
> LP := ~True(LP)

True(LP) is not a logical formula. Gödel proved that.

On 1/22/2024 1:56 PM, immibis wrote:
> On 1/22/24 20:47, olcott wrote:
>> On 1/22/2024 1:16 PM, immibis wrote:
>>> On 1/22/24 20:08, olcott wrote:
>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>
>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>>>>> understand it)
>>>>>>>>>>>>
>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>
>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>
>>>>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>>>>
>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>
>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>> x is unprovable in L.
>>>>>>>>>
>>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>
>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>> as invalid input.
>>>>>>>>
>>>>>>>> This what Tarski should have done.
>>>>>>>
>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>
>>>>>> That it the reason why formal theories get confused
>>>>>> and make semantic errors that are invisible to them.
>>>>>
>>>>> Nobody is talking about semantics except for you.
>>>> *That is their mistake*
>>>>
>>>>> What is the formal truth value of x?
>>>>
>>>> Something that seems over your head is the self-contradictory
>>>> sentences cannot possibly have a truth value.
>>>>
>>>>
>>> Every logical formula has a truth value.
>>
>> LP := ~True(LP)
>
> True(LP) is not a logical formula. Gödel proved that.
>
>

He proved no such thing.

He proved that G cannot be proved in PA yet can be proved in
metamathematics.

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

On 1/22/24 21:30, olcott wrote:
> On 1/22/2024 1:56 PM, immibis wrote:
>> On 1/22/24 20:47, olcott wrote:
>>> On 1/22/2024 1:16 PM, immibis wrote:
>>>> On 1/22/24 20:08, olcott wrote:
>>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>>
>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>
>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>
>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>
>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not
>>>>>>>>>>>> valid.
>>>>>>>>>>>>
>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>>
>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>
>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>
>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>> as invalid input.
>>>>>>>>>
>>>>>>>>> This what Tarski should have done.
>>>>>>>>
>>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>>
>>>>>>> That it the reason why formal theories get confused
>>>>>>> and make semantic errors that are invisible to them.
>>>>>>
>>>>>> Nobody is talking about semantics except for you.
>>>>> *That is their mistake*
>>>>>
>>>>>> What is the formal truth value of x?
>>>>>
>>>>> Something that seems over your head is the self-contradictory
>>>>> sentences cannot possibly have a truth value.
>>>>>
>>>>>
>>>> Every logical formula has a truth value.
>>>
>>> LP := ~True(LP)
>>
>> True(LP) is not a logical formula. Gödel proved that.
>>
>>
>
> He proved no such thing.
>
> He proved that G cannot be proved in PA yet can be proved in
> metamathematics.
>

On 1/22/2024 5:20 PM, immibis wrote:
> On 1/22/24 21:30, olcott wrote:
>> On 1/22/2024 1:56 PM, immibis wrote:
>>> On 1/22/24 20:47, olcott wrote:
>>>> On 1/22/2024 1:16 PM, immibis wrote:
>>>>> On 1/22/24 20:08, olcott wrote:
>>>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>>>
>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>
>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not
>>>>>>>>>>>>> valid.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>>>
>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>
>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>>
>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>> as invalid input.
>>>>>>>>>>
>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>
>>>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>>>
>>>>>>>> That it the reason why formal theories get confused
>>>>>>>> and make semantic errors that are invisible to them.
>>>>>>>
>>>>>>> Nobody is talking about semantics except for you.
>>>>>> *That is their mistake*
>>>>>>
>>>>>>> What is the formal truth value of x?
>>>>>>
>>>>>> Something that seems over your head is the self-contradictory
>>>>>> sentences cannot possibly have a truth value.
>>>>>>
>>>>>>
>>>>> Every logical formula has a truth value.
>>>>
>>>> LP := ~True(LP)
>>>
>>> True(LP) is not a logical formula. Gödel proved that.
>>>
>>>
>>
>> He proved no such thing.
>>
>> He proved that G cannot be proved in PA yet can be proved in
>> metamathematics.
>>
>
> I don't think you get this. Every system has a G that can't be proved in
> that system,

On 1/23/24 00:31, olcott wrote:
> On 1/22/2024 5:20 PM, immibis wrote:
>> On 1/22/24 21:30, olcott wrote:
>>> On 1/22/2024 1:56 PM, immibis wrote:
>>>> On 1/22/24 20:47, olcott wrote:
>>>>> On 1/22/2024 1:16 PM, immibis wrote:
>>>>>> On 1/22/24 20:08, olcott wrote:
>>>>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>>>>
>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not
>>>>>>>>>>>>>> valid.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>>>>
>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>
>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>> it's unprovable. There are different ways to find out that
>>>>>>>>>>>> it's unprovable, or different ways to understand that it's
>>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>
>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>> as invalid input.
>>>>>>>>>>>
>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>
>>>>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>>>>
>>>>>>>>> That it the reason why formal theories get confused
>>>>>>>>> and make semantic errors that are invisible to them.
>>>>>>>>
>>>>>>>> Nobody is talking about semantics except for you.
>>>>>>> *That is their mistake*
>>>>>>>
>>>>>>>> What is the formal truth value of x?
>>>>>>>
>>>>>>> Something that seems over your head is the self-contradictory
>>>>>>> sentences cannot possibly have a truth value.
>>>>>>>
>>>>>>>
>>>>>> Every logical formula has a truth value.
>>>>>
>>>>> LP := ~True(LP)
>>>>
>>>> True(LP) is not a logical formula. Gödel proved that.
>>>>
>>>>
>>>
>>> He proved no such thing.
>>>
>>> He proved that G cannot be proved in PA yet can be proved in
>>> metamathematics.
>>>
>>
>> I don't think you get this. Every system has a G that can't be proved
>> in that system,
>
> Yet can be proved in metamathematics.
>
Is metamathematics a system?

On 1/22/2024 6:10 PM, immibis wrote:
> On 1/23/24 00:31, olcott wrote:
>> On 1/22/2024 5:20 PM, immibis wrote:
>>> On 1/22/24 21:30, olcott wrote:
>>>> On 1/22/2024 1:56 PM, immibis wrote:
>>>>> On 1/22/24 20:47, olcott wrote:
>>>>>> On 1/22/2024 1:16 PM, immibis wrote:
>>>>>>> On 1/22/24 20:08, olcott wrote:
>>>>>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>>>>>
>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not
>>>>>>>>>>>>>>> valid.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>
>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>>> it's unprovable. There are different ways to find out that
>>>>>>>>>>>>> it's unprovable, or different ways to understand that it's
>>>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>>
>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>
>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>
>>>>>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>>>>>
>>>>>>>>>> That it the reason why formal theories get confused
>>>>>>>>>> and make semantic errors that are invisible to them.
>>>>>>>>>
>>>>>>>>> Nobody is talking about semantics except for you.
>>>>>>>> *That is their mistake*
>>>>>>>>
>>>>>>>>> What is the formal truth value of x?
>>>>>>>>
>>>>>>>> Something that seems over your head is the self-contradictory
>>>>>>>> sentences cannot possibly have a truth value.
>>>>>>>>
>>>>>>>>
>>>>>>> Every logical formula has a truth value.
>>>>>>
>>>>>> LP := ~True(LP)
>>>>>
>>>>> True(LP) is not a logical formula. Gödel proved that.
>>>>>
>>>>>
>>>>
>>>> He proved no such thing.
>>>>
>>>> He proved that G cannot be proved in PA yet can be proved in
>>>> metamathematics.
>>>>
>>>
>>> I don't think you get this. Every system has a G that can't be proved
>>> in that system,
>>
>> Yet can be proved in metamathematics.
>>
> Is metamathematics a system?

On 1/22/24 1:59 PM, olcott wrote:
> On 1/22/2024 6:23 AM, Richard Damon wrote:
>> On 1/21/24 11:37 PM, olcott wrote:
>>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>>> On 1/21/24 11:01 PM, olcott wrote:
>>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already
>>>>>>>>>>>>>>>> not valid.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not
>>>>>>>>>>>>>>>> the same as infinite recursion.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>>>> it's unprovable. There are different ways to find out that
>>>>>>>>>>>>>> it's unprovable, or different ways to understand that it's
>>>>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>>>
>>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>>
>>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> But there are x that are unprovable in L because the chain
>>>>>>>>>>>> to them is infinitely long, which makes them true but
>>>>>>>>>>>> unprovale.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>>
>>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> WHy is it "erroneous", it is a simple statement previously
>>>>>>>>>> proven.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> He proved that there are some things that we know
>>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>>> they are true?
>>>>>>>>>
>>>>>>>>
>>>>>>>> No, he proved that there are some things that ARE true that we
>>>>>>>> can not prove to be true.
>>>>>>>>
>>>>>>>
>>>>>>> How the Hell is he going to do that on his basis
>>>>>>> of the Liar Paradox?
>>>>>>>
>>>>>>
>>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>>
>>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>>> He get his line (1) directly from the Liar Paradox
>>>>>
>>>>> Below he shows how he transforms the Liar Paradox
>>>>> x ∉ True if and only if p
>>>>>
>>>>> into his line (1) by replacing "Tr" (for True)
>>>>> with 'Pr" (for provable) Here is his line
>>>>> (1) x ∉ Provable if and only if p
>>>>>
>>>>> <page 275>
>>>>>     In accordance with the first
>>>>>     part of Th. I we can obtain the negation of one of the sentences
>>>>>     in condition (α) of convention T of § 3 as a consequence of the
>>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in this
>>>>>     convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
>>>>> </page 275>
>>>>>
>>>>> <page 248> Liar Paradox
>>>>>     Should we succeed in constructing in the metalanguage
>>>>>     a correct definition of truth, then
>>>>>
>>>>>     It would
>>>>>     then be possible to reconstruct the antinomy of the liar in the
>>>>>     metalanguage, by forming in the language itself a sentence x
>>>>>     such that the sentence of the metalanguage which is correlated
>>>>>     with x asserts that x is not a true sentence.
>>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>>> </page 248>
>>>>>
>>>>> Many people today are simply too stupid to understand
>>>>> that the Liar Paradox is simply not a truth bearer
>>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>>
>>>>> When Tarski assumes the Liar Paradox as a premise
>>>>> this must be rejected and over-ruled.
>>>>
>>>> Where does he assume it as a premise?
>>>>
>>>
>>> His line (1) is a premise.
>>
>> Then why does he say, "In other words, we can construct ... " just
>> above it.
>>
>> (1) is a CONCLUSION from the previous paragraph.
>>
>> you clearly don't know much about logic.
>>
>>>
>>>>>
>>>>> (1) x ∉ Provable if and only if p
>>>>> must be corrected to say
>>>>> (1) x ∈ Provable if and only if p
>>>>>
>>>>
>>>> What was actually wrong with (1). You haven't shown the error in logic.
>>>
>>> His line (1) <is> an adapted form of the actual Liar
>>> Paradox as I have shown by the quotes above.
>>
>> NO, the liar paradox says NOTHING about "Provable".
>
> Tarski says that he takes the Liar Paradox:
> x ∉ True if and only if p
> and changes it to this
> (1) x ∉ Provable if and only if p
> on page <275> quoted above.
>
> It is <page 248> quoted above where he says
> that he is using the actual Liar Paradox.
>
> You have to carefully study what I say before
> providing a rebuttal. It took me a half hour
> to compose the Tarski quotes.
>
>

On 1/22/24 1:39 PM, olcott wrote:
> On 1/22/2024 4:17 AM, Mikko wrote:
>> On 2024-01-22 02:18:35 +0000, olcott said:
>>
>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>> On 1/22/24 02:43, olcott wrote:
>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>
>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>> pathologically self-referential, making his argument invalid?
>>>>>>>>>>>>
>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>
>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>
>>>>>>>>
>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects ALL
>>>>>>>> cycles, even if they don't cause logical issues (as I understand
>>>>>>>> it)
>>>>>>>
>>>>>>> As you fail to understand it.
>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>> automatically generated the directed graph of the
>>>>>>> evaluation sequence of any of its expressions.
>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>
>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>
>>>>>>
>>>>>> You are rebutting the infinite formulas such as
>>>>>> ¬True(¬True(¬True(...)))
>>>>>>
>>>>>> But this is already in the standard theory. Infinite formulas such
>>>>>> as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>
>>>>>> Olcott doesn't understand that diagonalization is not the same as
>>>>>> infinite recursion.
>>>>>
>>>>> Finally a reply that is not nonsense.
>>>>> Diagonalization only knows that for some reason or another
>>>>> x is unprovable in L.
>>>>
>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>> unprovable. There are different ways to find out that it's
>>>> unprovable, or different ways to understand that it's unprovable,
>>>> but not reasons why it's unprovable.
>>>
>>> If the reason that x is unprovable in L is that x
>>> is semantically incorrect in L then instead of saying
>>> that x is undecidable in L the decider rejects x
>>> as invalid input.
>>>
>>> This what Tarski should have done.
>>
>> In a formal theory nothing is semantically anything.
>
> That it the reason why formal theories get confused
> and make semantic errors that are invisible to them.

While you try to use natural language and claim things that are
impossible must be, becuase you don't understand logic.

>
>> The semantics only
>> enter when the theory is interpreted. In a first order theory if x is
>> undecidable then it is true in some models and false in all others.
>> If neither x nor ¬x is provable you can add either one (but not both)
>> to the axioms of the theory and get another theory where x is decidable.
>>
>> Mikko
>>
>

On 1/22/2024 9:43 PM, Richard Damon wrote:
> On 1/22/24 1:59 PM, olcott wrote:
>> On 1/22/2024 6:23 AM, Richard Damon wrote:
>>> On 1/21/24 11:37 PM, olcott wrote:
>>>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>>>> On 1/21/24 11:01 PM, olcott wrote:
>>>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making
>>>>>>>>>>>>>>>>>>>>>>> his argument invalid?
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other
>>>>>>>>>>>>>>>>>>>> systems
>>>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already
>>>>>>>>>>>>>>>>> not valid.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not
>>>>>>>>>>>>>>>>> the same as infinite recursion.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>>>>> it's unprovable. There are different ways to find out
>>>>>>>>>>>>>>> that it's unprovable, or different ways to understand
>>>>>>>>>>>>>>> that it's unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> But there are x that are unprovable in L because the chain
>>>>>>>>>>>>> to them is infinitely long, which makes them true but
>>>>>>>>>>>>> unprovale.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>>>
>>>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> WHy is it "erroneous", it is a simple statement previously
>>>>>>>>>>> proven.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> He proved that there are some things that we know
>>>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>>>> they are true?
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> No, he proved that there are some things that ARE true that we
>>>>>>>>> can not prove to be true.
>>>>>>>>>
>>>>>>>>
>>>>>>>> How the Hell is he going to do that on his basis
>>>>>>>> of the Liar Paradox?
>>>>>>>>
>>>>>>>
>>>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>>>
>>>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>>>> He get his line (1) directly from the Liar Paradox
>>>>>>
>>>>>> Below he shows how he transforms the Liar Paradox
>>>>>> x ∉ True if and only if p
>>>>>>
>>>>>> into his line (1) by replacing "Tr" (for True)
>>>>>> with 'Pr" (for provable) Here is his line
>>>>>> (1) x ∉ Provable if and only if p
>>>>>>
>>>>>> <page 275>
>>>>>>     In accordance with the first
>>>>>>     part of Th. I we can obtain the negation of one of the sentences
>>>>>>     in condition (α) of convention T of § 3 as a consequence of the
>>>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in this
>>>>>>     convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
>>>>>> </page 275>
>>>>>>
>>>>>> <page 248> Liar Paradox
>>>>>>     Should we succeed in constructing in the metalanguage
>>>>>>     a correct definition of truth, then
>>>>>>
>>>>>>     It would
>>>>>>     then be possible to reconstruct the antinomy of the liar in the
>>>>>>     metalanguage, by forming in the language itself a sentence x
>>>>>>     such that the sentence of the metalanguage which is correlated
>>>>>>     with x asserts that x is not a true sentence.
>>>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>>>> </page 248>
>>>>>>
>>>>>> Many people today are simply too stupid to understand
>>>>>> that the Liar Paradox is simply not a truth bearer
>>>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>>>
>>>>>> When Tarski assumes the Liar Paradox as a premise
>>>>>> this must be rejected and over-ruled.
>>>>>
>>>>> Where does he assume it as a premise?
>>>>>
>>>>
>>>> His line (1) is a premise.
>>>
>>> Then why does he say, "In other words, we can construct ... " just
>>> above it.
>>>
>>> (1) is a CONCLUSION from the previous paragraph.
>>>
>>> you clearly don't know much about logic.
>>>
>>>>
>>>>>>
>>>>>> (1) x ∉ Provable if and only if p
>>>>>> must be corrected to say
>>>>>> (1) x ∈ Provable if and only if p
>>>>>>
>>>>>
>>>>> What was actually wrong with (1). You haven't shown the error in
>>>>> logic.
>>>>
>>>> His line (1) <is> an adapted form of the actual Liar
>>>> Paradox as I have shown by the quotes above.
>>>
>>> NO, the liar paradox says NOTHING about "Provable".
>>
>> Tarski says that he takes the Liar Paradox:
>> x ∉ True if and only if p
>> and changes it to this
>> (1) x ∉ Provable if and only if p
>> on page <275> quoted above.
>>
>> It is <page 248> quoted above where he says
>> that he is using the actual Liar Paradox.
>>
>> You have to carefully study what I say before
>> providing a rebuttal. It took me a half hour
>> to compose the Tarski quotes.
>>
>>
>
> Note, page 247 doesn't say "start with the Liar's Paradox" he points out
> that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that the
Carefully study every single word of my quotes from
<page 248> and <page 275> again and again until you
see that what I say is true.

On 1/22/24 10:53 PM, olcott wrote:
> On 1/22/2024 9:43 PM, Richard Damon wrote:
>> On 1/22/24 1:59 PM, olcott wrote:
>>> On 1/22/2024 6:23 AM, Richard Damon wrote:
>>>> On 1/21/24 11:37 PM, olcott wrote:
>>>>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>>>>> On 1/21/24 11:01 PM, olcott wrote:
>>>>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't
>>>>>>>>>>>>>>>>>>>>>>>> Cantor's number pathologically self-referential,
>>>>>>>>>>>>>>>>>>>>>>>> making his argument invalid?
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other
>>>>>>>>>>>>>>>>>>>>> systems
>>>>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical
>>>>>>>>>>>>>>>>>>>> issues (as I understand it)
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already
>>>>>>>>>>>>>>>>>> not valid.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not
>>>>>>>>>>>>>>>>>> the same as infinite recursion.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact that
>>>>>>>>>>>>>>>> it's unprovable. There are different ways to find out
>>>>>>>>>>>>>>>> that it's unprovable, or different ways to understand
>>>>>>>>>>>>>>>> that it's unprovable, but not reasons why it's unprovable.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> But there are x that are unprovable in L because the chain
>>>>>>>>>>>>>> to them is infinitely long, which makes them true but
>>>>>>>>>>>>>> unprovale.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>>>>
>>>>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> WHy is it "erroneous", it is a simple statement previously
>>>>>>>>>>>> proven.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> He proved that there are some things that we know
>>>>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>>>>> they are true?
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> No, he proved that there are some things that ARE true that we
>>>>>>>>>> can not prove to be true.
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> How the Hell is he going to do that on his basis
>>>>>>>>> of the Liar Paradox?
>>>>>>>>>
>>>>>>>>
>>>>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>>>>
>>>>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>>>>> He get his line (1) directly from the Liar Paradox
>>>>>>>
>>>>>>> Below he shows how he transforms the Liar Paradox
>>>>>>> x ∉ True if and only if p
>>>>>>>
>>>>>>> into his line (1) by replacing "Tr" (for True)
>>>>>>> with 'Pr" (for provable) Here is his line
>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>
>>>>>>> <page 275>
>>>>>>>     In accordance with the first
>>>>>>>     part of Th. I we can obtain the negation of one of the sentences
>>>>>>>     in condition (α) of convention T of § 3 as a consequence of the
>>>>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in this
>>>>>>>     convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
>>>>>>> </page 275>
>>>>>>>
>>>>>>> <page 248> Liar Paradox
>>>>>>>     Should we succeed in constructing in the metalanguage
>>>>>>>     a correct definition of truth, then
>>>>>>>
>>>>>>>     It would
>>>>>>>     then be possible to reconstruct the antinomy of the liar in the
>>>>>>>     metalanguage, by forming in the language itself a sentence x
>>>>>>>     such that the sentence of the metalanguage which is correlated
>>>>>>>     with x asserts that x is not a true sentence.
>>>>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>>>>> </page 248>
>>>>>>>
>>>>>>> Many people today are simply too stupid to understand
>>>>>>> that the Liar Paradox is simply not a truth bearer
>>>>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>>>>
>>>>>>> When Tarski assumes the Liar Paradox as a premise
>>>>>>> this must be rejected and over-ruled.
>>>>>>
>>>>>> Where does he assume it as a premise?
>>>>>>
>>>>>
>>>>> His line (1) is a premise.
>>>>
>>>> Then why does he say, "In other words, we can construct ... " just
>>>> above it.
>>>>
>>>> (1) is a CONCLUSION from the previous paragraph.
>>>>
>>>> you clearly don't know much about logic.
>>>>
>>>>>
>>>>>>>
>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>> must be corrected to say
>>>>>>> (1) x ∈ Provable if and only if p
>>>>>>>
>>>>>>
>>>>>> What was actually wrong with (1). You haven't shown the error in
>>>>>> logic.
>>>>>
>>>>> His line (1) <is> an adapted form of the actual Liar
>>>>> Paradox as I have shown by the quotes above.
>>>>
>>>> NO, the liar paradox says NOTHING about "Provable".
>>>
>>> Tarski says that he takes the Liar Paradox:
>>> x ∉ True if and only if p
>>> and changes it to this
>>> (1) x ∉ Provable if and only if p
>>> on page <275> quoted above.
>>>
>>> It is <page 248> quoted above where he says
>>> that he is using the actual Liar Paradox.
>>>
>>> You have to carefully study what I say before
>>> providing a rebuttal. It took me a half hour
>>> to compose the Tarski quotes.
>>>
>>>
>>
>> Note, page 247 doesn't say "start with the Liar's Paradox" he points
>> out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that the
> Carefully study every single word of my quotes from
> <page 248> and <page 275> again and again until you
> see that what I say is true.
>
> I had to study these four pages hundreds and hundreds
> of times before I could see that his line (1) was
> adapted from:
> *x ∉ True if and only if p*
> which <is> his version of the Liar Paradox.
>

On 1/22/2024 10:22 PM, Richard Damon wrote:
> On 1/22/24 10:53 PM, olcott wrote:
>> On 1/22/2024 9:43 PM, Richard Damon wrote:
>>> On 1/22/24 1:59 PM, olcott wrote:
>>>> On 1/22/2024 6:23 AM, Richard Damon wrote:
>>>>> On 1/21/24 11:37 PM, olcott wrote:
>>>>>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>>>>>> On 1/21/24 11:01 PM, olcott wrote:
>>>>>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know
>>>>>>>>>>>>>>>>>>>>>>>>>> that
>>>>>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore
>>>>>>>>>>>>>>>>>>>>>>>>>> the
>>>>>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't
>>>>>>>>>>>>>>>>>>>>>>>>> Cantor's number pathologically
>>>>>>>>>>>>>>>>>>>>>>>>> self-referential, making his argument invalid?
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other
>>>>>>>>>>>>>>>>>>>>>> systems
>>>>>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It
>>>>>>>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause
>>>>>>>>>>>>>>>>>>>>> logical issues (as I understand it)
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already
>>>>>>>>>>>>>>>>>>> not valid.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is not
>>>>>>>>>>>>>>>>>>> the same as infinite recursion.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>>>>>> Diagonalization only knows that for some reason or
>>>>>>>>>>>>>>>>>> another
>>>>>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact
>>>>>>>>>>>>>>>>> that it's unprovable. There are different ways to find
>>>>>>>>>>>>>>>>> out that it's unprovable, or different ways to
>>>>>>>>>>>>>>>>> understand that it's unprovable, but not reasons why
>>>>>>>>>>>>>>>>> it's unprovable.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> But there are x that are unprovable in L because the
>>>>>>>>>>>>>>> chain to them is infinitely long, which makes them true
>>>>>>>>>>>>>>> but unprovale.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> WHy is it "erroneous", it is a simple statement previously
>>>>>>>>>>>>> proven.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> He proved that there are some things that we know
>>>>>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>>>>>> they are true?
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> No, he proved that there are some things that ARE true that
>>>>>>>>>>> we can not prove to be true.
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> How the Hell is he going to do that on his basis
>>>>>>>>>> of the Liar Paradox?
>>>>>>>>>>
>>>>>>>>>
>>>>>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>>>>>
>>>>>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>>>>>> He get his line (1) directly from the Liar Paradox
>>>>>>>>
>>>>>>>> Below he shows how he transforms the Liar Paradox
>>>>>>>> x ∉ True if and only if p
>>>>>>>>
>>>>>>>> into his line (1) by replacing "Tr" (for True)
>>>>>>>> with 'Pr" (for provable) Here is his line
>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>
>>>>>>>> <page 275>
>>>>>>>>     In accordance with the first
>>>>>>>>     part of Th. I we can obtain the negation of one of the
>>>>>>>> sentences
>>>>>>>>     in condition (α) of convention T of § 3 as a consequence of the
>>>>>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in this
>>>>>>>>     convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
>>>>>>>> </page 275>
>>>>>>>>
>>>>>>>> <page 248> Liar Paradox
>>>>>>>>     Should we succeed in constructing in the metalanguage
>>>>>>>>     a correct definition of truth, then
>>>>>>>>
>>>>>>>>     It would
>>>>>>>>     then be possible to reconstruct the antinomy of the liar in the
>>>>>>>>     metalanguage, by forming in the language itself a sentence x
>>>>>>>>     such that the sentence of the metalanguage which is correlated
>>>>>>>>     with x asserts that x is not a true sentence.
>>>>>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>>>>>> </page 248>
>>>>>>>>
>>>>>>>> Many people today are simply too stupid to understand
>>>>>>>> that the Liar Paradox is simply not a truth bearer
>>>>>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>>>>>
>>>>>>>> When Tarski assumes the Liar Paradox as a premise
>>>>>>>> this must be rejected and over-ruled.
>>>>>>>
>>>>>>> Where does he assume it as a premise?
>>>>>>>
>>>>>>
>>>>>> His line (1) is a premise.
>>>>>
>>>>> Then why does he say, "In other words, we can construct ... " just
>>>>> above it.
>>>>>
>>>>> (1) is a CONCLUSION from the previous paragraph.
>>>>>
>>>>> you clearly don't know much about logic.
>>>>>
>>>>>>
>>>>>>>>
>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>> must be corrected to say
>>>>>>>> (1) x ∈ Provable if and only if p
>>>>>>>>
>>>>>>>
>>>>>>> What was actually wrong with (1). You haven't shown the error in
>>>>>>> logic.
>>>>>>
>>>>>> His line (1) <is> an adapted form of the actual Liar
>>>>>> Paradox as I have shown by the quotes above.
>>>>>
>>>>> NO, the liar paradox says NOTHING about "Provable".
>>>>
>>>> Tarski says that he takes the Liar Paradox:
>>>> x ∉ True if and only if p
>>>> and changes it to this
>>>> (1) x ∉ Provable if and only if p
>>>> on page <275> quoted above.
>>>>
>>>> It is <page 248> quoted above where he says
>>>> that he is using the actual Liar Paradox.
>>>>
>>>> You have to carefully study what I say before
>>>> providing a rebuttal. It took me a half hour
>>>> to compose the Tarski quotes.
>>>>
>>>>
>>>
>>> Note, page 247 doesn't say "start with the Liar's Paradox" he points
>>> out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that the
>> Carefully study every single word of my quotes from
>> <page 248> and <page 275> again and again until you
>> see that what I say is true.
>>
>> I had to study these four pages hundreds and hundreds
>> of times before I could see that his line (1) was
>> adapted from:
>> *x ∉ True if and only if p*
>> which <is> his version of the Liar Paradox.
>>
>
> Nope, He doesn't "ASSUME" the Liar has a true value, he shows that given
> a construction of the procedure that answers if any statement is True,
> we can show that there exist a statment, with a truth value, that turns
> out to be the Liar.

On 1/22/24 11:30 PM, olcott wrote:
> On 1/22/2024 10:22 PM, Richard Damon wrote:
>> On 1/22/24 10:53 PM, olcott wrote:
>>> On 1/22/2024 9:43 PM, Richard Damon wrote:
>>>> On 1/22/24 1:59 PM, olcott wrote:
>>>>> On 1/22/2024 6:23 AM, Richard Damon wrote:
>>>>>> On 1/21/24 11:37 PM, olcott wrote:
>>>>>>> On 1/21/2024 10:06 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 11:01 PM, olcott wrote:
>>>>>>>>> On 1/21/2024 9:39 PM, Richard Damon wrote:
>>>>>>>>>> On 1/21/24 10:30 PM, olcott wrote:
>>>>>>>>>>> On 1/21/2024 9:28 PM, Richard Damon wrote:
>>>>>>>>>>>> On 1/21/24 10:22 PM, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 9:19 PM, Richard Damon wrote:
>>>>>>>>>>>>>> On 1/21/24 9:55 PM, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 8:28 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>> On 1/21/24 9:18 PM, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know
>>>>>>>>>>>>>>>>>>>>>>>>>>> that
>>>>>>>>>>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to
>>>>>>>>>>>>>>>>>>>>>>>>>>> ignore the
>>>>>>>>>>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't
>>>>>>>>>>>>>>>>>>>>>>>>>> Cantor's number pathologically
>>>>>>>>>>>>>>>>>>>>>>>>>> self-referential, making his argument invalid?
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about
>>>>>>>>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
>>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>> That Prolog pays attention to details that other
>>>>>>>>>>>>>>>>>>>>>>> systems
>>>>>>>>>>>>>>>>>>>>>>> ignore make it wrong is like saying that
>>>>>>>>>>>>>>>>>>>>>>> ignorance is
>>>>>>>>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems.
>>>>>>>>>>>>>>>>>>>>>> It rejects ALL cycles, even if they don't cause
>>>>>>>>>>>>>>>>>>>>>> logical issues (as I understand it)
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> But this is already in the standard theory. Infinite
>>>>>>>>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are
>>>>>>>>>>>>>>>>>>>> already not valid.
>>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>>> Olcott doesn't understand that diagonalization is
>>>>>>>>>>>>>>>>>>>> not the same as infinite recursion.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>>>>>>>>>>> Diagonalization only knows that for some reason or
>>>>>>>>>>>>>>>>>>> another
>>>>>>>>>>>>>>>>>>> x is unprovable in L.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> I dispute the notion of "reasons". It's just a fact
>>>>>>>>>>>>>>>>>> that it's unprovable. There are different ways to find
>>>>>>>>>>>>>>>>>> out that it's unprovable, or different ways to
>>>>>>>>>>>>>>>>>> understand that it's unprovable, but not reasons why
>>>>>>>>>>>>>>>>>> it's unprovable.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>>>>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>>>>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>>>>>>>>>>> as invalid input.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> This what Tarski should have done.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> But there are x that are unprovable in L because the
>>>>>>>>>>>>>>>> chain to them is infinitely long, which makes them true
>>>>>>>>>>>>>>>> but unprovale.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>>>>>>> (2) x ∈ True if and only if p
>>>>>>>>>>>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> When we correct the erroneous line (1) then line (3) becomes
>>>>>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>>>>>>>>>>> Thus making your (infinite chain) x simply untrue.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> WHy is it "erroneous", it is a simple statement previously
>>>>>>>>>>>>>> proven.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> He proved that there are some things that we know
>>>>>>>>>>>>> are true yet have no way what-so-ever to know that
>>>>>>>>>>>>> they are true?
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> No, he proved that there are some things that ARE true that
>>>>>>>>>>>> we can not prove to be true.
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> How the Hell is he going to do that on his basis
>>>>>>>>>>> of the Liar Paradox?
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> Read his proof. And it isn't "based' on the Liar's paradox,
>>>>>>>>>
>>>>>>>>> *It sure as Hell is anchored in the Liar Paradox*
>>>>>>>>> He get his line (1) directly from the Liar Paradox
>>>>>>>>>
>>>>>>>>> Below he shows how he transforms the Liar Paradox
>>>>>>>>> x ∉ True if and only if p
>>>>>>>>>
>>>>>>>>> into his line (1) by replacing "Tr" (for True)
>>>>>>>>> with 'Pr" (for provable) Here is his line
>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>>
>>>>>>>>> <page 275>
>>>>>>>>>     In accordance with the first
>>>>>>>>>     part of Th. I we can obtain the negation of one of the
>>>>>>>>> sentences
>>>>>>>>>     in condition (α) of convention T of § 3 as a consequence of
>>>>>>>>> the
>>>>>>>>>     definition of the symbol 'Pr' (provided we replace 'Tr' in
>>>>>>>>> this
>>>>>>>>>     convention by 'Pr').
>>>>>>>>> https://liarparadox.org/Tarski_275_276.pdf
>>>>>>>>> </page 275>
>>>>>>>>>
>>>>>>>>> <page 248> Liar Paradox
>>>>>>>>>     Should we succeed in constructing in the metalanguage
>>>>>>>>>     a correct definition of truth, then
>>>>>>>>>
>>>>>>>>>     It would
>>>>>>>>>     then be possible to reconstruct the antinomy of the liar in
>>>>>>>>> the
>>>>>>>>>     metalanguage, by forming in the language itself a sentence x
>>>>>>>>>     such that the sentence of the metalanguage which is correlated
>>>>>>>>>     with x asserts that x is not a true sentence.
>>>>>>>>>     https://liarparadox.org/Tarski_247_248.pdf
>>>>>>>>> </page 248>
>>>>>>>>>
>>>>>>>>> Many people today are simply too stupid to understand
>>>>>>>>> that the Liar Paradox is simply not a truth bearer
>>>>>>>>> thus must be rejected by any correct True(L, x) predicate.
>>>>>>>>>
>>>>>>>>> When Tarski assumes the Liar Paradox as a premise
>>>>>>>>> this must be rejected and over-ruled.
>>>>>>>>
>>>>>>>> Where does he assume it as a premise?
>>>>>>>>
>>>>>>>
>>>>>>> His line (1) is a premise.
>>>>>>
>>>>>> Then why does he say, "In other words, we can construct ... " just
>>>>>> above it.
>>>>>>
>>>>>> (1) is a CONCLUSION from the previous paragraph.
>>>>>>
>>>>>> you clearly don't know much about logic.
>>>>>>
>>>>>>>
>>>>>>>>>
>>>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>>>> must be corrected to say
>>>>>>>>> (1) x ∈ Provable if and only if p
>>>>>>>>>
>>>>>>>>
>>>>>>>> What was actually wrong with (1). You haven't shown the error in
>>>>>>>> logic.
>>>>>>>
>>>>>>> His line (1) <is> an adapted form of the actual Liar
>>>>>>> Paradox as I have shown by the quotes above.
>>>>>>
>>>>>> NO, the liar paradox says NOTHING about "Provable".
>>>>>
>>>>> Tarski says that he takes the Liar Paradox:
>>>>> x ∉ True if and only if p
>>>>> and changes it to this
>>>>> (1) x ∉ Provable if and only if p
>>>>> on page <275> quoted above.
>>>>>
>>>>> It is <page 248> quoted above where he says
>>>>> that he is using the actual Liar Paradox.
>>>>>
>>>>> You have to carefully study what I say before
>>>>> providing a rebuttal. It took me a half hour
>>>>> to compose the Tarski quotes.
>>>>>
>>>>>
>>>>
>>>> Note, page 247 doesn't say "start with the Liar's Paradox" he points
>>>> out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that
>>>> the
>>> Carefully study every single word of my quotes from
>>> <page 248> and <page 275> again and again until you
>>> see that what I say is true.
>>>
>>> I had to study these four pages hundreds and hundreds
>>> of times before I could see that his line (1) was
>>> adapted from:
>>> *x ∉ True if and only if p*
>>> which <is> his version of the Liar Paradox.
>>>
>>
>> Nope, He doesn't "ASSUME" the Liar has a true value, he shows that
>> given a construction of the procedure that answers if any statement is
>> True, we can show that there exist a statment, with a truth value,
>> that turns out to be the Liar.
>
> In other words you believe that the Liar Paradox has a truth value?
>

On 1/23/24 05:30, olcott wrote:
> In other words you believe that the Liar Paradox has a truth value?

If YOU believe that True(L,x) exists then YOU believe the Liar Paradox
has a truth value.

On 1/23/24 01:31, olcott wrote:
> On 1/22/2024 6:10 PM, immibis wrote:
>> On 1/23/24 00:31, olcott wrote:
>>> On 1/22/2024 5:20 PM, immibis wrote:
>>>>
>>>> I don't think you get this. Every system has a G that can't be
>>>> proved in that system,
>>>
>>> Yet can be proved in metamathematics.
>>>
>> Is metamathematics a system?
>
> Yes

Then it has a G that can't be proven OR it allows false things to be proven.

On 1/23/2024 3:23 AM, Mikko wrote:
> On 2024-01-22 18:39:44 +0000, olcott said:
>
>> On 1/22/2024 4:17 AM, Mikko wrote:
>
>>> In a formal theory nothing is semantically anything.
>
>> That it the reason why formal theories get confused
>> and make semantic errors that are invisible to them.
>
> As there are no semantics in a formal system there can
> be no semantic errors. However, it is possible that the
> intended interpretation is not a model of the system.
> Then one may hope that a small change will make it useful
> for its intended purpose.
>
> Mikko
>

True is an inherently semantic concept, thus logic systems
always have semantics. The truth tables for propositional
logic provide the semantics of its operators.

The Tarski undefinability theorem is totally refuted by
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)

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

On 1/23/2024 3:27 AM, Mikko wrote:
> On 2024-01-22 19:16:49 +0000, immibis said:
>
>> On 1/22/24 20:08, olcott wrote:
>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>> On 1/22/24 19:39, olcott wrote:
>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>
>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's number
>>>>>>>>>>>>>>>> pathologically self-referential, making his argument
>>>>>>>>>>>>>>>> invalid?
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>
>>>>>>>>>>>>
>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>>>> understand it)
>>>>>>>>>>>
>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>
>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>
>>>>>>>>>>
>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>
>>>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>>>
>>>>>>>>>> Olcott doesn't understand that diagonalization is not the same
>>>>>>>>>> as infinite recursion.
>>>>>>>>>
>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>> x is unprovable in L.
>>>>>>>>
>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>
>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>> as invalid input.
>>>>>>>
>>>>>>> This what Tarski should have done.
>>>>>>
>>>>>> In a formal theory nothing is semantically anything.
>>>>>
>>>>> That it the reason why formal theories get confused
>>>>> and make semantic errors that are invisible to them.
>>>>
>>>> Nobody is talking about semantics except for you.
>>> *That is their mistake*
>>>
>>>> What is the formal truth value of x?
>>>
>>> Something that seems over your head is the self-contradictory
>>> sentences cannot possibly have a truth value.
>>>
>>>
>> Every logical formula has a truth value.
>
> In a particular interpretation. In another interpretation it
> may have a different interpretation. For example,
>
> ∀x ∀y (xy = yx)
>
> is true about real numbers but not about quaternions.
>
> Mikko
>
>

Tarski's Liar Paradox has no truth value.
(1) x ∉ True if and only if p
--
Copyright 2023 Olcott "Talent hits a target no one else can hit; Genius
hits a target no one else can see." Arthur Schopenhauer

On 1/23/24 16:17, olcott wrote:
> On 1/23/2024 3:27 AM, Mikko wrote:
>> On 2024-01-22 19:16:49 +0000, immibis said:
>>
>>> On 1/22/24 20:08, olcott wrote:
>>>> On 1/22/2024 1:00 PM, immibis wrote:
>>>>> On 1/22/24 19:39, olcott wrote:
>>>>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>>>>>> On 2024-01-22 02:18:35 +0000, olcott said:
>>>>>>>
>>>>>>>> On 1/21/2024 8:07 PM, immibis wrote:
>>>>>>>>> On 1/22/24 02:43, olcott wrote:
>>>>>>>>>> On 1/21/2024 7:38 PM, immibis wrote:
>>>>>>>>>>> On 1/22/24 02:04, olcott wrote:
>>>>>>>>>>>> On 1/21/2024 6:58 PM, Richard Damon wrote:
>>>>>>>>>>>>> On 1/21/24 7:54 PM, olcott wrote:
>>>>>>>>>>>>>> On 1/21/2024 6:50 PM, immibis wrote:
>>>>>>>>>>>>>>> On 1/22/24 01:37, olcott wrote:
>>>>>>>>>>>>>>>> On 1/21/2024 6:27 PM, immibis wrote:
>>>>>>>>>>>>>>>>> On 1/22/24 01:13, olcott wrote:
>>>>>>>>>>>>>>>>>> On 1/21/2024 6:04 PM, immibis wrote:
>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
>>>>>>>>>>>>>>>>>>>> Tarski didn't understand that the correct
>>>>>>>>>>>>>>>>>>>> evaluation of the Liar Paradox requires
>>>>>>>>>>>>>>>>>>>> an infinite cycle in the directed graph
>>>>>>>>>>>>>>>>>>>> of its evaluation sequence.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> You don't understand the difference between
>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion.
>>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>>> Do you think the real numbers are countable?
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> Diagonalization is a process by which we know that
>>>>>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the
>>>>>>>>>>>>>>>>>> reason why x is unprovable in L.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> So are the real numbers countable? Isn't Cantor's
>>>>>>>>>>>>>>>>> number pathologically self-referential, making his
>>>>>>>>>>>>>>>>> argument invalid?
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>> unify_with_occurs_check(LP, not(true(LP))).
>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable
>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation
>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
>>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>> Provability doesn't give a flying fuck about evaluation
>>>>>>>>>>>>>>>>> cycles, whatever those are.
>>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>>> It sure does in Prolog.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>> Then Prolog is wrong.
>>>>>>>>>>>>>>>
>>>>>>>>>>>>>>
>>>>>>>>>>>>>> That Prolog pays attention to details that other systems
>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is
>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
>>>>>>>>>>>>>>
>>>>>>>>>>>>>
>>>>>>>>>>>>> Prolog handles SIMPLE logic system and problems. It rejects
>>>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
>>>>>>>>>>>>> understand it)
>>>>>>>>>>>>
>>>>>>>>>>>> As you fail to understand it.
>>>>>>>>>>>> I took 18 months creating Minimal Type Theory that
>>>>>>>>>>>> automatically generated the directed graph of the
>>>>>>>>>>>> evaluation sequence of any of its expressions.
>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive
>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
>>>>>>>>>>>>
>>>>>>>>>>>> https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
>>>>>>>>>>>>
>>>>>>>>>>>
>>>>>>>>>>> You are rebutting the infinite formulas such as
>>>>>>>>>>> ¬True(¬True(¬True(...)))
>>>>>>>>>>>
>>>>>>>>>>> But this is already in the standard theory. Infinite formulas
>>>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid.
>>>>>>>>>>>
>>>>>>>>>>> Olcott doesn't understand that diagonalization is not the
>>>>>>>>>>> same as infinite recursion.
>>>>>>>>>>
>>>>>>>>>> Finally a reply that is not nonsense.
>>>>>>>>>> Diagonalization only knows that for some reason or another
>>>>>>>>>> x is unprovable in L.
>>>>>>>>>
>>>>>>>>> I dispute the notion of "reasons". It's just a fact that it's
>>>>>>>>> unprovable. There are different ways to find out that it's
>>>>>>>>> unprovable, or different ways to understand that it's
>>>>>>>>> unprovable, but not reasons why it's unprovable.
>>>>>>>>
>>>>>>>> If the reason that x is unprovable in L is that x
>>>>>>>> is semantically incorrect in L then instead of saying
>>>>>>>> that x is undecidable in L the decider rejects x
>>>>>>>> as invalid input.
>>>>>>>>
>>>>>>>> This what Tarski should have done.
>>>>>>>
>>>>>>> In a formal theory nothing is semantically anything.
>>>>>>
>>>>>> That it the reason why formal theories get confused
>>>>>> and make semantic errors that are invisible to them.
>>>>>
>>>>> Nobody is talking about semantics except for you.
>>>> *That is their mistake*
>>>>
>>>>> What is the formal truth value of x?
>>>>
>>>> Something that seems over your head is the self-contradictory
>>>> sentences cannot possibly have a truth value.
>>>>
>>>>
>>> Every logical formula has a truth value.
>>
>> In a particular interpretation. In another interpretation it
>> may have a different interpretation. For example,
>>
>> ∀x ∀y (xy = yx)
>>
>> is true about real numbers but not about quaternions.
>>
>> Mikko
>>
>>
>
> Tarski's Liar Paradox has no truth value.
> (1) x ∉ True if and only if p

On 1/23/24 16:14, olcott wrote:
> On 1/23/2024 3:23 AM, Mikko wrote:
>> On 2024-01-22 18:39:44 +0000, olcott said:
>>
>>> On 1/22/2024 4:17 AM, Mikko wrote:
>>
>>>> In a formal theory nothing is semantically anything.
>>
>>> That it the reason why formal theories get confused
>>> and make semantic errors that are invisible to them.
>>
>> As there are no semantics in a formal system there can
>> be no semantic errors. However, it is possible that the
>> intended interpretation is not a model of the system.
>> Then one may hope that a small change will make it useful
>> for its intended purpose.
>>
>> Mikko
>>
>
> True is an inherently semantic concept, thus logic systems
> always have semantics. The truth tables for propositional
> logic provide the semantics of its operators.
>
> The Tarski undefinability theorem is totally refuted by
> True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
>

In which system is ⊢ a logical connective?