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: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.
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? >>>>>>>>>>>>>>>>>>>
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.
(1) x ∉ Provable if and only if p
must be corrected to say
(1) x ∈ Provable if and only if p
On 1/21/2024 10:06 PM, Richard Damon wrote:
On 1/21/24 11:01 PM, olcott wrote:
On 1/21/2024 9:39 PM, Richard Damon wrote:
On 1/21/24 10:30 PM, olcott wrote:
On 1/21/2024 9:28 PM, Richard Damon wrote:
On 1/21/24 10:22 PM, olcott wrote:
On 1/21/2024 9:19 PM, Richard Damon wrote:
On 1/21/24 9:55 PM, olcott wrote:
On 1/21/2024 8:28 PM, Richard Damon wrote:
On 1/21/24 9:18 PM, olcott wrote:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote: >>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
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.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? >>>>>>>>>>>>>>>>>>>>>
So are the real numbers countable? Isn't Cantor's >>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his >>>>>>>>>>>>>>>>>>>> argument invalid?
unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable >>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation >>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle. >>>>>>>>>>>>>>>>>>>>>
Provability doesn't give a flying fuck about >>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are. >>>>>>>>>>>>>>>>>>>>
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is >>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It >>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical >>>>>>>>>>>>>>>> issues (as I understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that >>>>>>>>>>>>>>> automatically generated the directed graph of the >>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive >>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite >>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not >>>>>>>>>>>>>> valid.
Olcott doesn't understand that diagonalization is not the >>>>>>>>>>>>>> same as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another >>>>>>>>>>>>> x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that >>>>>>>>>>>> it's unprovable. There are different ways to find out that >>>>>>>>>>>> it's unprovable, or different ways to understand that it's >>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
But there are x that are unprovable in L because the chain to >>>>>>>>>> them is infinitely long, which makes them true but unprovale. >>>>>>>>>>
(1) x ∉ Provable if and only if p
(2) x ∈ True if and only if p
(3) x ∉ Provable if and only if x ∈ True.
When we correct the erroneous line (1) then line (3) becomes >>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
Thus making your (infinite chain) x simply untrue.
WHy is it "erroneous", it is a simple statement previously proven. >>>>>>>>
He proved that there are some things that we know
are true yet have no way what-so-ever to know that
they are true?
No, he proved that there are some things that ARE true that we can >>>>>> not prove to be true.
How the Hell is he going to do that on his basis
of the Liar Paradox?
Read his proof. And it isn't "based' on the Liar's paradox,
*It sure as Hell is anchored in the Liar Paradox*
He get his line (1) directly from the Liar Paradox
Below he shows how he transforms the Liar Paradox
x ∉ True if and only if p
into his line (1) by replacing "Tr" (for True)
with 'Pr" (for provable) Here is his line
(1) x ∉ Provable if and only if p
<page 275>
In accordance with the first
part of Th. I we can obtain the negation of one of the sentences
in condition (α) of convention T of § 3 as a consequence of the >>> definition of the symbol 'Pr' (provided we replace 'Tr' in this
convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf
</page 275>
<page 248> Liar Paradox
Should we succeed in constructing in the metalanguage
a correct definition of truth, then
It would
then be possible to reconstruct the antinomy of the liar in the
metalanguage, by forming in the language itself a sentence x
such that the sentence of the metalanguage which is correlated
with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
</page 248>
Many people today are simply too stupid to understand
that the Liar Paradox is simply not a truth bearer
thus must be rejected by any correct True(L, x) predicate.
When Tarski assumes the Liar Paradox as a premise
this must be rejected and over-ruled.
Where does he assume it as a premise?
His line (1) is a premise.
(1) x ∉ Provable if and only if p
must be corrected to say
(1) x ∈ Provable if and only if p
What was actually wrong with (1). You haven't shown the error in logic.
His line (1) <is> an adapted form of the actual Liar
Paradox as I have shown by the quotes above.
I think that you are smart enough to understand that
the Liar Paradox is neither true nor false.
It turns out the the key error is Tarski's line (1)
that began as the Liar Paradox
(1) x ∉ True if and only if p
and was transformed into this
(1) x ∉ Provable if and only if p
Intelligent people understand that the Liar Paradox is
not a truth bearer, thus asking whether it is true or
false is like asking whether a question is true or false.
Is this sentence true or false: What time is it?
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote:
Tarski didn't understand that the correct
evaluation of the Liar Paradox requires
an infinite cycle in the directed graph
of its evaluation sequence.
You don't understand the difference between
diagonalization and infinite recursion.
Do you think the real numbers are countable?
Diagonalization is a process by which we know that
x is unprovable in L that makes sure to ignore the
reason why x is unprovable in L.
So are the real numbers countable? Isn't Cantor's number >>>>>>>>>>>> pathologically self-referential, making his argument invalid? >>>>>>>>>>>>
unify_with_occurs_check(LP, not(true(LP))).
correctly determines that LP is unprovable
BECAUSE the directed graph of its evaluation
sequence contains an infinite cycle.
Provability doesn't give a flying fuck about evaluation >>>>>>>>>>>> cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems
ignore make it wrong is like saying that ignorance is
knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It rejects ALL >>>>>>>> cycles, even if they don't cause logical issues (as I understand >>>>>>>> it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas such >>>>>> as ¬True(¬True(¬True(...))) are already not valid.
Olcott doesn't understand that diagonalization is not the same as
infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another
x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's
unprovable. There are different ways to find out that it's
unprovable, or different ways to understand that it's unprovable,
but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
The semantics only
enter when the theory is interpreted. In a first order theory if x is
undecidable then it is true in some models and false in all others.
If neither x nor ¬x is provable you can add either one (but not both)
to the axioms of the theory and get another theory where x is decidable.
Mikko
On 1/22/2024 1:00 PM, immibis wrote:
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote:
Tarski didn't understand that the correct
evaluation of the Liar Paradox requires
an infinite cycle in the directed graph
of its evaluation sequence.
You don't understand the difference between
diagonalization and infinite recursion.
Do you think the real numbers are countable?
Diagonalization is a process by which we know that >>>>>>>>>>>>>>> x is unprovable in L that makes sure to ignore the >>>>>>>>>>>>>>> reason why x is unprovable in L.
So are the real numbers countable? Isn't Cantor's number >>>>>>>>>>>>>> pathologically self-referential, making his argument invalid? >>>>>>>>>>>>>>
unify_with_occurs_check(LP, not(true(LP))).
correctly determines that LP is unprovable
BECAUSE the directed graph of its evaluation
sequence contains an infinite cycle.
Provability doesn't give a flying fuck about evaluation >>>>>>>>>>>>>> cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>> ignore make it wrong is like saying that ignorance is
knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It rejects >>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I
understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas
such as ¬True(¬True(¬True(...))) are already not valid.
Olcott doesn't understand that diagonalization is not the same >>>>>>>> as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another
x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's
unprovable. There are different ways to find out that it's
unprovable, or different ways to understand that it's unprovable,
but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
On 1/22/2024 1:16 PM, immibis wrote:
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote: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.
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? >>>>>>>>>>>>>>>>>
So are the real numbers countable? Isn't Cantor's number >>>>>>>>>>>>>>>> pathologically self-referential, making his argument >>>>>>>>>>>>>>>> invalid?
unify_with_occurs_check(LP, not(true(LP))).
correctly determines that LP is unprovable
BECAUSE the directed graph of its evaluation >>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
Provability doesn't give a flying fuck about evaluation >>>>>>>>>>>>>>>> cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is >>>>>>>>>>>>> knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It rejects >>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I >>>>>>>>>>>> understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas >>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid. >>>>>>>>>>
Olcott doesn't understand that diagonalization is not the same >>>>>>>>>> as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another
x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's
unprovable. There are different ways to find out that it's
unprovable, or different ways to understand that it's
unprovable, but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
LP := ~True(LP)
On 1/22/2024 1:56 PM, immibis wrote:
On 1/22/24 20:47, olcott wrote:
On 1/22/2024 1:16 PM, immibis wrote:
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote: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.
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? >>>>>>>>>>>>>>>>>>>
So are the real numbers countable? Isn't Cantor's >>>>>>>>>>>>>>>>>> number pathologically self-referential, making his >>>>>>>>>>>>>>>>>> argument invalid?
unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable >>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation >>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
Provability doesn't give a flying fuck about >>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is >>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It >>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical >>>>>>>>>>>>>> issues (as I understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite
formulas such as ¬True(¬True(¬True(...))) are already not >>>>>>>>>>>> valid.
Olcott doesn't understand that diagonalization is not the >>>>>>>>>>>> same as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another >>>>>>>>>>> x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's >>>>>>>>>> unprovable. There are different ways to find out that it's >>>>>>>>>> unprovable, or different ways to understand that it's
unprovable, but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
LP := ~True(LP)
True(LP) is not a logical formula. Gödel proved that.
He proved no such thing.
He proved that G cannot be proved in PA yet can be proved in
metamathematics.
On 1/22/2024 5:20 PM, immibis wrote:
On 1/22/24 21:30, olcott wrote:
On 1/22/2024 1:56 PM, immibis wrote:
On 1/22/24 20:47, olcott wrote:
On 1/22/2024 1:16 PM, immibis wrote:
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote: >>>>>>>>>>>>>>>>>>>>>> On 1/21/24 23:56, olcott wrote:
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.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? >>>>>>>>>>>>>>>>>>>>>
So are the real numbers countable? Isn't Cantor's >>>>>>>>>>>>>>>>>>>> number pathologically self-referential, making his >>>>>>>>>>>>>>>>>>>> argument invalid?
unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable >>>>>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation >>>>>>>>>>>>>>>>>>>>> sequence contains an infinite cycle. >>>>>>>>>>>>>>>>>>>>>
Provability doesn't give a flying fuck about >>>>>>>>>>>>>>>>>>>> evaluation cycles, whatever those are. >>>>>>>>>>>>>>>>>>>>
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is >>>>>>>>>>>>>>>>> knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It >>>>>>>>>>>>>>>> rejects ALL cycles, even if they don't cause logical >>>>>>>>>>>>>>>> issues (as I understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that >>>>>>>>>>>>>>> automatically generated the directed graph of the >>>>>>>>>>>>>>> evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive >>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite >>>>>>>>>>>>>> formulas such as ¬True(¬True(¬True(...))) are already not >>>>>>>>>>>>>> valid.
Olcott doesn't understand that diagonalization is not the >>>>>>>>>>>>>> same as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another >>>>>>>>>>>>> x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that >>>>>>>>>>>> it's unprovable. There are different ways to find out that >>>>>>>>>>>> it's unprovable, or different ways to understand that it's >>>>>>>>>>>> unprovable, but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
LP := ~True(LP)
True(LP) is not a logical formula. Gödel proved that.
He proved no such thing.
He proved that G cannot be proved in PA yet can be proved in
metamathematics.
I don't think you get this. Every system has a G that can't be proved
in that system,
Yet can be proved in metamathematics.
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote:
Tarski didn't understand that the correct
evaluation of the Liar Paradox requires
an infinite cycle in the directed graph
of its evaluation sequence.
You don't understand the difference between
diagonalization and infinite recursion.
Do you think the real numbers are countable?
Diagonalization is a process by which we know that
x is unprovable in L that makes sure to ignore the
reason why x is unprovable in L.
So are the real numbers countable? Isn't Cantor's number >>>>>>>>>>>> pathologically self-referential, making his argument invalid? >>>>>>>>>>>>
unify_with_occurs_check(LP, not(true(LP))).
correctly determines that LP is unprovable
BECAUSE the directed graph of its evaluation
sequence contains an infinite cycle.
Provability doesn't give a flying fuck about evaluation >>>>>>>>>>>> cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems
ignore make it wrong is like saying that ignorance is
knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It rejects ALL >>>>>>>> cycles, even if they don't cause logical issues (as I understand >>>>>>>> it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas such >>>>>> as ¬True(¬True(¬True(...))) are already not valid.
Olcott doesn't understand that diagonalization is not the same as
infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another
x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's
unprovable. There are different ways to find out that it's
unprovable, or different ways to understand that it's unprovable,
but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
The semantics only
enter when the theory is interpreted. In a first order theory if x is
undecidable then it is true in some models and false in all others.
If neither x nor ¬x is provable you can add either one (but not both)
to the axioms of the theory and get another theory where x is decidable.
Mikko
On 1/22/2024 9:43 PM, Richard Damon wrote:
On 1/22/24 1:59 PM, olcott wrote:Carefully study every single word of my quotes from
On 1/22/2024 6:23 AM, Richard Damon wrote:
On 1/21/24 11:37 PM, olcott wrote:
On 1/21/2024 10:06 PM, Richard Damon wrote:
On 1/21/24 11:01 PM, olcott wrote:
On 1/21/2024 9:39 PM, Richard Damon wrote:
On 1/21/24 10:30 PM, olcott wrote:
On 1/21/2024 9:28 PM, Richard Damon wrote:
On 1/21/24 10:22 PM, olcott wrote:
On 1/21/2024 9:19 PM, Richard Damon wrote:
On 1/21/24 9:55 PM, olcott wrote:
On 1/21/2024 8:28 PM, Richard Damon wrote:
On 1/21/24 9:18 PM, olcott wrote:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote: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.
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. >>>>>>>>>>>>>>>>>>>>>>>>>>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. >>>>>>>>>>>>>>>>>>>>>>>>>
Do you think the real numbers are countable? >>>>>>>>>>>>>>>>>>>>>>>>>
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. >>>>>>>>>>>>>>>
This what Tarski should have done.
But there are x that are unprovable in L because the chain >>>>>>>>>>>>>> to them is infinitely long, which makes them true but >>>>>>>>>>>>>> unprovale.
(1) x ∉ Provable if and only if p
(2) x ∈ True if and only if p
(3) x ∉ Provable if and only if x ∈ True.
When we correct the erroneous line (1) then line (3) becomes >>>>>>>>>>>>> (3) x ∈ Provable if and only if x ∈ True.
Thus making your (infinite chain) x simply untrue.
WHy is it "erroneous", it is a simple statement previously >>>>>>>>>>>> proven.
He proved that there are some things that we know
are true yet have no way what-so-ever to know that
they are true?
No, he proved that there are some things that ARE true that we >>>>>>>>>> can not prove to be true.
How the Hell is he going to do that on his basis
of the Liar Paradox?
Read his proof. And it isn't "based' on the Liar's paradox,
*It sure as Hell is anchored in the Liar Paradox*
He get his line (1) directly from the Liar Paradox
Below he shows how he transforms the Liar Paradox
x ∉ True if and only if p
into his line (1) by replacing "Tr" (for True)
with 'Pr" (for provable) Here is his line
(1) x ∉ Provable if and only if p
<page 275>
In accordance with the first
part of Th. I we can obtain the negation of one of the sentences >>>>>>> in condition (α) of convention T of § 3 as a consequence of the
definition of the symbol 'Pr' (provided we replace 'Tr' in this >>>>>>> convention by 'Pr'). https://liarparadox.org/Tarski_275_276.pdf >>>>>>> </page 275>
<page 248> Liar Paradox
Should we succeed in constructing in the metalanguage
a correct definition of truth, then
It would
then be possible to reconstruct the antinomy of the liar in the >>>>>>> metalanguage, by forming in the language itself a sentence x >>>>>>> such that the sentence of the metalanguage which is correlated >>>>>>> with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
</page 248>
Many people today are simply too stupid to understand
that the Liar Paradox is simply not a truth bearer
thus must be rejected by any correct True(L, x) predicate.
When Tarski assumes the Liar Paradox as a premise
this must be rejected and over-ruled.
Where does he assume it as a premise?
His line (1) is a premise.
Then why does he say, "In other words, we can construct ... " just
above it.
(1) is a CONCLUSION from the previous paragraph.
you clearly don't know much about logic.
(1) x ∉ Provable if and only if p
must be corrected to say
(1) x ∈ Provable if and only if p
What was actually wrong with (1). You haven't shown the error in
logic.
His line (1) <is> an adapted form of the actual Liar
Paradox as I have shown by the quotes above.
NO, the liar paradox says NOTHING about "Provable".
Tarski says that he takes the Liar Paradox:
x ∉ True if and only if p
and changes it to this
(1) x ∉ Provable if and only if p
on page <275> quoted above.
It is <page 248> quoted above where he says
that he is using the actual Liar Paradox.
You have to carefully study what I say before
providing a rebuttal. It took me a half hour
to compose the Tarski quotes.
Note, page 247 doesn't say "start with the Liar's Paradox" he points
out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that the
<page 248> and <page 275> again and again until you
see that what I say is true.
I had to study these four pages hundreds and hundreds
of times before I could see that his line (1) was
adapted from:
*x ∉ True if and only if p*
which <is> his version of the Liar Paradox.
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:As you fail to understand it.
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) >>>>>>>>>>
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as ¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas such as >>>>>>>>> ¬True(¬True(¬True(...))) are already not valid.
Olcott doesn't understand that diagonalization is not the same as >>>>>>>>> infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another
x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's
unprovable. There are different ways to find out that it's unprovable, >>>>>>> or different ways to understand that it's unprovable, but not reasons >>>>>>> why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
On 1/22/2024 4:17 AM, Mikko wrote:
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
On 1/23/24 00:31, olcott wrote:
On 1/22/2024 5:20 PM, immibis wrote:Is metamathematics a system?
On 1/22/24 21:30, olcott wrote:
On 1/22/2024 1:56 PM, immibis wrote:
On 1/22/24 20:47, olcott wrote:
On 1/22/2024 1:16 PM, immibis wrote:
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:As you fail to understand it.
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.
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.
You don't understand the difference between diagonalization and
infinite recursion.
Do you think the real numbers are countable? >>>>>>>>>>>>>>>>>>>>>>
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) >>>>>>>>>>>>>>>>
I took 18 months creating Minimal Type Theory that >>>>>>>>>>>>>>>> automatically generated the directed graph of the >>>>>>>>>>>>>>>> evaluation sequence of any of its expressions. >>>>>>>>>>>>>>>> It sued syntax similar to FOL yet is as expressive >>>>>>>>>>>>>>>> as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as ¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas such as
¬True(¬True(¬True(...))) are already not valid. >>>>>>>>>>>>>>>
Olcott doesn't understand that diagonalization is not the same as
infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another >>>>>>>>>>>>>> x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's >>>>>>>>>>>>> unprovable. There are different ways to find out that it's unprovable,
or different ways to understand that it's unprovable, but not reasons
why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
LP := ~True(LP)
True(LP) is not a logical formula. Gödel proved that.
He proved no such thing.
He proved that G cannot be proved in PA yet can be proved in metamathematics.
I don't think you get this. Every system has a G that can't be proved
in that system,
Yet can be proved in metamathematics.
On 1/22/2024 10:22 PM, Richard Damon wrote:
On 1/22/24 10:53 PM, olcott wrote:
On 1/22/2024 9:43 PM, Richard Damon wrote:
On 1/22/24 1:59 PM, olcott wrote:Carefully study every single word of my quotes from
On 1/22/2024 6:23 AM, Richard Damon wrote:
On 1/21/24 11:37 PM, olcott wrote:
On 1/21/2024 10:06 PM, Richard Damon wrote:
On 1/21/24 11:01 PM, olcott wrote:
On 1/21/2024 9:39 PM, Richard Damon wrote:
On 1/21/24 10:30 PM, olcott wrote:*It sure as Hell is anchored in the Liar Paradox*
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. >>>>>>>>>>>>>>>>>>>>>>>>>>>>
As you fail to understand it.You don't understand the difference between >>>>>>>>>>>>>>>>>>>>>>>>>>>> diagonalization and infinite recursion. >>>>>>>>>>>>>>>>>>>>>>>>>>>>Diagonalization is a process by which we know >>>>>>>>>>>>>>>>>>>>>>>>>>> that
Do you think the real numbers are countable? >>>>>>>>>>>>>>>>>>>>>>>>>>>
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) >>>>>>>>>>>>>>>>>>>>>
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, >>>>>>>>>
He get his line (1) directly from the Liar Paradox
Below he shows how he transforms the Liar Paradox
x ∉ True if and only if p
into his line (1) by replacing "Tr" (for True)
with 'Pr" (for provable) Here is his line
(1) x ∉ Provable if and only if p
<page 275>
In accordance with the first
part of Th. I we can obtain the negation of one of the >>>>>>>>> sentences
in condition (α) of convention T of § 3 as a consequence of >>>>>>>>> the
definition of the symbol 'Pr' (provided we replace 'Tr' in >>>>>>>>> this
convention by 'Pr').
https://liarparadox.org/Tarski_275_276.pdf
</page 275>
<page 248> Liar Paradox
Should we succeed in constructing in the metalanguage >>>>>>>>> a correct definition of truth, then
It would
then be possible to reconstruct the antinomy of the liar in >>>>>>>>> the
metalanguage, by forming in the language itself a sentence x >>>>>>>>> such that the sentence of the metalanguage which is correlated >>>>>>>>> with x asserts that x is not a true sentence.
https://liarparadox.org/Tarski_247_248.pdf
</page 248>
Many people today are simply too stupid to understand
that the Liar Paradox is simply not a truth bearer
thus must be rejected by any correct True(L, x) predicate.
When Tarski assumes the Liar Paradox as a premise
this must be rejected and over-ruled.
Where does he assume it as a premise?
His line (1) is a premise.
Then why does he say, "In other words, we can construct ... " just >>>>>> above it.
(1) is a CONCLUSION from the previous paragraph.
you clearly don't know much about logic.
(1) x ∉ Provable if and only if p
must be corrected to say
(1) x ∈ Provable if and only if p
What was actually wrong with (1). You haven't shown the error in >>>>>>>> logic.
His line (1) <is> an adapted form of the actual Liar
Paradox as I have shown by the quotes above.
NO, the liar paradox says NOTHING about "Provable".
Tarski says that he takes the Liar Paradox:
x ∉ True if and only if p
and changes it to this
(1) x ∉ Provable if and only if p
on page <275> quoted above.
It is <page 248> quoted above where he says
that he is using the actual Liar Paradox.
You have to carefully study what I say before
providing a rebuttal. It took me a half hour
to compose the Tarski quotes.
Note, page 247 doesn't say "start with the Liar's Paradox" he points
out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie, show that
the
<page 248> and <page 275> again and again until you
see that what I say is true.
I had to study these four pages hundreds and hundreds
of times before I could see that his line (1) was
adapted from:
*x ∉ True if and only if p*
which <is> his version of the Liar Paradox.
Nope, He doesn't "ASSUME" the Liar has a true value, he shows that
given a construction of the procedure that answers if any statement is
True, we can show that there exist a statment, with a truth value,
that turns out to be the Liar.
In other words you believe that the Liar Paradox has a truth value?
In other words you believe that the Liar Paradox has a truth value?
On 1/23/2024 3:27 AM, Mikko wrote:
On 2024-01-22 19:16:49 +0000, immibis said:
On 1/22/24 20:08, olcott wrote:
On 1/22/2024 1:00 PM, immibis wrote:Every logical formula has a truth value.
On 1/22/24 19:39, olcott wrote:*That is their mistake*
On 1/22/2024 4:17 AM, Mikko wrote:
On 2024-01-22 02:18:35 +0000, olcott said:
On 1/21/2024 8:07 PM, immibis wrote:
On 1/22/24 02:43, olcott wrote:
On 1/21/2024 7:38 PM, immibis wrote:
On 1/22/24 02:04, olcott wrote:
On 1/21/2024 6:58 PM, Richard Damon wrote:
On 1/21/24 7:54 PM, olcott wrote:
On 1/21/2024 6:50 PM, immibis wrote:
On 1/22/24 01:37, olcott wrote:
On 1/21/2024 6:27 PM, immibis wrote:
On 1/22/24 01:13, olcott wrote:
On 1/21/2024 6:04 PM, immibis wrote:
On 1/21/24 23:56, olcott wrote: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.
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? >>>>>>>>>>>>>>>>>>
So are the real numbers countable? Isn't Cantor's >>>>>>>>>>>>>>>>> number pathologically self-referential, making his >>>>>>>>>>>>>>>>> argument invalid?
unify_with_occurs_check(LP, not(true(LP))). >>>>>>>>>>>>>>>>>> correctly determines that LP is unprovable >>>>>>>>>>>>>>>>>> BECAUSE the directed graph of its evaluation >>>>>>>>>>>>>>>>>> sequence contains an infinite cycle.
Provability doesn't give a flying fuck about evaluation >>>>>>>>>>>>>>>>> cycles, whatever those are.
It sure does in Prolog.
Then Prolog is wrong.
That Prolog pays attention to details that other systems >>>>>>>>>>>>>> ignore make it wrong is like saying that ignorance is >>>>>>>>>>>>>> knowledge and knowledge is incorrect.
Prolog handles SIMPLE logic system and problems. It rejects >>>>>>>>>>>>> ALL cycles, even if they don't cause logical issues (as I >>>>>>>>>>>>> understand it)
As you fail to understand it.
I took 18 months creating Minimal Type Theory that
automatically generated the directed graph of the
evaluation sequence of any of its expressions.
It sued syntax similar to FOL yet is as expressive
as HOL. I encode a SOL expression in MTT.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
You are rebutting the infinite formulas such as
¬True(¬True(¬True(...)))
But this is already in the standard theory. Infinite formulas >>>>>>>>>>> such as ¬True(¬True(¬True(...))) are already not valid. >>>>>>>>>>>
Olcott doesn't understand that diagonalization is not the >>>>>>>>>>> same as infinite recursion.
Finally a reply that is not nonsense.
Diagonalization only knows that for some reason or another >>>>>>>>>> x is unprovable in L.
I dispute the notion of "reasons". It's just a fact that it's >>>>>>>>> unprovable. There are different ways to find out that it's
unprovable, or different ways to understand that it's
unprovable, but not reasons why it's unprovable.
If the reason that x is unprovable in L is that x
is semantically incorrect in L then instead of saying
that x is undecidable in L the decider rejects x
as invalid input.
This what Tarski should have done.
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
Nobody is talking about semantics except for you.
What is the formal truth value of x?
Something that seems over your head is the self-contradictory
sentences cannot possibly have a truth value.
In a particular interpretation. In another interpretation it
may have a different interpretation. For example,
∀x ∀y (xy = yx)
is true about real numbers but not about quaternions.
Mikko
Tarski's Liar Paradox has no truth value.
(1) x ∉ True if and only if p
On 1/23/2024 3:23 AM, Mikko wrote:
On 2024-01-22 18:39:44 +0000, olcott said:
On 1/22/2024 4:17 AM, Mikko wrote:
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
As there are no semantics in a formal system there can
be no semantic errors. However, it is possible that the
intended interpretation is not a model of the system.
Then one may hope that a small change will make it useful
for its intended purpose.
Mikko
True is an inherently semantic concept, thus logic systems
always have semantics. The truth tables for propositional
logic provide the semantics of its operators.
The Tarski undefinability theorem is totally refuted by
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
On 1/23/2024 7:41 AM, immibis wrote:
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value?
If YOU believe that True(L,x) exists then YOU believe the Liar Paradox
has a truth value.
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
On 1/23/2024 7:41 AM, immibis wrote:
On 1/23/24 01:31, olcott wrote:
On 1/22/2024 6:10 PM, immibis wrote:
On 1/23/24 00:31, olcott wrote:
On 1/22/2024 5:20 PM, immibis wrote:Is metamathematics a system?
I don't think you get this. Every system has a G that can't be
proved in that system,
Yet can be proved in metamathematics.
Yes
Then it has a G that can't be proven OR it allows false things to be
proven.
Read the first few pages of the introduction https://mavdisk.mnsu.edu/pj2943kt/Fall%202015/Promotion%20Application/Previous%20Years%20Article%2022%20Materials/godel-1931.pdf
It does not say that. It is merely a sentence having no truth value.
On 1/23/2024 11:23 AM, immibis wrote:
On 1/23/24 18:03, olcott wrote:
On 1/23/2024 7:41 AM, immibis wrote:Then you believe the liar paradox has a truth value.
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value?
If YOU believe that True(L,x) exists then YOU believe the Liar
Paradox has a truth value.
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) >>
Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
Thus Invalid(L, LP) is TRUE.
On 1/23/2024 9:55 AM, immibis wrote:
True is like the set of all sets which do not contain themselves.
Not at all:
True(PA, "2 + 3 = 5") is not pathological like the Liar Paradox.
On 1/23/2024 11:40 AM, immibis wrote:
On 1/23/24 17:25, olcott wrote:
It does not say that. It is merely a sentence having no truth value.
If it has no truth value, then any proof that says it has a truth
value must be wrong. Yes?
If the liar paradox is false, then it has a truth value. But it
doesn't, so it can't be false. Yes?
If True(L,x) exists, then the liar paradox has a truth value. But it
doesn't, so True(L,x) doesn't exist.
If True(L,x) exists, then the question "What time is it?" has a truth value...
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
thus Invalid(L, “this sentence is not true”) is true.
On 1/23/2024 2:04 PM, immibis wrote:
On 1/23/24 20:33, olcott wrote:
On 1/23/2024 11:40 AM, immibis wrote:Invalid should be called "independent". For example, ZF is independent
On 1/23/24 17:25, olcott wrote:
It does not say that. It is merely a sentence having no truth value.
If it has no truth value, then any proof that says it has a truth
value must be wrong. Yes?
If the liar paradox is false, then it has a truth value. But it
doesn't, so it can't be false. Yes?
If True(L,x) exists, then the liar paradox has a truth value. But it
doesn't, so True(L,x) doesn't exist.
If True(L,x) exists, then the question "What time is it?" has a truth
value...
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) >>> Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
thus Invalid(L, “this sentence is not true”) is true.
of C.
My new idea is different than this.
My new idea proves that Tarski is wrong.
On 1/23/2024 3:16 PM, immibis wrote:
On 1/23/24 21:15, olcott wrote:
On 1/23/2024 2:04 PM, immibis wrote:Your new idea is exactly this. Independent means that neither x nor ¬x
On 1/23/24 20:33, olcott wrote:
On 1/23/2024 11:40 AM, immibis wrote:Invalid should be called "independent". For example, ZF is
On 1/23/24 17:25, olcott wrote:
It does not say that. It is merely a sentence having no truth value. >>>>>>If it has no truth value, then any proof that says it has a truth
value must be wrong. Yes?
If the liar paradox is false, then it has a truth value. But it
doesn't, so it can't be false. Yes?
If True(L,x) exists, then the liar paradox has a truth value. But
it doesn't, so True(L,x) doesn't exist.
If True(L,x) exists, then the question "What time is it?" has a
truth value...
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
thus Invalid(L, “this sentence is not true”) is true.
independent of C.
My new idea is different than this.
My new idea proves that Tarski is wrong.
is provable in a system.
We must over-ride the convention of construing
that self-contradictory expressions prove anything
other than they must be rejected as incorrect.
On 1/23/2024 6:49 AM, Richard Damon wrote:
On 1/22/24 11:30 PM, olcott wrote:
On 1/22/2024 10:22 PM, Richard Damon wrote:
On 1/22/24 10:53 PM, olcott wrote:
On 1/22/2024 9:43 PM, Richard Damon wrote:
On 1/22/24 1:59 PM, olcott wrote:Carefully study every single word of my quotes from
On 1/22/2024 6:23 AM, Richard Damon wrote:
On 1/21/24 11:37 PM, olcott wrote:
(1) x ∉ Provable if and only if p
must be corrected to say
(1) x ∈ Provable if and only if p
What was actually wrong with (1). You haven't shown the error >>>>>>>>>> in logic.
His line (1) <is> an adapted form of the actual Liar
Paradox as I have shown by the quotes above.
NO, the liar paradox says NOTHING about "Provable".
Tarski says that he takes the Liar Paradox:
x ∉ True if and only if p
and changes it to this
(1) x ∉ Provable if and only if p
on page <275> quoted above.
It is <page 248> quoted above where he says
that he is using the actual Liar Paradox.
You have to carefully study what I say before
providing a rebuttal. It took me a half hour
to compose the Tarski quotes.
Note, page 247 doesn't say "start with the Liar's Paradox" he
points out that IT WOULD BE POSSIBLE TO RECONSTRUCT THE LIAR, ie,
show that the
<page 248> and <page 275> again and again until you
see that what I say is true.
I had to study these four pages hundreds and hundreds
of times before I could see that his line (1) was
adapted from:
*x ∉ True if and only if p*
which <is> his version of the Liar Paradox.
Nope, He doesn't "ASSUME" the Liar has a true value, he shows that
given a construction of the procedure that answers if any statement
is True, we can show that there exist a statment, with a truth
value, that turns out to be the Liar.
In other words you believe that the Liar Paradox has a truth value?
No, it says that anything that can lead to a proof that it does is false.
It does not say that. It is merely a sentence having no truth value.
Like the "Definiton of Truth" as Tarski defines it.
He was too dumb to know that the Liar Paradox is not a truth bearer.
When we define this corresponding pair of predicates:
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) Then we get: (~True(L, LP) & ~False(L, x)) ⊢ Invalid(L, LP).
You don't seem to understand English very well, do you.
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value?
If YOU believe that True(L,x) exists then YOU believe the Liar Paradox
has a truth value.
On 1/23/24 19:30, olcott wrote:
On 1/23/2024 11:23 AM, immibis wrote:
On 1/23/24 18:03, olcott wrote:
On 1/23/2024 7:41 AM, immibis wrote:Then you believe the liar paradox has a truth value.
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value? >>>>>If YOU believe that True(L,x) exists then YOU believe the Liar Paradox >>>>> has a truth value.
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) >>>
Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
Thus Invalid(L, LP) is TRUE.
⊢ stands for provability. True and False should be called Provable and OppositeProvable.
On 1/23/24 19:16, olcott wrote:
On 1/23/2024 9:55 AM, immibis wrote:
True is like the set of all sets which do not contain themselves.
Not at all:
True(PA, "2 + 3 = 5") is not pathological like the Liar Paradox.
S = {x | x ∉ x}
{1}∈S is not pathological.
On 1/23/24 16:14, olcott wrote:
On 1/23/2024 3:23 AM, Mikko wrote:
On 2024-01-22 18:39:44 +0000, olcott said:
On 1/22/2024 4:17 AM, Mikko wrote:
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
As there are no semantics in a formal system there can
be no semantic errors. However, it is possible that the
intended interpretation is not a model of the system.
Then one may hope that a small change will make it useful
for its intended purpose.
Mikko
True is an inherently semantic concept, thus logic systems
always have semantics. The truth tables for propositional
logic provide the semantics of its operators.
The Tarski undefinability theorem is totally refuted by
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) >>
In which system is ⊢ a logical connective?
On 1/23/2024 3:23 AM, Mikko wrote:
On 2024-01-22 18:39:44 +0000, olcott said:
On 1/22/2024 4:17 AM, Mikko wrote:
In a formal theory nothing is semantically anything.
That it the reason why formal theories get confused
and make semantic errors that are invisible to them.
As there are no semantics in a formal system there can
be no semantic errors. However, it is possible that the
intended interpretation is not a model of the system.
Then one may hope that a small change will make it useful
for its intended purpose.
Mikko
True is an inherently semantic concept,
thus logic systems
always have semantics.
The truth tables for propositional
logic provide the semantics of its operators.
The Tarski undefinability theorem is totally refuted by
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
On 1/24/2024 4:54 AM, Mikko wrote:
On 2024-01-23 19:07:32 +0000, immibis said:
On 1/23/24 19:30, olcott wrote:
On 1/23/2024 11:23 AM, immibis wrote:
On 1/23/24 18:03, olcott wrote:
On 1/23/2024 7:41 AM, immibis wrote:
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value? >>>>>>>If YOU believe that True(L,x) exists then YOU believe the Liar
Paradox has a truth value.
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
Then you believe the liar paradox has a truth value.
Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
Thus Invalid(L, LP) is TRUE.
⊢ stands for provability. True and False should be called Provable
and OppositeProvable.
Disprovable is shorter.
Mikko
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
thus Invalid(L, “this sentence is not true”) is true.
On 1/24/2024 4:54 AM, Mikko wrote:
On 2024-01-23 19:07:32 +0000, immibis said:
On 1/23/24 19:30, olcott wrote:
On 1/23/2024 11:23 AM, immibis wrote:
On 1/23/24 18:03, olcott wrote:
On 1/23/2024 7:41 AM, immibis wrote:
On 1/23/24 05:30, olcott wrote:
In other words you believe that the Liar Paradox has a truth value? >>>>>>>If YOU believe that True(L,x) exists then YOU believe the Liar
Paradox has a truth value.
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x)
Then you believe the liar paradox has a truth value.
Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
Thus Invalid(L, LP) is TRUE.
⊢ stands for provability. True and False should be called Provable
and OppositeProvable.
Disprovable is shorter.
Mikko
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
thus Invalid(L, “this sentence is not true”) is true.
On 1/25/2024 9:22 AM, immibis wrote:
On 1/25/24 16:01, olcott wrote:
The proof by contradiction begins with the false assumption
All proofs by contradiction begin with false assumptions. That's how
they work.
It superficially seems that Tarski Undefinability is a valid
proof by contradiction. Tarski assumes that a consistent and
correct True(L, x) predicate exists and derives a contradiction
when True(Tarski_theory, Liar_Paradox) cannot provide a correct
truth value.
Tarski stupidly assumes that Truth predicates must work
correctly on incorrect inputs.
If we assume that a baker can bake cakes using any ingredients
what-so-ever and they fail to bake a perfect angel food cake
using only house bricks for ingredients, then (using Tarski's
faulty reasoning) we conclude that bakers do not exist.
On 1/25/2024 11:16 AM, immibis wrote:
On 1/25/24 18:10, olcott wrote:
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate
exists.
The actual assumption is that a truth predicate exists that can
correctly determine the truth value of an expression having no truth >>>>> value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it.
It can only be written in Montague Grammar.
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
On 1/25/2024 11:02 AM, Alan Mackenzie wrote:
immibis <news@immibis.com> wrote:
On 1/25/24 16:30, Alan Mackenzie wrote:
I know it's not correct. If it were, Tarski's work on this would never >>>> have been accepted for publication, he would have become the laughing
stock of his peers, and his name would have remained unknown.
This is not a valid way to prove things.
Possibly not, but it's a valid argument to show that those who doubt the
theorem have the burden of proof. Hundreds of thousands, possibly
millions of mathematicians and computer scientists have learnt Tarski's
theorem and
by rote and simply assumed that Tarski was correct.
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.” https://plato.stanford.edu/entries/self-reference/
These people never understood that the Liar Paradox is not a truth
bearer because it has been a long standing convention to formalize self-reference (thus the self-reference of the Liar Paradox)
incorrectly.
--
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/25/2024 11:29 AM, immibis wrote:
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate
exists.
The actual assumption is that a truth predicate exists that can
correctly determine the truth value of an expression having no truth >>>>>>> value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it.
It can only be written in Montague Grammar.
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate
exists.
The actual assumption is that a truth predicate exists that can
correctly determine the truth value of an expression having no truth >>>>>> value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it.
It can only be written in Montague Grammar.
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
On 1/25/2024 12:17 PM, immibis wrote:
On 1/25/24 18:47, olcott wrote:
On 1/25/2024 11:29 AM, immibis wrote:Probably because self-reference is pathological.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate >>>>>>>>> exists.
The actual assumption is that a truth predicate exists that can >>>>>>>>> correctly determine the truth value of an expression having no >>>>>>>>> truth
value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it.
It can only be written in Montague Grammar.
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
LP := ~True(LP)
G := ~Provable(PA, G)
Are both pathological and are expressed in a formal system.
On 1/25/2024 12:09 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/25/2024 11:02 AM, Alan Mackenzie wrote:
immibis <news@immibis.com> wrote:
On 1/25/24 16:30, Alan Mackenzie wrote:
I know it's not correct. If it were, Tarski's work on this would never >>>>>> have been accepted for publication, he would have become the laughing >>>>>> stock of his peers, and his name would have remained unknown.
This is not a valid way to prove things.
Possibly not, but it's a valid argument to show that those who doubt the >>>> theorem have the burden of proof. Hundreds of thousands, possibly
millions of mathematicians and computer scientists have learnt Tarski's >>>> theorem and
by rote and simply assumed that Tarski was correct.
That just confirms your ignorance of academic life. You haven't a clue.
"By rote" is not how mathematics is taught or learnt in universities.
What is taught is a systematic understanding based on uncontrovertable
truths. Note that word "understanding".
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
These people never understood that the Liar Paradox is not a truth
bearer because it has been a long standing convention to formalize
self-reference (thus the self-reference of the Liar Paradox)
incorrectly.
"These people" understand the liar paradox perfectly.
It is not exactly
deep or difficult. Somebody who does not even understand proof by
contradiction should not be casting aspersions on distinguished and
capable academics.
That you foolishly disagree with verified facts out of
laziness proves that you are a lazy fool.
https://liarparadox.org/Tarski_247_248.pdf https://liarparadox.org/Tarski_275_276.pdf
It is a verified fact that Tarski assumes an adapted
form of the Liar Paradox on the first line of his proof.
--
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/25/2024 1:22 PM, immibis wrote:
On 1/25/24 20:21, olcott wrote:
On 1/25/2024 12:17 PM, immibis wrote:
On 1/25/24 18:47, olcott wrote:
On 1/25/2024 11:29 AM, immibis wrote:Probably because self-reference is pathological.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:It can only be written in Montague Grammar.
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth
predicate exists.
The actual assumption is that a truth predicate exists that can >>>>>>>>>>> correctly determine the truth value of an expression having >>>>>>>>>>> no truth
value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it. >>>>>>>
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
LP := ~True(LP)
G := ~Provable(PA, G)
Are both pathological and are expressed in a formal system.
Is this MTT? Then perhaps MTT is pathological.
*MTT is merely more expressive that other formal systems*
On 1/25/2024 2:37 PM, immibis wrote:
On 1/25/24 20:28, olcott wrote:
On 1/25/2024 1:22 PM, immibis wrote:
On 1/25/24 20:21, olcott wrote:
On 1/25/2024 12:17 PM, immibis wrote:
On 1/25/24 18:47, olcott wrote:
On 1/25/2024 11:29 AM, immibis wrote:Probably because self-reference is pathological.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:It can only be written in Montague Grammar.
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth >>>>>>>>>>>>> predicate exists.
The actual assumption is that a truth predicate exists that >>>>>>>>>>>>> can
correctly determine the truth value of an expression having >>>>>>>>>>>>> no truth
value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it. >>>>>>>>>
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
LP := ~True(LP)
G := ~Provable(PA, G)
Are both pathological and are expressed in a formal system.
Is this MTT? Then perhaps MTT is pathological.
*MTT is merely more expressive that other formal systems*
Because it allows you to express pathologies?
Because it correctly represents self-reference rather
that following the established convention of encoding
self-reference incorrectly.
On 1/25/2024 5:52 PM, immibis wrote:
On 1/26/24 00:20, olcott wrote:
It does not.
x := ~True(x) thus expands to ~True(~True(~True(~True(...))))
becomes
x := ~Provable(x) thus expands to ~Provable(~Provable(~Provable(...)))
Neither of them is valid in FOL/ZFC.
None-the-less Tarski specifies both of them:
"x ∉ True if and only if p"
"where the symbol 'p' represents the whole sentence x"
"(1) x ∉ Provable if and only if p"
"where the symbol 'p' represents the whole sentence x"
On 1/25/2024 7:40 PM, immibis wrote:
On 1/26/24 01:19, olcott wrote:
On 1/25/2024 5:52 PM, immibis wrote:neither one is the same as
On 1/26/24 00:20, olcott wrote:
It does not.
x := ~True(x) thus expands to ~True(~True(~True(~True(...))))
becomes
x := ~Provable(x) thus expands to ~Provable(~Provable(~Provable(...))) >>>>>
Neither of them is valid in FOL/ZFC.
None-the-less Tarski specifies both of them:
"x ∉ True if and only if p"
"where the symbol 'p' represents the whole sentence x"
"(1) x ∉ Provable if and only if p"
"where the symbol 'p' represents the whole sentence x"
x := ~True(x)
or
x := ~Provable(x)
Yes they are because:
"the symbol 'p' represents the whole sentence x"
x ∉ True if and only if p
thus the above really says
x ∉ True if and only if x
simplify syntax
x ∉ True ↔ x
swapping sides
x ↔ x ∉ True
converting syntax to predicate form
x ↔ ~True(x)
*The standard convention of encoding self-reference incorrectly*
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
*Correcting to this*
x := ~True(x)
On 1/25/2024 8:20 PM, immibis wrote:
On 1/26/24 03:03, olcott wrote:
On 1/25/2024 7:40 PM, immibis wrote:so you just add self-reference where none exists because you just feel
On 1/26/24 01:19, olcott wrote:
On 1/25/2024 5:52 PM, immibis wrote:neither one is the same as
On 1/26/24 00:20, olcott wrote:
It does not.
x := ~True(x) thus expands to ~True(~True(~True(~True(...))))
becomes
x := ~Provable(x) thus expands to
~Provable(~Provable(~Provable(...)))
Neither of them is valid in FOL/ZFC.
None-the-less Tarski specifies both of them:
"x ∉ True if and only if p"
"where the symbol 'p' represents the whole sentence x"
"(1) x ∉ Provable if and only if p"
"where the symbol 'p' represents the whole sentence x"
x := ~True(x)
or
x := ~Provable(x)
Yes they are because:
"the symbol 'p' represents the whole sentence x"
x ∉ True if and only if p
thus the above really says
x ∉ True if and only if x
simplify syntax
x ∉ True ↔ x
swapping sides
x ↔ x ∉ True
converting syntax to predicate form
x ↔ ~True(x)
*The standard convention of encoding self-reference incorrectly*
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
*Correcting to this*
x := ~True(x)
like it should be there.
"the symbol 'p' represents the whole sentence x"
Stipulates self-reference
On 1/25/2024 8:30 PM, immibis wrote:
On 1/26/24 03:27, olcott wrote:
On 1/25/2024 8:20 PM, immibis wrote:The fact that one thing references another thing does not stipulate
On 1/26/24 03:03, olcott wrote:
On 1/25/2024 7:40 PM, immibis wrote:so you just add self-reference where none exists because you just
On 1/26/24 01:19, olcott wrote:
On 1/25/2024 5:52 PM, immibis wrote:neither one is the same as
On 1/26/24 00:20, olcott wrote:
It does not.
x := ~True(x) thus expands to ~True(~True(~True(~True(...)))) >>>>>>>>> becomes
x := ~Provable(x) thus expands to
~Provable(~Provable(~Provable(...)))
Neither of them is valid in FOL/ZFC.
None-the-less Tarski specifies both of them:
"x ∉ True if and only if p"
"where the symbol 'p' represents the whole sentence x"
"(1) x ∉ Provable if and only if p"
"where the symbol 'p' represents the whole sentence x"
x := ~True(x)
or
x := ~Provable(x)
Yes they are because:
"the symbol 'p' represents the whole sentence x"
x ∉ True if and only if p
thus the above really says
x ∉ True if and only if x
simplify syntax
x ∉ True ↔ x
swapping sides
x ↔ x ∉ True
converting syntax to predicate form
x ↔ ~True(x)
*The standard convention of encoding self-reference incorrectly* >>>>> ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
*Correcting to this*
x := ~True(x)
feel like it should be there.
"the symbol 'p' represents the whole sentence x"
Stipulates self-reference
self-reference.
Of course not goofus, that fact that a thing references itself
is what make is self-reference.
I take 45 minutes composing a reply to you and you skim it in 45
seconds. Please go back and read it again and again until you get it.
On 1/25/2024 12:31 PM, Alan Mackenzie wrote:
immibis <news@immibis.com> wrote:
On 1/25/24 18:29, Alan Mackenzie wrote:
I doubt that very much. If that were a flaw in the proof, it would
have
been picked up by Tarski's reviewers before its first publication. And >>>> it would certainly have been picked up by one of the multitude of
scientists who've since verified a proof.
Please stop affirming mathematical results on the basis of authority.
Olcott is wrong because he's wrong, not because he contradicts a certain >>> other person.
You misunderstand me. That would certainly not be valid reasoning in a
mathematical journal. But to take the view that anybody, of no matter
how meagre capabilities, is to be taken seriously when they disparage
simple mathematically proven results which are universally accepted is
untenable.
If Olcott started going on about 2 + 2 != 4, would you take him
seriously? I doubt it. So why take him seriously when he refuses to
accept equally sound proven mathematics?
By doing so, you're confusing legitimate "freedom of speech" with the
notion that everybody's views are of equal value. Olcott's views are
worth far less than those of University mathematics professors.
Maybe I'm not getting my message across, but at the very least you
should accept my quoted paragraph as a good reason not to waste too much
time on Peter Olcott's ideas. They're worthless.
[ .... ]
If Foolish troll idiots used correct reasoning instead of foolish troll rhetoric they would find that there is no correct reasoning rebuttal.
On 1/25/2024 3:34 AM, Mikko wrote:
On 2024-01-24 17:32:45 +0000, olcott said:
On 1/24/2024 9:36 AM, Mikko wrote:
On 2024-01-24 15:03:25 +0000, olcott said:
On 1/24/2024 4:40 AM, Mikko wrote:
On 2024-01-21 20:15:54 +0000, olcott said:
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.
It is a sin to lie about other people. Tarski obviously unnderstood that,
as he could see an opportunity to exloit the fact.
Mikko
If Tarski understood that self-contradictory expressions
have no truth value and did not have his truth predicate
reject such expressions as invalid then Tarski was stupid.
Tarski was discussion the problem of constructing a predicate to
determine the truth of an arthmetic sentence. The liar's paradox
is not an arithmetic sentence so it is obviously invalid for his
predicate of arithmetic truth.
Mikko
Then why did he anchor his whole proof in the Liar Paradox?
The first line of his proof began with an adapted form of
the Liar Paradox. I had to carefully study his proof hundreds
of times before I noticed this.
*Tarski anchors his whole proof in the Liar Paradox*
https://liarparadox.org/Tarski_247_248.pdf
x asserts that x is not a true sentence. page 248
What x are you talking about? Is it a sentence of arithmetic
or a metalanguage sentence about arithmetic?
https://liarparadox.org/Tarski_275_276.pdf
x asserts that x is not a true sentence. page 248
From the top of page 275
is encoded as: x ∉ True if and only if p
"where the symbol 'p' represents the whole sentence x"
and transformed into the Tarski line (1)
"(1) x ∉ Provable if and only if p"
by swapping 'Tr' for True with 'Pr' for Provable.
On 1/26/2024 3:47 AM, Mikko wrote:
On 2024-01-25 16:24:09 +0000, olcott said:
On 1/25/2024 3:56 AM, Mikko wrote:
On 2024-01-24 16:22:53 +0000, olcott said:
On 1/24/2024 5:39 AM, Mikko wrote:
On 2024-01-24 03:51:39 +0000, Richard Damon said:
Remember, Prolog is limited to Prepositional logic, not even full >>>>>>> first order, and only for system with a finite domain.
The basic logical system of Prolog is Horn clauses. However, it also >>>>>> has library predicates (like assert and not and
unify_with_occurs_check)
that can break the logic system if used in a wrong place.
Mikko
unify_with_occurs_check detects cycles in the evaluation of
expressions such as LP := ~True(LP)
because it can see that this specifies
~True(~True(~True(~True(~True(...)))))
Prolog rules also permit but do no require that every unification
do the same. The consequence is that true conclusions about liar's
paradox or Quine's atom are impossible to infer.
Mikko
Not at all.
The problem is that it is conventional to encode
self-reference incorrectly.
No, it isn't. A Prolog implementation does not need to support
a self-reference. If a self reference needs be encoded then it
must be encoded so that a Prolog imiplementation does not see
it as a self-reference.
Not at all.
unify_with_occurs_check() was intentionally defined
to detect and reject
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y,
which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure. END:(Clocksin & Mellish 2003:254)
The programmer must also ensure that any
processing of a self-reference does not produce an infinite
recursion.
An encoding is not incorrect if it serves its intended purpose.
Mikko
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.” https://plato.stanford.edu/entries/self-reference/
So that when actual self-reference is encoded correctly
LP := ~True(LP)
then it can be directly seen that this expression specifies
an infinitely recursive structure:
~True(~True(~True(~True(~True(...)))))
On 1/26/2024 2:45 PM, immibis wrote:
On 1/26/24 18:09, olcott wrote:
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
This is not self-referential any more than
x = 2*√x
is self-referential
The whole article is about self-reference /self-reference/
*and shows how to encode it incorrectly*
On 1/26/2024 3:23 PM, immibis wrote:
On 1/26/24 22:05, olcott wrote:
On 1/26/2024 2:45 PM, immibis wrote:
On 1/26/24 18:09, olcott wrote:
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential >>>>> in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
This is not self-referential any more than
x = 2*√x
is self-referential
The whole article is about self-reference /self-reference/
*and shows how to encode it incorrectly*
How do you correctly encode:
x = 2*√x
When it is an assignment operator in a programming language
x = 2*√x is simply a contradiction.
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false because the LHS contradicts the RHS.
On 1/26/2024 6:31 PM, André G. Isaak wrote:
On 2024-01-26 17:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false because the LHS contradicts the RHS.
Where's the contradiction?
Both sides of the equation equal 4. How does 4 contradict 4?
André
That depends on the existential or universal quantification of x.
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does, specifically
x = 4).
André
On 1/26/2024 4:25 AM, Mikko wrote:
On 2024-01-25 20:37:32 +0000, immibis said:
On 1/25/24 20:28, olcott wrote:
On 1/25/2024 1:22 PM, immibis wrote:
On 1/25/24 20:21, olcott wrote:
On 1/25/2024 12:17 PM, immibis wrote:
On 1/25/24 18:47, olcott wrote:
On 1/25/2024 11:29 AM, immibis wrote:Probably because self-reference is pathological.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:It can only be written in Montague Grammar.
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate exists.
The actual assumption is that a truth predicate exists that can >>>>>>>>>>>>>> correctly determine the truth value of an expression having no truth
value.
Every expression has a truth value.
OK then give me the truth value of this expression:
"What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it. >>>>>>>>>>
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
LP := ~True(LP)
G := ~Provable(PA, G)
Are both pathological and are expressed in a formal system.
Is this MTT? Then perhaps MTT is pathological.
*MTT is merely more expressive that other formal systems*
Because it allows you to express pathologies?
No but because it allows to express pathologically.
Mikko
Diagonalization is a trick that can recognize that a sentence
is unprovable while having no idea why it is unprovable.
This incorrectly causes the formal system to be blamed for being
incomplete when the real issue is that the expression is incorrect.
On 1/26/2024 6:55 PM, André G. Isaak wrote:
On 2024-01-26 17:36, olcott wrote:
On 1/26/2024 6:31 PM, André G. Isaak wrote:
On 2024-01-26 17:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does, specifically >>>>>> x = 4).
André
OK, your answer was better than mine.
It is an equation that is false because the LHS contradicts the RHS.
Where's the contradiction?
Both sides of the equation equal 4. How does 4 contradict 4?
André
That depends on the existential or universal quantification of x.
If there had been a universal quantifier there (which there was not),
then it would simply have been a statement which if false.
Andre
Yes, so what is the default when no quantifier is specified?
On 1/26/2024 4:37 AM, Mikko wrote:
On 2024-01-25 19:16:02 +0000, olcott said:
On 1/25/2024 9:30 AM, Alan Mackenzie wrote:
olcott <polcott2@gmail.com> wrote:
On 1/25/2024 3:52 AM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 3:36 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 3:10 PM, Alan Mackenzie wrote:
olcott <polcott2@gmail.com> wrote:
On 1/24/2024 2:21 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 1:27 PM, Alan Mackenzie wrote:
[ .... ]
You're lying. You do not understand it [proof by contradiction]When we assume that X is possible and then prove that >>>>>>>>>>>>> this results in a contradiction then X is proven impossible.
at all. If I'm mistaken, feel free to outline it in your reply,
or give some other unambiguous indication you understand it. >>>>
So, you've got some idea. It's not "possible" and "impossible", >>>>>>>>>>>> it's true and false. But all the indications are that you don't >>>>>>>>>>>> really understand it; all the libel against mathematicians who use >>>>>>>>>>>> proof by contradiction, and failure to understand the basis of >>>>>>>>>>>> their results.
When we falsely assume that a correct and consistent truth >>>>>>>>>>>>> predicate must correctly determine the truth value of a non truth >>>>>>>>>>>>> bearer, then this false assumption derives the false conclusion >>>>>>>>>>>>> that correct and consistent truth predicate does not exist.
But here you go right off the wall into incoherent rambling.
In other words you don't know what the term truth-bearer >>>>>>>>>>> means so this seems like nonsense to you.
Where does that come from? I know full well what a truth bearer is.
I can only guess what you mean by your rambling. If my guess is >>>>>>>>>> right, you're wrong, hopelessly wrong.
*I will make it more explicit*
The fact that this predicate:
Boolean True(Formalized_English, "What time is it?")
cannot return a correct Boolean value
DOES NOT PROVE THAT A CORRECT AND CONSISTENT
TRUTH PREDICATE DOES NOT EXIST.
No, of course it doesn't. Who other than you said it does? The >>>>>>>>>> truth predicate of Tarski's theorem cannot exist. This was >>>>>>>>>> proven by contradiction, something you assert you understand. >>>>>>>>>> But given you don't accept the result, it seems your
understanding is, at best, superficial.
THAT YOU FAIL TO COMPREHEND THAT TARSKI'S LINE (1)
ASSUMES THE LIAR PARADOX AS HIS BASIS IS NO ACTUAL
REBUTTAL WHAT-SO-EVER.
You don't understand proof by contradiction after all.
Tarski was a top rate mathematician, you are not. His work has been >>>>>>>> learnt, reviewed, checked, and tested by thousands, if not millions, >>>>>>>> of capable mathematicians. It is correct.
True(L, x) was proven to not exist on the basis of Tarski's line(1) >>>>>>>>> that has been adapted from the Liar Paradox.
My understanding of the theorem's proof is that it uses the liar >>>>>>>> paradox merely as an absurdity.
Conclusively proving ....
Stop swearing! You shouldn't use words you don't understand.
.... that you never carefully studied these four pages of his proof. >>>>
https://liarparadox.org/Tarski_247_248.pdf
https://liarparadox.org/Tarski_275_276.pdf
I've never looked at his proof in my life. Unlike you, I've got other >>>>>> things to do. Also unlike you, were I to look at it, I could
understand it. I just can't be bothered. Further unlike you, I >>>>>> understand proof by contradiction, an essential part of that proof.
The proof by contradiction begins with the false assumption
that a correct and consistent truth predicate must be able
to return a correct truth value for a non-truth bearer.
No. It begins with an assumption, and shows that this assumption leads >>>> to that absurdity.
It begins with an absurdity and from this absurdity
derives a false conclusion.
The assumption that there is a method to determine whether a formula
of Peano arithmetic is true is no more absurd than the assumption that
there is a method to determine whether a formula of Abelian group theory
is true.
The conclusion inferred from this assumption is useful exacly because
it is so obviously false that one can call it absurd.
Mikko
Most other sources simply say that Tarski directly applies
his Truth() predicate to the Liar Paradox itself.
But the diagonal lemma yields a counterexample to this equivalence,
*by giving a "liar" formula S ⟺ ¬True((g(S))} holds in N* https://en.wikipedia.org/wiki/Tarski%27s_undefinability_theorem#General_form
On 1/26/2024 6:37 AM, Mikko wrote:
On 2024-01-25 16:11:17 +0000, olcott said:
On 1/25/2024 3:17 AM, Mikko wrote:
On 2024-01-24 21:00:27 +0000, olcott said:
On 1/24/2024 2:21 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 1:27 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 12:28 PM, Alan Mackenzie wrote:
In comp.theory olcott <polcott2@gmail.com> wrote:
On 1/24/2024 11:23 AM, acm@muc.de wrote:
olcott <polcott2@gmail.com> wrote:
On 1/24/2024 10:45 AM, Alan Mackenzie wrote:
olcott <polcott2@gmail.com> wrote:
On 1/24/2024 9:29 AM, acm@muc.de wrote:
olcott <polcott2@gmail.com> wrote:
On 1/24/2024 4:40 AM, Mikko wrote:
On 2024-01-21 20:15:54 +0000, olcott said:
Tarski did not understand that the Liar Paradox is not a >>>>>>>>>>>>>>>>>>> truth bearer thus cannot possibly be true or false.
It is a sin to lie about other people. Tarski obviously >>>>>>>>>>>>>>>>>> unnderstood that, as he could see an opportunity to exloit >>>>>>>>>>>>>>>>>> the fact.
Mikko
If Tarski understood that self-contradictory expressions have >>>>>>>>>>>>>>>>> no truth value and did not have his truth predicate reject >>>>>>>>>>>>>>>>> such expressions as invalid then Tarski was stupid.
That is a bit rich coming from you. You don't even understand
proof by contradiction.
The correct evaluation of the correctly formalized Liar Paradox >>>>>>>>>>>>>>> never reaches its own self-contradiction.
The Liar Paradox has a cycle in the directed graph of its >>>>>>>>>>>>>>> evaluation sentence. Few people have noticed this besides me >>>>>>>>>>>>>>> because it is the convention to formalize self-reference >>>>>>>>>>>>>>> incorrectly as explained below.
[ and so on .... ]
I don't know what that gobbledeegook means,Question: why should we take seriously anything you say about >>>>>>>>>>>>>> logic, given you don't even understand proof by contradiction? >>>>>>That you did not bother to notice that the cycle in the directed >>>>>>>>>>>>> graph of the evaluation sequence of the correct formalization of >>>>>>>>>>>>> the Liar Paradox prevents it from even reaching a contraction >>>>>>>>>>>>> *DOES NOT MEAN THAT I DO NOT UNDERSTAND PROOF BY CONTRADICTION* >>>>>>
That you cannot understand my proof that the Liar Paradox >>>>>>>>>>> is not a truth bearer ....
Don't need to. Everybody understands that the "liar paradox" isn't a
truth bearer.
And everybody here, except ignorant you, understands proof by >>>>>>>>>> contradiction.
Just the opposite.
You're lying. You do not understand it at all. If I'm mistaken, feel
free to outline it in your reply, or give some other unambiguous >>>>>>>> indication you understand it.
When we assume that X is possible and then prove that
this results in a contradiction then X is proven impossible.
So, you've got some idea. It's not "possible" and "impossible", it's >>>>>> true and false. But all the indications are that you don't really >>>>>> understand it; all the libel against mathematicians who use proof by >>>>>> contradiction, and failure to understand the basis of their results. >>>>>>
When we falsely assume that a correct and consistent truth
predicate must correctly determine the truth value of a
non truth bearer, then this false assumption derives the
false conclusion that correct and consistent truth
predicate does not exist.
But here you go right off the wall into incoherent rambling.
In other words you don't know what the term truth-bearer
means so this seems like nonsense to you.
*I will make it more explicit*
The fact that this predicate:
Boolean True(Formalized_English, "What time is it?")
cannot return a correct Boolean value
DOES NOT PROVE THAT A CORRECT AND CONSISTENT
TRUTH PREDICATE DOES NOT EXIST.
If you can't tell the page and line where an error or gap
in the proof is you can't construct a correct truth predicate.
(Someone else might if there really is an error but not you).
Mikko
*I have done that many times and you simply ignore what I say*
Line (1) of his proof on page 275 <is> an adapted form of
the Liar Paradox.
*Line (1) and Line (2) begin as directly contradictory assumptions*
(1) x ∉ True if and only if p
(2) x ∈ True if and only if p
Not true. The symbol Pr is present in (1) and absent in (2).
The symbol Tr is absent in (1) and present in (2). Therefore
there is no contraction between the two.
Mikko
They are isomorphic in structure and every reference to the Tarski Undefinability theorem directly states that it is anchored in the actual
Liar Paradox.
On 1/26/2024 6:53 AM, Mikko wrote:
On 2024-01-25 16:03:51 +0000, olcott said:
On 1/25/2024 3:08 AM, Mikko wrote:
On 2024-01-24 15:03:25 +0000, olcott said:
On 1/24/2024 4:40 AM, Mikko wrote:
On 2024-01-21 20:15:54 +0000, olcott said:
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.
It is a sin to lie about other people. Tarski obviously unnderstood that,
as he could see an opportunity to exloit the fact.
Mikko
If Tarski understood that self-contradictory expressions
have no truth value and did not have his truth predicate
reject such expressions as invalid then Tarski was stupid.
If you could show some exmples of self-contradictory arithmetic
expressions we perhaps could understand what you are trying to say.
Mikko
Tarski did not use PA in this proof:
Tarski's discussion is fairly generic. It is applicable to PA and
many other theories.
Mikko
No conventional language encodes self-reference correctly
thus No conventional language encodes the Liar Paradox
correctly. Thus No conventional language can directly
see the infinite recursive structure of the actual Liar
Paradox.
On 1/26/2024 3:47 AM, Mikko wrote:
On 2024-01-25 16:24:09 +0000, olcott said:
On 1/25/2024 3:56 AM, Mikko wrote:
On 2024-01-24 16:22:53 +0000, olcott said:
On 1/24/2024 5:39 AM, Mikko wrote:
On 2024-01-24 03:51:39 +0000, Richard Damon said:
Remember, Prolog is limited to Prepositional logic, not even full first >>>>>>> order, and only for system with a finite domain.
The basic logical system of Prolog is Horn clauses. However, it also >>>>>> has library predicates (like assert and not and unify_with_occurs_check) >>>>>> that can break the logic system if used in a wrong place.
Mikko
unify_with_occurs_check detects cycles in the evaluation of
expressions such as LP := ~True(LP)
because it can see that this specifies
~True(~True(~True(~True(~True(...)))))
Prolog rules also permit but do no require that every unification
do the same. The consequence is that true conclusions about liar's
paradox or Quine's atom are impossible to infer.
Mikko
Not at all.
The problem is that it is conventional to encode
self-reference incorrectly.
No, it isn't. A Prolog implementation does not need to support
a self-reference. If a self reference needs be encoded then it
must be encoded so that a Prolog imiplementation does not see
it as a self-reference.
Not at all.
unify_with_occurs_check() was intentionally defined
to detect and reject
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.” https://plato.stanford.edu/entries/self-reference/
On 1/26/2024 4:55 PM, immibis wrote:
On 1/26/24 22:50, olcott wrote:
On 1/26/2024 3:23 PM, immibis wrote:
On 1/26/24 22:05, olcott wrote:
On 1/26/2024 2:45 PM, immibis wrote:
On 1/26/24 18:09, olcott wrote:
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential >>>>>>> in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
This is not self-referential any more than
x = 2*√x
is self-referential
The whole article is about self-reference /self-reference/
*and shows how to encode it incorrectly*
How do you correctly encode:
x = 2*√x
When it is an assignment operator in a programming language
It isn't. How do you correctly encode it?
I am going to simply ignore any of your replies that
ask the same question that I already answered in the
part of the reply that you ignored.
x = 2*√x is simply a contradiction.
On 1/26/2024 6:55 PM, André G. Isaak wrote:
On 2024-01-26 17:36, olcott wrote:
On 1/26/2024 6:31 PM, André G. Isaak wrote:
On 2024-01-26 17:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false because the LHS contradicts the RHS.
Where's the contradiction?
Both sides of the equation equal 4. How does 4 contradict 4?
André
That depends on the existential or universal quantification of x.
If there had been a universal quantifier there (which there was not),
then it would simply have been a statement which if false.
Andre
Yes, so what is the default when no quantifier is specified?
On 1/26/2024 6:31 PM, André G. Isaak wrote:
On 2024-01-26 17:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false because the LHS contradicts the RHS.
Where's the contradiction?
Both sides of the equation equal 4. How does 4 contradict 4?
André
Although your answer was a correction to my position
it seems that your answer is wrong.
Only logic sentences have truth values open WFF do not. https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
x = 2*√x is simply a contradiction.
On 2024-01-26 17:01:58 +0000, olcott said:
Most other sources simply say that Tarski directly applies
his Truth() predicate to the Liar Paradox itself.
It does not really matter what other sources say,
only what Tarski says.
On 1/27/2024 1:39 AM, Mikko wrote:
On 2024-01-26 22:00:57 +0000, olcott said:
On 1/26/2024 3:42 PM, immibis wrote:
On 1/26/24 22:17, olcott wrote:
On 1/26/2024 2:39 PM, immibis wrote:
On 1/26/24 18:54, olcott wrote:
On 10/13/2022 11:46 AM, olcott wrote:
MIT Professor Michael Sipser has agreed that the following
verbatim paragraph is correct (he has not agreed to anything
else in this paper):
If simulating halt decider H correctly simulates its input D
until H correctly determines that its simulated D would never
stop running unless aborted then H can abort its simulation of D >>>>>>>> and correctly report that D specifies a non-halting sequence of >>>>>>>> configurations.
Professor Sipser is the best selling author of theory of
computation textbooks.
P = "simulating halt decider H correctly simulates its input D
until H correctly determines that its simulated D would never
stop running unless aborted,"
Q = "H can abort its simulation of D and correctly report that D >>>>>>> specifies a non-halting sequence of configurations."
P → Q
Correct determination is impossible.
In other words you believe that Professor Sipser
agreed to a vacuous truth. He did not do that.
Vacuous truths are true.
Not within the conventional understanding of true.
Depends on whose convetion you ask. In logic and among logically
thinking people the convetion is that truths are true, including
vacuous ones.
"It is true that all of the billion ton elephants
in the middle of my living room are rainbow colored"
Is not actually true at all when we bother to account
for false presuppositions.
For logically thinking people that is true unless in the middle
of the living room there is a billoin ton epephant that is not
rainbow colored.
Thus the whole notion of vacuous truth is inherently incorrect.
For a logically thinking people it is not incorrect. It just is
not very useful.
It only superficially seems to be correct when one hardly pays
any attention.
It often seems incorrect to those who don't pay attention.
*This also deals with false presuppositions*
Peter Olcott Feb 20, 2015, 11:38:48 AM
[The logical law of polar questions] [sci.lang]
When posed to a man whom has never been married,
the question: Have you stopped beating your wife?
Is an incorrect polar question because neither yes nor
no is a correct answer.
When that sort of questions are needed for serious purposes,
valid answer options include 'not applicable' and 'don't konw'.
Mikko
*All undecidable decision problems have that same form*
Is this sentence true or false: "This sentence is not true" ???
On 1/27/2024 6:38 AM, immibis wrote:
On 1/27/24 09:48, Mikko wrote:
On 2024-01-26 17:01:58 +0000, olcott said:
Most other sources simply say that Tarski directly applies
his Truth() predicate to the Liar Paradox itself.
It does not really matter what other sources say,
only what Tarski says.
Please stop trying to prove truth or falsehood based on a person's
authority.
When we are determining whether or not Tarski is
wrong we must go by what Tarski actually said.
On the first line of his proof he contradicts
the actual correct truth predicate
(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.
*Here is the correct way to do that*
(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.
True(L, LP) == false
True(L, ~LP) == false.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Because LP := ~True(LP) expands to ~True(~True(~True(~True(...))))
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of
the words that a formal system is incomplete if there is a sequence
of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violate the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
On 1/27/2024 11:06 AM, immibis wrote:
On 1/27/24 16:50, olcott wrote:
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of
the words that a formal system is incomplete if there is a sequence
of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violates the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
Every time you read "incomplete" just pretend it said "has an
unprovable true sentence" because that is the stipulative definition
of "incomplete".
Incomplete incorrectly blames the formal system
rather than blaming the self-contradictory input.
On 1/27/2024 11:06 AM, immibis wrote:
On 1/27/24 16:50, olcott wrote:
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of
the words that a formal system is incomplete if there is a sequence
of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violates the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
Every time you read "incomplete" just pretend it said "has an
unprovable true sentence" because that is the stipulative definition
of "incomplete".
Incomplete incorrectly blames the formal system
rather than blaming the self-contradictory input.
On 1/27/2024 11:46 AM, immibis wrote:
On 1/27/24 18:24, olcott wrote:
On 1/27/2024 11:06 AM, immibis wrote:There is no blame. It is like blaming the formal system for 1+1=2.
On 1/27/24 16:50, olcott wrote:
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of >>>>>> the words that a formal system is incomplete if there is a sequence >>>>>> of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violates the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
Every time you read "incomplete" just pretend it said "has an
unprovable true sentence" because that is the stipulative definition
of "incomplete".
Incomplete incorrectly blames the formal system
rather than blaming the self-contradictory input.
When a formal system is determined to be incomplete
on the basis that it cannot prove an incorrect
expression of language this determination is WRONG.
On 1/27/2024 12:08 PM, Richard Damon wrote:
On 1/27/24 12:24 PM, olcott wrote:
On 1/27/2024 11:06 AM, immibis wrote:
On 1/27/24 16:50, olcott wrote:
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of >>>>>> the words that a formal system is incomplete if there is a sequence >>>>>> of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violates the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
Every time you read "incomplete" just pretend it said "has an
unprovable true sentence" because that is the stipulative definition
of "incomplete".
Incomplete incorrectly blames the formal system
rather than blaming the self-contradictory input.
Except the problem is that the statement ISN'T "self-contradictory"
but just a statment that is true but unprovable
*In other words you forgot how to read the title of the thread*
LP := ~True(LP) specifies ~True(~True(~True(~True(...))))
On 1/27/2024 11:46 AM, immibis wrote:
On 1/27/24 18:24, olcott wrote:
On 1/27/2024 11:06 AM, immibis wrote:There is no blame. It is like blaming the formal system for 1+1=2.
On 1/27/24 16:50, olcott wrote:
On 1/27/2024 2:25 AM, Mikko wrote:
There is nothing incorrect in that. If follows from the meanings of >>>>>> the words that a formal system is incomplete if there is a sequence >>>>>> of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted. This violates the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
Every time you read "incomplete" just pretend it said "has an
unprovable true sentence" because that is the stipulative definition
of "incomplete".
Incomplete incorrectly blames the formal system
rather than blaming the self-contradictory input.
When a formal system is determined to be incomplete
on the basis that it cannot prove an incorrect
expression of language this determination is WRONG.
On 1/27/2024 6:31 AM, immibis wrote:
On 1/27/24 01:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does, specifically >>>> x = 4).
André
OK, your answer was better than mine.
It is an equation that is false
It's true if x=0 or x=4
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential
in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
x = 2*√x ... The variable x is of course not self-referential in a
strict sense, but mathematically it behaves like one.
No it does not behave the same way as actual self-reference.
LP := ~True(LP) expands to ~True(~True(~True(~True(...))))
LP ↔ ~True(LP) does not do that.
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does, specifically
x = 4).
André
But it cannot be used as a definition because x = 0 is also a solution.
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound. https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
On 1/27/24 09:48, Mikko wrote:
On 2024-01-26 17:01:58 +0000, olcott said:
Most other sources simply say that Tarski directly applies
his Truth() predicate to the Liar Paradox itself.
It does not really matter what other sources say,
only what Tarski says.
Please stop trying to prove truth or falsehood based on a person's
authority. Olcott is wrong because he is wrong, not because Tarski said
he's wrong.
On 1/27/2024 2:25 AM, Mikko wrote:
On 2024-01-26 17:09:39 +0000, olcott said:
On 1/26/2024 4:25 AM, Mikko wrote:
On 2024-01-25 20:37:32 +0000, immibis said:
On 1/25/24 20:28, olcott wrote:
On 1/25/2024 1:22 PM, immibis wrote:
On 1/25/24 20:21, olcott wrote:
On 1/25/2024 12:17 PM, immibis wrote:
On 1/25/24 18:47, olcott wrote:
On 1/25/2024 11:29 AM, immibis wrote:Probably because self-reference is pathological.
On 1/25/24 18:23, olcott wrote:
On 1/25/2024 11:16 AM, immibis wrote:This isn't FOL and ZFC.
On 1/25/24 18:10, olcott wrote:It can only be written in Montague Grammar.
On 1/25/2024 9:52 AM, immibis wrote:
On 1/25/24 16:45, olcott wrote:
The assumption superficially seems to be that a Truth predicate exists.
The actual assumption is that a truth predicate exists that can
correctly determine the truth value of an expression having no truth
value.
Every expression has a truth value.
OK then give me the truth value of this expression: >>>>>>>>>>>>>> "What time is it?"
If you write this as a sentence in FOL and ZFC, I will answer it. >>>>>>>>>>>>
LP := ~True(LP)
specifies: ~True(~True(~True(~True(~True(...)))))
Is LP true or false?
To the best of my knowledge there are zero formal systems
besides MTT that encode actual self-reference correctly.
LP := ~True(LP)
G := ~Provable(PA, G)
Are both pathological and are expressed in a formal system.
Is this MTT? Then perhaps MTT is pathological.
*MTT is merely more expressive that other formal systems*
Because it allows you to express pathologies?
No but because it allows to express pathologically.
Mikko
Diagonalization is a trick that can recognize that a sentence
is unprovable while having no idea why it is unprovable.
Not just recognize but prove.
The "why" part is relevant only if one wants to construct a
system where that sentence is provable. Otherwise it sufficess
to know that that sentence is unprovable and there may be
other unprovable sentences.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y,
which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure. END:(Clocksin & Mellish 2003:254)
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Diagonalization would also show that the Liar Paradox is
unprovable
and it would incorrectly blame the formal
system for being incomplete.
This incorrectly causes the formal system to be blamed for being
incomplete when the real issue is that the expression is incorrect.
There is nothing incorrect in that. If follows from the meanings of
the words that a formal system is incomplete if there is a sequence
of symbols that conforms to the systems syntax and is neither
provable nor unprovable.
We could define a dead rabbit as any ice cream cones that
has melted.
This violate the stipulated meaning of these terms.
It is better to do like what the Cyc project does and stipulate
meanings for 128-bit GUIDs.
If you need or want a complete system you may try to create one.
It is not impossible, at least as long as you don't require too
much usefulness.
Mikko
*Not at all*
*The Tarski undefinability theorem is totally refuted by*
True(L, x) ≡ (L ⊢ x) with its corresponding False(L, x) ≡ (L ⊢ ~x) Invalid(L, x) ≡ (~True(L, x) & ~False(L, x))
What was previously thought of as undecidable(L, x)
becomes Invalid(L, x) thus no longer defines Incomplete(L).
On 1/27/2024 6:38 AM, immibis wrote:
On 1/27/24 09:48, Mikko wrote:
On 2024-01-26 17:01:58 +0000, olcott said:
Most other sources simply say that Tarski directly applies
his Truth() predicate to the Liar Paradox itself.
It does not really matter what other sources say,
only what Tarski says.
Please stop trying to prove truth or falsehood based on a person's authority.
When we are determining whether or not Tarski is
wrong we must go by what Tarski actually said.
On the first line of his proof he contradicts
the actual correct truth predicate
(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.
On 1/28/2024 6:46 AM, Mikko wrote:
On 2024-01-27 21:03:34 +0000, immibis said:
On 1/27/24 16:52, olcott wrote:
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
But it cannot be used as a definition because x = 0 is also a
solution.
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
LP := ¬True(LP) has no truth value until its variables are bound
Which includes the predicate True as that is not a standard name
of any predicate. In some formalisms True is a sentence but that
meaning is not applicable here.
Mikko
That <is> the correct way to formalize the actual Liar Paradox.
The issue seems to be that LP is bound to itself thus specifies: ¬True(¬True(¬True(¬True(¬True(...)))))
Which Prolog correctly rejects.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
On 1/28/2024 6:41 AM, Mikko wrote:
On 2024-01-27 16:24:42 +0000, olcott said:
On 1/27/2024 6:31 AM, immibis wrote:
On 1/27/24 01:17, olcott wrote:
On 1/26/2024 6:08 PM, André G. Isaak wrote:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
OK, your answer was better than mine.
It is an equation that is false
It's true if x=0 or x=4
ψ ↔ ϕ⟨ψ⟩ … The sentence ψ is of course not self-referential >>>>> in a strict sense, but mathematically it behaves like one.”
https://plato.stanford.edu/entries/self-reference/
x = 2*√x ... The variable x is of course not self-referential in a
strict sense, but mathematically it behaves like one.
No it does not behave the same way as actual self-reference.
LP := ~True(LP) expands to ~True(~True(~True(~True(...))))
LP ↔ ~True(LP) does not do that.
From LP ↔ ~True(LP) can be inferred that LP ↔ ~True(~True(LP)) and
then that LP ↔ ~True(LP ↔ ~True(LP ↔ ~True(LP))) and then ...
Mikko
Possibly, yet the <defined as> operator makes this much more
explicit with its macro expansion of instances in the LHS within
the RHS.
On 1/28/2024 6:44 AM, Mikko wrote:
On 2024-01-27 15:52:22 +0000, olcott said:
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does,
specifically x = 4).
André
But it cannot be used as a definition because x = 0 is also a solution. >>>>
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
It is a logic formula that can be used where a logic formula
can be used, e.g., as a part of a sentence or definition.
Mikko
It has no truth value until its variables are bound.
On 1/28/2024 6:46 AM, Mikko wrote:
On 2024-01-27 21:03:34 +0000, immibis said:
On 1/27/24 16:52, olcott wrote:
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a
solution or it does not (in this particular case, it does, specifically >>>>>> x = 4).
André
But it cannot be used as a definition because x = 0 is also a solution. >>>>>
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
LP := ¬True(LP) has no truth value until its variables are bound
Which includes the predicate True as that is not a standard name
of any predicate. In some formalisms True is a sentence but that
meaning is not applicable here.
Mikko
That <is> the correct way to formalize the actual Liar Paradox.
Making them incapable of correctly representing the ACTUAL
self-reference of the Liar Paradox.
LP := ~True(LP)
<is> the correct way to formalize the Liar Paradox
and most languages cannot do that so I created Minimal
Type Theory.
https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF
On 1/28/2024 10:51 AM, immibis wrote:
On 1/28/24 17:08, olcott wrote:
On 1/28/2024 6:44 AM, Mikko wrote:
On 2024-01-27 15:52:22 +0000, olcott said:
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a >>>>>>> solution or it does not (in this particular case, it does,
specifically x = 4).
André
But it cannot be used as a definition because x = 0 is also a
solution.
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
It is a logic formula that can be used where a logic formula
can be used, e.g., as a part of a sentence or definition.
Mikko
It has no truth value until its variables are bound.
Does LP := ¬True(LP) have a truth value until its variables are bound?
Does: ¬True(¬True(¬True(¬True(¬True(¬True(...)))))) have a truth value? No it does not have a truth value.
On 1/28/2024 12:16 PM, Mikko wrote:
On 2024-01-28 16:04:36 +0000, olcott said:
On 1/28/2024 6:46 AM, Mikko wrote:
On 2024-01-27 21:03:34 +0000, immibis said:
On 1/27/24 16:52, olcott wrote:
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has a >>>>>>>> solution or it does not (in this particular case, it does, specifically
x = 4).
André
But it cannot be used as a definition because x = 0 is also a solution. >>>>>>>
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
LP := ¬True(LP) has no truth value until its variables are bound
Which includes the predicate True as that is not a standard name
of any predicate. In some formalisms True is a sentence but that
meaning is not applicable here.
Mikko
That <is> the correct way to formalize the actual Liar Paradox.
Not in languages that require that the expression on the right side
of := must not contain the symbol on the left side. Languages that
have the := often have that restriction.
Mikko
Making them incapable of correctly representing the ACTUAL
self-reference of the Liar Paradox.
On 1/27/2024 4:30 AM, Mikko wrote:
On 2024-01-26 17:24:34 +0000, olcott said:
On 1/26/2024 3:47 AM, Mikko wrote:
On 2024-01-25 16:24:09 +0000, olcott said:
On 1/25/2024 3:56 AM, Mikko wrote:
On 2024-01-24 16:22:53 +0000, olcott said:
On 1/24/2024 5:39 AM, Mikko wrote:
On 2024-01-24 03:51:39 +0000, Richard Damon said:
Remember, Prolog is limited to Prepositional logic, not even full first
order, and only for system with a finite domain.
The basic logical system of Prolog is Horn clauses. However, it also >>>>>>>> has library predicates (like assert and not and unify_with_occurs_check)
that can break the logic system if used in a wrong place.
Mikko
unify_with_occurs_check detects cycles in the evaluation of
expressions such as LP := ~True(LP)
because it can see that this specifies
~True(~True(~True(~True(~True(...)))))
Prolog rules also permit but do no require that every unification
do the same. The consequence is that true conclusions about liar's >>>>>> paradox or Quine's atom are impossible to infer.
Mikko
Not at all.
The problem is that it is conventional to encode
self-reference incorrectly.
No, it isn't. A Prolog implementation does not need to support
a self-reference. If a self reference needs be encoded then it
must be encoded so that a Prolog imiplementation does not see
it as a self-reference.
Not at all.
unify_with_occurs_check() was intentionally defined
to detect and reject
?- LP = not(true(LP)).
LP = not(true(LP)).
And also X = a(X) and X = [X] as well as more complicated
examples of the same. But the plain = is allowed to detect
and reject them, too. There is no promice that such structures
can be created and used for any purpose although in some
conforming implementations that may be possible.
?- unify_with_occurs_check(LP, not(true(LP))).
false.
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the
unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
According to Prolog rules, Both "yes" or "no" are permitted answers.
Mikko
BEGIN:(Clocksin & Mellish 2003:254)
Finally, a note about how Prolog matching sometimes differs from the unification used in Resolution. Most Prolog systems will allow you to
satisfy goals like:
equal(X, X).
?- equal(foo(Y), Y).
that is, they will allow you to match a term against an uninstantiated subterm of itself. In this example, foo(Y) is matched against Y,
which appears within it. As a result, Y will stand for foo(Y), which is foo(foo(Y)) (because of what Y stands for), which is foo(foo(foo(Y))),
and so on. So Y ends up standing for some kind of infinite structure. END:(Clocksin & Mellish 2003:254)
*Not for infinite terms, they abnormally terminate*
On 1/27/2024 4:20 AM, Mikko wrote:
On 2024-01-26 16:27:24 +0000, olcott said:
On 1/26/2024 6:53 AM, Mikko wrote:
On 2024-01-25 16:03:51 +0000, olcott said:
On 1/25/2024 3:08 AM, Mikko wrote:
On 2024-01-24 15:03:25 +0000, olcott said:
On 1/24/2024 4:40 AM, Mikko wrote:
On 2024-01-21 20:15:54 +0000, olcott said:
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.
It is a sin to lie about other people. Tarski obviously unnderstood that,
as he could see an opportunity to exloit the fact.
Mikko
If Tarski understood that self-contradictory expressions
have no truth value and did not have his truth predicate
reject such expressions as invalid then Tarski was stupid.
If you could show some exmples of self-contradictory arithmetic
expressions we perhaps could understand what you are trying to say. >>>>>>
Mikko
Tarski did not use PA in this proof:
Tarski's discussion is fairly generic. It is applicable to PA and
many other theories.
Mikko
No conventional language encodes self-reference correctly
thus No conventional language encodes the Liar Paradox
correctly. Thus No conventional language can directly
see the infinite recursive structure of the actual Liar
Paradox.
What do you mean by "conventional"? Is the l anguage of ordinary
formal first order logic "conventional"? Is ordinary Enlish
"conventional"?
Mikko
Every conventional formal language incorrectly formalizes the Liar
Paradox as something like this LP ↔ ~True(LP) rather than like this
LP := ~True(LP) thus the infinitely recursive structure of the Liar
Paradox is invisible when formalized incorrectly.
On 1/29/2024 1:54 AM, Mikko wrote:
On 2024-01-28 18:44:21 +0000, olcott said:
On 1/28/2024 12:16 PM, Mikko wrote:
On 2024-01-28 16:04:36 +0000, olcott said:
On 1/28/2024 6:46 AM, Mikko wrote:
On 2024-01-27 21:03:34 +0000, immibis said:
On 1/27/24 16:52, olcott wrote:Which includes the predicate True as that is not a standard name
On 1/27/2024 2:32 AM, Mikko wrote:
On 2024-01-27 00:08:34 +0000, André G. Isaak said:
On 2024-01-26 16:07, olcott wrote:
x = 2*√x is simply a contradiction.
No. It isn't. It is simply an equation. As such, it either has >>>>>>>>>> a solution or it does not (in this particular case, it does, >>>>>>>>>> specifically x = 4).
André
But it cannot be used as a definition because x = 0 is also a >>>>>>>>> solution.
Mikko
It is not a logic sentence thus has no truth value until
its variables are bound.
https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
LP := ¬True(LP) has no truth value until its variables are bound >>>>>>
of any predicate. In some formalisms True is a sentence but that
meaning is not applicable here.
Mikko
That <is> the correct way to formalize the actual Liar Paradox.
Not in languages that require that the expression on the right side
of := must not contain the symbol on the left side. Languages that
have the := often have that restriction.
Mikko
Making them incapable of correctly representing the ACTUAL
self-reference of the Liar Paradox.
And incabable of claiming that the Liar Paradox must be true or false.
Mikko
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Any system powerful enough to detect cycles in the directed
graph of an expression's evaluation sequence detects and rejects
pathological self-reference(Olcott 2004).
On 1/29/2024 8:56 AM, immibis wrote:
On 1/29/24 15:35, olcott wrote:
On 1/29/2024 1:54 AM, Mikko wrote:
?- LP = not(true(LP)).
LP = not(true(LP)).
?- unify_with_occurs_check(LP, not(true(LP))).
false.
Any system powerful enough to detect cycles in the directed
graph of an expression's evaluation sequence detects and rejects
pathological self-reference(Olcott 2004).
x=2√x
Contains a cycle.
But it is fine.
You have never responded to this point because you know it proves you
are wrong.
Other people have responded that you are wrong.
| Sysop: | Keyop |
|---|---|
| Location: | Huddersfield, West Yorkshire, UK |
| Users: | 307 |
| Nodes: | 16 (2 / 14) |
| Uptime: | 45:45:42 |
| Calls: | 6,910 |
| Files: | 12,377 |
| Messages: | 5,429,451 |