On 1/21/24 7:55 PM, olcott wrote:
> On 1/21/2024 6:52 PM, Richard Damon wrote:
>> On 1/21/24 7:34 PM, olcott wrote:
>>> On 1/21/2024 6:26 PM, immibis wrote:
>>>> On 1/22/24 01:21, olcott wrote:
>>>>> Not at all. After 10,000 hours of careful thought over many years
>>>>> I have determined this: ∀x ∈ L (True(L,x) ≡ (L ⊢ x) > is the
>>>>> correct way to encode a consistent and correct Truth(L,x)
>>>>> predicate. It even works correctly with natural language
>>>>> that has been formalized with something like Montague Grammar.
>>>>
>>>> Tarski proved that if you put ⊢ in your logic system, then your
>>>> logic system is inconsistent and wrong.
>>>>
>>>
>>> When we replace his line
>>> (3) x ∉ Provable if and only if x ∈ True.
>>> with this
>>> (3) x ∈ Provable if and only if x ∈ True.
>>>
>>> Then Tarski gets the True(L, x) predicate that he falsely
>>> assumed was impossible.
>>>
>>
>> No, we get a contradiction, since from (1) and (2) we get
>
> We get rid of (1) and (2) and begin with
> (3) x ∈ Provable if and only if x ∈ True.
>

You CAN'T get rid of (1) and (2) or even (3).

You can make your own (PO-3), but it would be in contradiction to (3).

Remember True statements remain True in the system no matter what else
you add to it, as they are anchored in the chain of proven linkages to
the basic Truth Makers, and you can not delete a basic Truth Maker.

You are just proving you totally don't understand how to do logic, and
are making an utter fool of yourself with you fumbling false statements.

On 1/21/24 8:19 PM, olcott wrote:
> On 1/21/2024 7:05 PM, immibis wrote:
>> On 1/22/24 01:55, olcott wrote:
>>> On 1/21/2024 6:52 PM, Richard Damon wrote:
>>>> On 1/21/24 7:34 PM, olcott wrote:
>>>>> On 1/21/2024 6:26 PM, immibis wrote:
>>>>>> On 1/22/24 01:21, olcott wrote:
>>>>>>> Not at all. After 10,000 hours of careful thought over many years
>>>>>>> I have determined this: ∀x ∈ L (True(L,x) ≡ (L ⊢ x) > is the
>>>>>>> correct way to encode a consistent and correct Truth(L,x)
>>>>>>> predicate. It even works correctly with natural language
>>>>>>> that has been formalized with something like Montague Grammar.
>>>>>>
>>>>>> Tarski proved that if you put ⊢ in your logic system, then your
>>>>>> logic system is inconsistent and wrong.
>>>>>>
>>>>>
>>>>> When we replace his line
>>>>> (3) x ∉ Provable if and only if x ∈ True.
>>>>> with this
>>>>> (3) x ∈ Provable if and only if x ∈ True.
>>>>>
>>>>> Then Tarski gets the True(L, x) predicate that he falsely
>>>>> assumed was impossible.
>>>>>
>>>>
>>>> No, we get a contradiction, since from (1) and (2) we get
>>>
>>> We get rid of (1) and (2) and begin with
>>> (3) x ∈ Provable if and only if x ∈ True.
>>>
>> Then you are defeating the whole point.
>>
>> That's like I have a proof
>
> A stipulative definition is a type of definition in which a new or
> currently existing term is given a new specific meaning for the purposes
> of argument or discussion in a given context. When the term already
> exists, this definition may, but does not necessarily, contradict the
> dictionary (lexical) definition of the term. Because of this, a
> stipulative definition cannot be "correct" or "incorrect"; it can only
> differ from other definitions, but it can be useful for its intended
> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>
> (1) x ∉ Provable if and only if p
> says that p is true if and only if we
> HAVE NO WAY to know that p is true.
>
> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>
> (1) x  Provable if and only if p
> says that p is true if and only if we
> HAVE A WAY to know that p is true.
>

Not allowed.

You can't "stipulate" statements away, only what you will use a word to
mean in your future part of the argument (and that disconnects the word
from things based on different meanings).

You are just proving you don't know what you are talking about.

On 1/21/24 8:18 PM, olcott wrote:
> On 1/21/2024 7:03 PM, Richard Damon wrote:
>> On 1/21/24 7:46 PM, olcott wrote:
>>> 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.
>>>
>>> Then Tarski gets the truth predicate that he falsely assumed was
>>> impossible.
>>>
>>  > You don't get to "erase" statements.
>
> A stipulative definition is a type of definition in which a new or
> currently existing term is given a new specific meaning for the purposes
> of argument or discussion in a given context. When the term already
> exists, this definition may, but does not necessarily, contradict the
> dictionary (lexical) definition of the term. Because of this, a
> stipulative definition cannot be "correct" or "incorrect"; it can only
> differ from other definitions, but it can be useful for its intended
> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>
> (1) x ∉ Provable if and only if p
> says that p is true if and only if we
> HAVE NO WAY to know that p is true.
>
> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
NOT ALLOWED.

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.

>
> MTT and Prolog show you that the reason is that the
> directed graph of the evaluation sequence has an
> infinite cycle.
>
> This sentence is not true.
> not true about what?
> not true about being not true.
> not true about being not true about what?
> not true about being not true about being not true...
>

That doesn't prove unprovability. It just proves that PROLOG can't prove
it. There are no evaluation cycles in the logic, only in YOUR MIND and
in PROLOG.

x = x + 1 - 1
What number is x?
x + 1 - 1. What number is x?
x + 1 - 1 + 1 - 1. What number is x?
x + 1 - 1 + 1 - 1 + 1 - 1. What number is x?
x + 1 - 1 + 1 - 1 + 1 - 1 + 1 - 1. What number is x?

(Actually, x is 42.)

What colour is grass? Green.
What colour is green? The colour of grass.
What colour is grass? Green.
What colour is green? The colour of grass.
This does not prove anything.

On 1/21/24 8:33 PM, olcott wrote:
> On 1/21/2024 7:23 PM, Richard Damon wrote:
>> On 1/21/24 8:04 PM, 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
>>>
>>
>> Yes, I've looked at it, and it just shows that you don't understand
>> what HOL actually is.
>>
>
> Your ADD prevents you from paying close enough attention.
> You most often provide a rebuttal to something that I never said.

Really, like the statement

All P(S1)

where P is a formulla

is a first order statement

It is still a qualifier over a relationship and thus a second order
statement, and not a first order statment which can only qualify over
the elments of reguard, the x that were put into S1.

Note that your first statement:

S1 := All x (Px or not Px)

isn't a valid statement as P is not defined. If you mena it creates some
substitution item that cn be put int

>
>> The differnce between First Order Logic and Higher Order Logic isn't
>> the "syntax", but the domain of the items the operator works over.
>
> The domain is all objects of thought as defined below:

In other words, you are breaking your system by having an uncountable
number of elements in its basic domain?

Most of the logic you are familiar with presumes that the domain of
reqard is countable, if not finite.

I suspect your "type theory" can not be expressed in the proper set
theory like ZFC.

>
> By the theory of simple types I mean the doctrine which says that the
> objects of thought ... are divided into types, namely: individuals,
> properties of individuals, relations between individuals, properties of
> such relations, etc. (with a similar hierarchy for extensions), and that
> sentences of the form: " a has the property φ ", " b bears the relation
> R to c ", etc. are meaningless, if a, b, c, R, φ are not of types
> fitting together. https://en.wikipedia.org/wiki/History_of_type_theory
>

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.

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

That doesn't mean it is semantically incorrect, but it is in fact
semantically correct.

You just don't understand what semantics mean in logic.

On 1/21/2024 8:04 PM, Richard Damon wrote:
> On 1/21/24 8:18 PM, olcott wrote:
>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>> On 1/21/24 7:46 PM, olcott wrote:
>>>> 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.
>>>>
>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>> impossible.
>>>>
>>>  > You don't get to "erase" statements.
>>
>> A stipulative definition is a type of definition in which a new or
>> currently existing term is given a new specific meaning for the purposes
>> of argument or discussion in a given context. When the term already
>> exists, this definition may, but does not necessarily, contradict the
>> dictionary (lexical) definition of the term. Because of this, a
>> stipulative definition cannot be "correct" or "incorrect"; it can only
>> differ from other definitions, but it can be useful for its intended
>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>
>> (1) x ∉ Provable if and only if p
>> says that p is true if and only if we
>> HAVE NO WAY to know that p is true.
>>
>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
> NOT ALLOWED.
>

On 1/22/24 03:36, olcott wrote:
> On 1/21/2024 8:04 PM, Richard Damon wrote:
>> On 1/21/24 8:18 PM, olcott wrote:
>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>> 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.
>>>>>
>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>> impossible.
>>>>>
>>>>  > You don't get to "erase" statements.
>>>
>>> A stipulative definition is a type of definition in which a new or
>>> currently existing term is given a new specific meaning for the purposes
>>> of argument or discussion in a given context. When the term already
>>> exists, this definition may, but does not necessarily, contradict the
>>> dictionary (lexical) definition of the term. Because of this, a
>>> stipulative definition cannot be "correct" or "incorrect"; it can only
>>> differ from other definitions, but it can be useful for its intended
>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>
>>> (1) x ∉ Provable if and only if p
>>> says that p is true if and only if we
>>> HAVE NO WAY to know that p is true.
>>>
>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>> NOT ALLOWED.
>>
>
> If a proof is trying to prove that cats are not dogs begins
> with the premise that cats are dogs the proof will fail.

On 1/22/24 03:18, olcott wrote:
> On 1/21/2024 8:07 PM, immibis wrote:
>> I dispute the notion of "reasons".
>
> If the reason

You weren't listening.

On 1/21/2024 8:39 PM, immibis wrote:
> On 1/22/24 03:36, olcott wrote:
>> On 1/21/2024 8:04 PM, Richard Damon wrote:
>>> On 1/21/24 8:18 PM, olcott wrote:
>>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>>> 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.
>>>>>>
>>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>>> impossible.
>>>>>>
>>>>>  > You don't get to "erase" statements.
>>>>
>>>> A stipulative definition is a type of definition in which a new or
>>>> currently existing term is given a new specific meaning for the
>>>> purposes
>>>> of argument or discussion in a given context. When the term already
>>>> exists, this definition may, but does not necessarily, contradict the
>>>> dictionary (lexical) definition of the term. Because of this, a
>>>> stipulative definition cannot be "correct" or "incorrect"; it can only
>>>> differ from other definitions, but it can be useful for its intended
>>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>>
>>>> (1) x ∉ Provable if and only if p
>>>> says that p is true if and only if we
>>>> HAVE NO WAY to know that p is true.
>>>>
>>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>>> NOT ALLOWED.
>>>
>>
>> If a proof is trying to prove that cats are not dogs begins
>> with the premise that cats are dogs the proof will fail.
>
> If cats are dogs, you can't prove that cats are not dogs.

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.

--
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/21/24 9:36 PM, olcott wrote:
> On 1/21/2024 8:04 PM, Richard Damon wrote:
>> On 1/21/24 8:18 PM, olcott wrote:
>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>> 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.
>>>>>
>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>> impossible.
>>>>>
>>>>  > You don't get to "erase" statements.
>>>
>>> A stipulative definition is a type of definition in which a new or
>>> currently existing term is given a new specific meaning for the purposes
>>> of argument or discussion in a given context. When the term already
>>> exists, this definition may, but does not necessarily, contradict the
>>> dictionary (lexical) definition of the term. Because of this, a
>>> stipulative definition cannot be "correct" or "incorrect"; it can only
>>> differ from other definitions, but it can be useful for its intended
>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>
>>> (1) x ∉ Provable if and only if p
>>> says that p is true if and only if we
>>> HAVE NO WAY to know that p is true.
>>>
>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>> NOT ALLOWED.
>>
>
> If a proof is trying to prove that cats are not dogs begins
> with the premise that cats are dogs the proof will fail.
> Tarski does this same thing with his line (1).

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.

Note, the statement is we can construct an x such that
x ∉ Provable if and only if p

You need to find the mistake in that proof to say they are not true.

You don't get to just say it is wrong, you need to PROVE it is wrong.

The fact that you don't understand it and don't agree with it does not
affect the fact that it is proven.

On 1/21/2024 9:14 PM, Richard Damon wrote:
> On 1/21/24 9:36 PM, olcott wrote:
>> On 1/21/2024 8:04 PM, Richard Damon wrote:
>>> On 1/21/24 8:18 PM, olcott wrote:
>>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>>> 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.
>>>>>>
>>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>>> impossible.
>>>>>>
>>>>>  > You don't get to "erase" statements.
>>>>
>>>> A stipulative definition is a type of definition in which a new or
>>>> currently existing term is given a new specific meaning for the
>>>> purposes
>>>> of argument or discussion in a given context. When the term already
>>>> exists, this definition may, but does not necessarily, contradict the
>>>> dictionary (lexical) definition of the term. Because of this, a
>>>> stipulative definition cannot be "correct" or "incorrect"; it can only
>>>> differ from other definitions, but it can be useful for its intended
>>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>>
>>>> (1) x ∉ Provable if and only if p
>>>> says that p is true if and only if we
>>>> HAVE NO WAY to know that p is true.
>>>>
>>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>>> NOT ALLOWED.
>>>
>>
>> If a proof is trying to prove that cats are not dogs begins
>> with the premise that cats are dogs the proof will fail.
>> Tarski does this same thing with his line (1).
>
> No, a lot of proof to show that As are not Bs, will begin with an
> assumption that As are Bs, and then show that as a necessary result of
> that, we get a contradiciton.
>
> That you don't understand this shows your lack of knowledge.
>
> For example if I have an equation with two variable, and I want to prove
> that the variables can not have an equal value at a root of the
> equation, I can replace one with the other and look at the result, if
> that can never be 0, I have proven that no root has x equal to y.
>
> So, the key to a proof by contradictions is we start with an assumption,
> an "if x" (or if cats are dogs) and we then manipulate thing, all under
> the assumption of if x, then ... and if the results ends up at
>
> if x, then true = false
>
> The proof hasn't "failed" but we have proven
>
>>
>> He assumes that we only know that p is true if and
>> only if we have no way to know that p is true.
>>
>
> No, he starts from the PROVEN statement (proven earlier in the paper)
> that we know there exists a statement x, that is in not provable if and
> only if p is true.
>

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?

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

True does not mean "Known True" it means "IS True".

We don't need to know everything that is true, in fact, we can't.

Note also, we may be able to prove it true, just not in that system.

Remember Pr is the set of statement provable IN THAT SYSTEM.

You don't seem to understand the concept of formal system of logic.

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?

--
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/21/24 10:20 PM, olcott wrote:
> On 1/21/2024 9:14 PM, Richard Damon wrote:
>> On 1/21/24 9:36 PM, olcott wrote:
>>> On 1/21/2024 8:04 PM, Richard Damon wrote:
>>>> On 1/21/24 8:18 PM, olcott wrote:
>>>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>>>> 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.
>>>>>>>
>>>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>>>> impossible.
>>>>>>>
>>>>>>  > You don't get to "erase" statements.
>>>>>
>>>>> A stipulative definition is a type of definition in which a new or
>>>>> currently existing term is given a new specific meaning for the
>>>>> purposes
>>>>> of argument or discussion in a given context. When the term already
>>>>> exists, this definition may, but does not necessarily, contradict the
>>>>> dictionary (lexical) definition of the term. Because of this, a
>>>>> stipulative definition cannot be "correct" or "incorrect"; it can only
>>>>> differ from other definitions, but it can be useful for its intended
>>>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>>>
>>>>> (1) x ∉ Provable if and only if p
>>>>> says that p is true if and only if we
>>>>> HAVE NO WAY to know that p is true.
>>>>>
>>>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>>>> NOT ALLOWED.
>>>>
>>>
>>> If a proof is trying to prove that cats are not dogs begins
>>> with the premise that cats are dogs the proof will fail.
>>> Tarski does this same thing with his line (1).
>>
>> No, a lot of proof to show that As are not Bs, will begin with an
>> assumption that As are Bs, and then show that as a necessary result of
>> that, we get a contradiciton.
>>
>> That you don't understand this shows your lack of knowledge.
>>
>> For example if I have an equation with two variable, and I want to
>> prove that the variables can not have an equal value at a root of the
>> equation, I can replace one with the other and look at the result, if
>> that can never be 0, I have proven that no root has x equal to y.
>>
>> So, the key to a proof by contradictions is we start with an
>> assumption, an "if x" (or if cats are dogs) and we then manipulate
>> thing, all under the assumption of if x, then ... and if the results
>> ends up at
>>
>> if x, then true = false
>>
>> The proof hasn't "failed" but we have proven
>>
>>>
>>> He assumes that we only know that p is true if and
>>> only if we have no way to know that p is true.
>>>
>>
>> No, he starts from the PROVEN statement (proven earlier in the paper)
>> that we know there exists a statement x, that is in not provable if
>> and only if p is true.
>>
>
> What page?
>

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, except that
the Liar can't be a truth bearer.

Your limits of understanding do not restrict what someone else can
prove, only your ability to understand what he proved.

Trying to refute something you don't understand is just a fool's errand.

On 1/21/2024 9:35 PM, Richard Damon wrote:
> On 1/21/24 10:20 PM, olcott wrote:
>> On 1/21/2024 9:14 PM, Richard Damon wrote:
>>> On 1/21/24 9:36 PM, olcott wrote:
>>>> On 1/21/2024 8:04 PM, Richard Damon wrote:
>>>>> On 1/21/24 8:18 PM, olcott wrote:
>>>>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>>>>> 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.
>>>>>>>>
>>>>>>>> Then Tarski gets the truth predicate that he falsely assumed was
>>>>>>>> impossible.
>>>>>>>>
>>>>>>>  > You don't get to "erase" statements.
>>>>>>
>>>>>> A stipulative definition is a type of definition in which a new or
>>>>>> currently existing term is given a new specific meaning for the
>>>>>> purposes
>>>>>> of argument or discussion in a given context. When the term already
>>>>>> exists, this definition may, but does not necessarily, contradict the
>>>>>> dictionary (lexical) definition of the term. Because of this, a
>>>>>> stipulative definition cannot be "correct" or "incorrect"; it can
>>>>>> only
>>>>>> differ from other definitions, but it can be useful for its intended
>>>>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>>>>
>>>>>> (1) x ∉ Provable if and only if p
>>>>>> says that p is true if and only if we
>>>>>> HAVE NO WAY to know that p is true.
>>>>>>
>>>>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>>>>> NOT ALLOWED.
>>>>>
>>>>
>>>> If a proof is trying to prove that cats are not dogs begins
>>>> with the premise that cats are dogs the proof will fail.
>>>> Tarski does this same thing with his line (1).
>>>
>>> No, a lot of proof to show that As are not Bs, will begin with an
>>> assumption that As are Bs, and then show that as a necessary result
>>> of that, we get a contradiciton.
>>>
>>> That you don't understand this shows your lack of knowledge.
>>>
>>> For example if I have an equation with two variable, and I want to
>>> prove that the variables can not have an equal value at a root of the
>>> equation, I can replace one with the other and look at the result, if
>>> that can never be 0, I have proven that no root has x equal to y.
>>>
>>> So, the key to a proof by contradictions is we start with an
>>> assumption, an "if x" (or if cats are dogs) and we then manipulate
>>> thing, all under the assumption of if x, then ... and if the results
>>> ends up at
>>>
>>> if x, then true = false
>>>
>>> The proof hasn't "failed" but we have proven
>>>
>>>>
>>>> He assumes that we only know that p is true if and
>>>> only if we have no way to know that p is true.
>>>>
>>>
>>> No, he starts from the PROVEN statement (proven earlier in the paper)
>>> that we know there exists a statement x, that is in not provable if
>>> and only if p is true.
>>>
>>
>> What page?
>>
>
> Read the paragraph above statement (1), he references his "Th I"
>
> He also describes a textual man[pulation to perform on that proof to get
> some addition properties, that he then comes to statement (1) as the
> conclusion.
>
> You need to find an error in Th I, or in these steps he is describing,
> in order to attempt to disprove his statemet. Not just disagree with the
> conclusion, but find an error in logic or an assumption that he is
> making in the statement.
>
> I doubt you understand the logic well enough to do that, since I doubt
> there is an error since it has been looked over by people much smarter
> than you.

On 1/21/24 10:44 PM, olcott wrote:
> On 1/21/2024 9:35 PM, Richard Damon wrote:
>> On 1/21/24 10:20 PM, olcott wrote:
>>> On 1/21/2024 9:14 PM, Richard Damon wrote:
>>>> On 1/21/24 9:36 PM, olcott wrote:
>>>>> On 1/21/2024 8:04 PM, Richard Damon wrote:
>>>>>> On 1/21/24 8:18 PM, olcott wrote:
>>>>>>> On 1/21/2024 7:03 PM, Richard Damon wrote:
>>>>>>>> On 1/21/24 7:46 PM, olcott wrote:
>>>>>>>>> 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.
>>>>>>>>>
>>>>>>>>> Then Tarski gets the truth predicate that he falsely assumed
>>>>>>>>> was impossible.
>>>>>>>>>
>>>>>>>>  > You don't get to "erase" statements.
>>>>>>>
>>>>>>> A stipulative definition is a type of definition in which a new or
>>>>>>> currently existing term is given a new specific meaning for the
>>>>>>> purposes
>>>>>>> of argument or discussion in a given context. When the term already
>>>>>>> exists, this definition may, but does not necessarily, contradict
>>>>>>> the
>>>>>>> dictionary (lexical) definition of the term. Because of this, a
>>>>>>> stipulative definition cannot be "correct" or "incorrect"; it can
>>>>>>> only
>>>>>>> differ from other definitions, but it can be useful for its intended
>>>>>>> purpose. https://en.wikipedia.org/wiki/Stipulative_definition
>>>>>>>
>>>>>>> (1) x ∉ Provable if and only if p
>>>>>>> says that p is true if and only if we
>>>>>>> HAVE NO WAY to know that p is true.
>>>>>>>
>>>>>>> THUS IT IS STIPULATED THAT IT IS REPLACED BY THIS
>>>>>> NOT ALLOWED.
>>>>>>
>>>>>
>>>>> If a proof is trying to prove that cats are not dogs begins
>>>>> with the premise that cats are dogs the proof will fail.
>>>>> Tarski does this same thing with his line (1).
>>>>
>>>> No, a lot of proof to show that As are not Bs, will begin with an
>>>> assumption that As are Bs, and then show that as a necessary result
>>>> of that, we get a contradiciton.
>>>>
>>>> That you don't understand this shows your lack of knowledge.
>>>>
>>>> For example if I have an equation with two variable, and I want to
>>>> prove that the variables can not have an equal value at a root of
>>>> the equation, I can replace one with the other and look at the
>>>> result, if that can never be 0, I have proven that no root has x
>>>> equal to y.
>>>>
>>>> So, the key to a proof by contradictions is we start with an
>>>> assumption, an "if x" (or if cats are dogs) and we then manipulate
>>>> thing, all under the assumption of if x, then ... and if the results
>>>> ends up at
>>>>
>>>> if x, then true = false
>>>>
>>>> The proof hasn't "failed" but we have proven
>>>>
>>>>>
>>>>> He assumes that we only know that p is true if and
>>>>> only if we have no way to know that p is true.
>>>>>
>>>>
>>>> No, he starts from the PROVEN statement (proven earlier in the
>>>> paper) that we know there exists a statement x, that is in not
>>>> provable if and only if p is true.
>>>>
>>>
>>> What page?
>>>
>>
>> Read the paragraph above statement (1), he references his "Th I"
>>
>> He also describes a textual man[pulation to perform on that proof to
>> get some addition properties, that he then comes to statement (1) as
>> the conclusion.
>>
>> You need to find an error in Th I, or in these steps he is describing,
>> in order to attempt to disprove his statemet. Not just disagree with
>> the conclusion, but find an error in logic or an assumption that he is
>> making in the statement.
>>
>> I doubt you understand the logic well enough to do that, since I doubt
>> there is an error since it has been looked over by people much smarter
>> than you.
>
> 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
>
> There are still many people today that are simply too stupid
> to understand that the Liar Paradox IS NOT A TRUTH BEARER.
>

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,

On 1/21/24 8:04 PM, 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
>

But that doesn't mean it could DO Higher Order Logic as first order logic.

You don't seem to understand the issues with having uncountable size
domains of regard has on logic system.

It just shows your inadequate knowledge of logic.

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.