On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor false.

The liar's paradox isn't an "undecidable" instance, as "undecidable" is
about a problem that has a true or false answer that can not be computed
for every case.

This just goes back your your ignorance of what you talk about and that
your whole life appears to have been build on just committing FRAUD when
you could, as you have admitted by your admittion that you recent work
is based on changes to the core definitions of terms-of-art, while still claiming to be working on the problems that used those terms.

Sorry, you are just proving that you are ignorant of the Nature of Logic.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/9/25 4:08 PM, olcott wrote:

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor false.

The liar's paradox isn't an "undecidable" instance, as "undecidable"
is about a problem that has a true or false answer that can not be
computed for every case.

Tarski thought that is was undecidable and anchored his
whole proof in it.

Tarski's Liar Paradox from page 248
   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

Note, he says to construct the antinomy of the liar in the METALANGUAGE representing the statement x in the LANGUAGE. Thus "x" is *NOT* the
liar, but something that with the additional information of the
metalanguage can be reduced to it.

You are just showing you don't understand how formal logic works, and
how meta-systems/langauges relate to the base system/language.

Formalized as:
x ∉ True if and only if p
where the symbol 'p' represents the whole sentence x

So? x is some sentence in the language, like say Godel's G that says
there does not exist a number g such that g satisfies a particular
primative recursive relationship.

Clearly such a statement isn't what you just tried to specify it as.

He never shows the above intermediate step before
he arbitrarily swaps True for Provable on line (1)
of his proof in the first paragraph of this proof.

Because he refers to the work he did earlier that shows it to be a valid transformation in the system.

(1) x ∉ Provable and only if p

  In accordance with the first part of Th. I
  we can obtain the negation of one of the
  sentences in condition (ex) 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

Right, so look at Theorem I

The problem is you don't understand the logic it uses, in part because
you just don't understand how Formal Logic works, which is why you think
your fraud of changing the definitions was ok to do.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/9/25 6:28 PM, olcott wrote:

On 3/9/2025 4:43 PM, Richard Damon wrote:

On 3/9/25 4:08 PM, olcott wrote:

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor false.

The liar's paradox isn't an "undecidable" instance, as "undecidable"
is about a problem that has a true or false answer that can not be
computed for every case.

Tarski thought that is was undecidable and anchored his
whole proof in it.

Tarski's Liar Paradox from page 248
    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

Note, he says to construct the antinomy of the liar in the
METALANGUAGE representing the statement x in the LANGUAGE. Thus "x" is
*NOT* the liar, but something that with the additional information of
the metalanguage can be reduced to it.

"the antinomy of the liar in the metalanguage"

{the antinomy of the liar in the metalanguage}

So, you admit you don't understand what that means?

Do you understand the differene between the metalanguage and the language?

You do understand that the whole proof is about the Truth Predicate in
the LANGUAGE, not the Metalanguage.

And my understanding of his metalanguage that I have
had for several years and just refreshed from the
original source material does seem to prove that
this does mean that Tarski did anchor his whole
proof in the antinomy of the liar.

And clearly you don't understand the meaning of the metalanguage.

Note, the antinomy of the liar in the metalanguage is a result that
comes from the actual statement "x", that is in the language gets
manipulated based on new concepts from the metalanguage allowing it to
be simplifed.

Your ignorance of how that is done is NOT an error on Tarski's part,
just stupidity on yours.

Until you provide ALL OF THE REASONING PROVIDING
ALL OF THE DETAILS OF EXACTLY HOW I AM WRONG
it seems reasonable to conclude that you do not
have any of these details and only have pure bluster.

Not my job.

You need to point to the actual logical step you think Tarski got wrong,
not a conclusion you disagree with.

In particular, you need to show a claim he makes that is not supported
by what he has shown or from valid logical reasoning. Note, you can't
alter the rules of logic to be something different than what Tarski is
using, or you are just admitting that you don't know what you are
talking about.

Note, the paragraph you quote from page 248 isn't making a new claim,
but is pulling forward from his previous work, so if you disagree with
that step, you need to show how it doesn't follow from that previous
work, or the error in that previous work. Your not understanding it is
n0t finding an error in it.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 2025-03-09 17:15:13 +0000, olcott said:

Is the Liar Paradox True or False?

LP := ~True(LP)

In typical languages of formal logic that is not a syntactically valid expression.

?- LP = not(true(LP)).
LP = not(true(LP)).

Apparently you were using a Prolog implementation that does not check
whether a cyclic data structure is produced. Another Prolog implementation could say false instead.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

For this quesry the only permitted answer is false.

Its infinitely recursive structure makes it neither true nor false.

What is that "its" intended to refer to? According to Prolog rules unify_with_occurs_check(LP, not(true(LP))) is false. Accordint to
the implementation you were using LP = not(true(LP)) is true but
another implementation might say it is false. If you mean LP itself,
that is neither true nor false just lke 42 is neither true nor false.

--
Mikko

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/9/25 11:39 PM, olcott wrote:

On 3/9/2025 8:57 PM, Richard Damon wrote:

On 3/9/25 6:28 PM, olcott wrote:

On 3/9/2025 4:43 PM, Richard Damon wrote:

On 3/9/25 4:08 PM, olcott wrote:

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor false. >>>>>>>

The liar's paradox isn't an "undecidable" instance, as
"undecidable" is about a problem that has a true or false answer
that can not be computed for every case.

Tarski thought that is was undecidable and anchored his
whole proof in it.

Tarski's Liar Paradox from page 248
    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

Note, he says to construct the antinomy of the liar in the
METALANGUAGE representing the statement x in the LANGUAGE. Thus "x"
is *NOT* the liar, but something that with the additional
information of the metalanguage can be reduced to it.

"the antinomy of the liar in the metalanguage"
<is>
{the antinomy of the liar in the metalanguage}

So, you admit you don't understand what that means?

Do you understand the differene between the metalanguage and the
language?

You do understand that the whole proof is about the Truth Predicate in
the LANGUAGE, not the Metalanguage.

And my understanding of his metalanguage that I have
had for several years and just refreshed from the
original source material does seem to prove that
this does mean that Tarski did anchor his whole
proof in the antinomy of the liar.

And clearly you don't understand the meaning of the metalanguage.

Note, the antinomy of the liar in the metalanguage is a result that
comes from the actual statement "x", that is in the language gets
manipulated based on new concepts from the metalanguage allowing it to
be simplifed.

That does not really show any depth of understanding.
You might have greater depth, yet did not show it yet.

No, your reply, by not addressing *ANY* of

Your ignorance of how that is done is NOT an error on Tarski's part,
just stupidity on yours.

Yet you never said how it should be done, thus I
have no way to tell what you say is not pure bluster.

Maybe because what you want to define can't be.

Tarski shows how to derive that part in the earlier work. It is clear
that you just don't have the brains to understand that discussion, and
it isn't my job to educate you on that, particularly when you have
declared that you idea of logic fundamentally disagrees with the actual
rules of logic, so you fundamentally don't understand how to use logic.

That you refer to my stupidity yet fail to point out any
mistake seems to be strong evidence that you are clueless.

Sure I have pointed out your error. You are just too stupid to recognize
the.

Until you provide ALL OF THE REASONING PROVIDING
ALL OF THE DETAILS OF EXACTLY HOW I AM WRONG
it seems reasonable to conclude that you do not
have any of these details and only have pure bluster.

Not my job.

You need to point to the actual logical step you think Tarski got
wrong, not a conclusion you disagree with.

Yu failure to understand what i said is not my mistake,

I.E. your claim is that you don't understand the error pointed out to
you means the error wasn't pointed out to you.

Part of your problem is you create a world of strawmen as you start with
the fraud that claim you get to redefine the basic words of the logic
system, which you don't.

A Basic property of logic is that you can't prove something if your
premises aren't true.

In particular, you need to show a claim he makes that is not supported
by what he has shown or from valid logical reasoning. Note, you can't
alter the rules of logic to be something different than what Tarski is
using, or you are just admitting that you don't know what you are
talking about.

LP := ~True(LP)  DOES SPECIFY INFINITE RECURSION.

Yex, but isn't the way to express the statement "x"

Thus, your agruments that LP isn't validly defined is just a strawman.

Note, the paragraph you quote from page 248 isn't making a new claim,
but is pulling forward from his previous work, so if you disagree with
that step, you need to show how it doesn't follow from that previous
work, or the error in that previous work. Your not understanding it is
n0t finding an error in it.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/10/25 11:51 AM, olcott wrote:

On 3/10/2025 6:04 AM, Richard Damon wrote:

On 3/9/25 11:39 PM, olcott wrote:

On 3/9/2025 8:57 PM, Richard Damon wrote:

On 3/9/25 6:28 PM, olcott wrote:

On 3/9/2025 4:43 PM, Richard Damon wrote:

On 3/9/25 4:08 PM, olcott wrote:

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor >>>>>>>>> false.

The liar's paradox isn't an "undecidable" instance, as
"undecidable" is about a problem that has a true or false answer >>>>>>>> that can not be computed for every case.

Tarski thought that is was undecidable and anchored his
whole proof in it.

Tarski's Liar Paradox from page 248
    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

Note, he says to construct the antinomy of the liar in the
METALANGUAGE representing the statement x in the LANGUAGE. Thus
"x" is *NOT* the liar, but something that with the additional
information of the metalanguage can be reduced to it.

"the antinomy of the liar in the metalanguage"
<is>
{the antinomy of the liar in the metalanguage}

So, you admit you don't understand what that means?

Do you understand the differene between the metalanguage and the
language?

You do understand that the whole proof is about the Truth Predicate
in the LANGUAGE, not the Metalanguage.

And my understanding of his metalanguage that I have
had for several years and just refreshed from the
original source material does seem to prove that
this does mean that Tarski did anchor his whole
proof in the antinomy of the liar.

And clearly you don't understand the meaning of the metalanguage.

Note, the antinomy of the liar in the metalanguage is a result that
comes from the actual statement "x", that is in the language gets
manipulated based on new concepts from the metalanguage allowing it
to be simplifed.

That does not really show any depth of understanding.
You might have greater depth, yet did not show it yet.

No, your reply, by not addressing *ANY* of

Your ignorance of how that is done is NOT an error on Tarski's part,
just stupidity on yours.

Yet you never said how it should be done, thus I
have no way to tell what you say is not pure bluster.

Maybe because what you want to define can't be.

Tarski shows how to derive that part in the earlier work. It is clear
that you just don't have the brains to understand that discussion, and
it isn't my job to educate you on that, particularly when you have
declared that you idea of logic fundamentally disagrees with the
actual rules of logic, so you fundamentally don't understand how to
use logic.

That you refer to my stupidity yet fail to point out any
mistake seems to be strong evidence that you are clueless.

Sure I have pointed out your error. You are just too stupid to
recognize the.

Until you provide ALL OF THE REASONING PROVIDING
ALL OF THE DETAILS OF EXACTLY HOW I AM WRONG
it seems reasonable to conclude that you do not
have any of these details and only have pure bluster.

Not my job.

You need to point to the actual logical step you think Tarski got
wrong, not a conclusion you disagree with.

Yu failure to understand what i said is not my mistake,

I.E. your claim is that you don't understand the error pointed out to
you means the error wasn't pointed out to you.

You did not point any the details of any error
the most that you did is state your opinion
that I made some mistake somewhere. Even a bot
as stupid as the original bot Eliza could do that.

http://en.wikipedia.org/wiki/ELIZA

I pointed out that your error was not to point out an actual error, but
just disagreeing with a conclusion.

Thus, you are showing that you are just too stupid to know what you are
talking about.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/10/25 9:45 PM, olcott wrote:

On 3/10/2025 5:45 PM, Richard Damon wrote:

On 3/9/25 11:39 PM, olcott wrote:

On 3/9/2025 8:57 PM, Richard Damon wrote:

On 3/9/25 6:28 PM, olcott wrote:

On 3/9/2025 4:43 PM, Richard Damon wrote:

On 3/9/25 4:08 PM, olcott wrote:

On 3/9/2025 2:24 PM, Richard Damon wrote:

On 3/9/25 1:15 PM, olcott wrote:

Is the Liar Paradox True or False?

LP := ~True(LP)

?- LP = not(true(LP)).
LP = not(true(LP)).

?- unify_with_occurs_check(LP, not(true(LP))).
false.

Its infinitely recursive structure makes it neither true nor >>>>>>>>> false.

The liar's paradox isn't an "undecidable" instance, as
"undecidable" is about a problem that has a true or false answer >>>>>>>> that can not be computed for every case.

Tarski thought that is was undecidable and anchored his
whole proof in it.

Tarski's Liar Paradox from page 248
    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

Note, he says to construct the antinomy of the liar in the
METALANGUAGE representing the statement x in the LANGUAGE. Thus
"x" is *NOT* the liar, but something that with the additional
information of the metalanguage can be reduced to it.

"the antinomy of the liar in the metalanguage"
<is>
{the antinomy of the liar in the metalanguage}

So, you admit you don't understand what that means?

Do you understand the differene between the metalanguage and the
language?

You do understand that the whole proof is about the Truth Predicate
in the LANGUAGE, not the Metalanguage.

And my understanding of his metalanguage that I have
had for several years and just refreshed from the
original source material does seem to prove that
this does mean that Tarski did anchor his whole
proof in the antinomy of the liar.

And clearly you don't understand the meaning of the metalanguage.

Note, the antinomy of the liar in the metalanguage is a result that
comes from the actual statement "x", that is in the language gets
manipulated based on new concepts from the metalanguage allowing it
to be simplifed.

That does not really show any depth of understanding.
You might have greater depth, yet did not show it yet.

But showing depth isn't my job, as it doesn't require depth to point
out your error.

Your ignorance of how that is done is NOT an error on Tarski's part,
just stupidity on yours.

Yet you never said how it should be done, thus I
have no way to tell what you say is not pure bluster.

Why should I try to show an error in Tarski's argument, I think it is
sound.

YOU are the one claiming he is wrong, so YOU have the burden of proof
to show that.

That you refer to my stupidity yet fail to point out any
mistake seems to be strong evidence that you are clueless.

But I have, you are just too stupid to understand it.

AS I have said, the statement where you say Tarski is making a bad
assumption, isn't a statement of assumption, but a pulling forward of
a previous result, which you just fail to even try to address, or even
indicate you understand what he is trying to say.

Is seems the problem is he is using theory beyond your ability to
understand, so you just assume he is wrong, which is just invalid logic,

Until you provide ALL OF THE REASONING PROVIDING
ALL OF THE DETAILS OF EXACTLY HOW I AM WRONG
it seems reasonable to conclude that you do not
have any of these details and only have pure bluster.

Not my job.

You need to point to the actual logical step you think Tarski got
wrong, not a conclusion you disagree with.

Yu failure to understand what i said is not my mistake,

I didn't say I didn't understand what you said, I was pointing out
that you never pointed out an actual error in logic, just said the
results were illogical by your understand and thus you reject it.

That isn't how logic works, and just shows your ignorance of the field.

In particular, you need to show a claim he makes that is not
supported by what he has shown or from valid logical reasoning.
Note, you can't alter the rules of logic to be something different
than what Tarski is using, or you are just admitting that you don't
know what you are talking about.

LP := ~True(LP)  DOES SPECIFY INFINITE RECURSION.

WHich is irrelevent, as that isn't the statement in view, only what
could be shown to be a meaning of the actual statement.

The Liar Paradox PROPERLY FORMALIZED <is> Infinitely recursive
thus semantically incorrect.

But is irrelevent to your arguement.

"It would then be possible to reconstruct the antinomy of the liar
 in the metalanguage, by forming in the language itself a sentence"

Right, the "Liar" is in the METALANGUAGE, not the LANGUAGE where the
predicate is defined.

You are just showing you don't understand the concept of Metalanguage.

Thus anchoring his whole proof in the Liar Paradox even if
you do not understand the term "metalanguage" well enough
to know this.

Yes, there is a connection to the liar's paradox, and that is that he
shows that the presumed existance of a Truth Predicate forces the logic
system to have to resolve the liar's paradox.

Since that statement was shown to be a valid statement under just the
added assumption that a Truth Predicate Existed,

NOT AT ALL.
We assume that True(X) exists and X = "a box of rocks"
that does not  mean that True() does not exist. It means
that we must reject all Not_Truth_Bearer(X).

And thus you assume incorrectly.

Tarski shows that if True(x) is defined, then we get a statement which
can be reduced to:

x is true only if x is not true

must be a true statement.

Sorry, until you show you understand where that came from, you are just admitting to being too stupid to understand the proof, and thus can not
refute it,

He didn't pull just some garbage sentence out of the hat, but was able
to show that you can carefully construct a sentence that, in the
metalanguage, reduces to the liar, but also must have the same value as
the original sentence had in the language.

That this is beyond you don't make it wrong, it make YOU wrong for
objecting to something you do not understand, and you prove your
stupidity by trying to make that claim.

Thus, we must reject the assumption of the existance of the predicate
True(x) or we must admit our system is inconsistant.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 2025-03-10 15:36:28 +0000, olcott said:

On 3/10/2025 4:48 AM, Mikko wrote:

On 2025-03-09 17:15:13 +0000, olcott said:

Is the Liar Paradox True or False?

LP := ~True(LP)

In typical languages of formal logic that is not a syntactically valid
expression.

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web page?
Without a pointer to it there is no point to mention it. Of course one
can create a language that can express a self reference but why would
one?

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal language. Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

Here is how this is typically done in formal systems

2.4 Diagonalization, or, “Self-reference” https://plato.stanford.edu/entries/goedel-incompleteness/#DiaSelRef

Diagonalixation is not what is "typically" done. It is done when
it is useful.

LP := ~True(LP) is exactly self-reference without the
convoluted mess of the The Diagonalization Lemma.

Only in languages that allow the expression. Typical formal languages
either don't have the symbo ":=" or restrict its use so that the
symbol on the left side cannot be used on the right side. In those
languages the expression LP := ~True(LP) does not mean anything.

The other advantage of Minimal Type Theory is that

It does not make sense to say "The other advantage" when you haven't
already identified one. And how do you know there is no third
advantage?

it outputs a directed graph of the evaluation sequence
explicitly showing any cycles that prove the expression
is invalid in the exact same way that

?- unify_with_occurs_check(LP, not(true(LP))).
proves that LP = not(true(LP)). has a cycle in its
evaluation sequence.

The library predicate unify_with_occurs_check/2 gives the same result
when asked "unify_with_occurs_check(1, 2)". Is there a cycle in the
evaluation sequence of "1 = 2"?

?- LP = not(true(LP)).
LP = not(true(LP)).

Apparently you were using a Prolog implementation that does not check
whether a cyclic data structure is produced.

In other words you can see the infinite structure of:
?- LP = not(true(LP)).

Yes, but the unification algorithm of a typical Prolog implementation
creates it without seeing it.

Not checking for cycles This is the default because
checking for cycles is too costly.

And rarely useful.

Another Prolog implementation
could say false instead.

?- unify_with_occurs_check(LP, not(true(LP))).
false.

For this quesry the only permitted answer is false.

Proving a cycle in the evaluation sequence of ?- LP = not(true(LP)).

Only if there is a cycle in the evaluation sequence of 1 = 2.

Its infinitely recursive structure makes it neither true nor false.

What is that "its" intended to refer to? According to Prolog rules
unify_with_occurs_check(LP, not(true(LP))) is false.

Proving that ?- LP = not(true(LP)). is infinitely recursive.

There is nothing infinite there. Everything that can be in a computer's
memory is finite and everthinng a computer does is done in finite time.

--
Mikko

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web page?
Without a pointer to it there is no point to mention it. Of course one
can create a language that can express a self reference but why would
one?

https://www.researchgate.net/publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must be expressly stated in Minimal Type Theory" but the syntax allows untyped quantification.

https://www.researchgate.net/publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the syntax
says that := is used.

None of the articles defines what is a valid proof in Minimal Type Theory.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.

Until we do this we get confused into believing
that such expressions are in any way undecidable.

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal language.
Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

--
Mikko

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web page? >>>> Without a pointer to it there is no point to mention it. Of course one >>>> can create a language that can express a self reference but why would
one?

https://www.researchgate.net/
publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/
publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must be
expressly stated in Minimal Type Theory" but the syntax allows untyped
quantification.

https://www.researchgate.net/
publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the syntax
says that := is used.

None of the articles defines what is a valid proof in Minimal Type
Theory.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.

Until we do this we get confused into believing
that such expressions are in any way undecidable.

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal
language.
Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

LP := ~True(LP) obtains its entire semantics from the expression.

But none of your arguments have talked about an expression that derives
itself from that expression

Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

But the p that can be developed as a statement in the languaged, based
on the idea in the metalanguge that must be true if and only if it is
false, doesn't.

Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy. https://en.wikipedia.org/wiki/Ontology_(information_science)

Right, like Godel's expression G specifically derives its semantics from
the natured of the system F and the mathematics the system F creates.
And, in the meta we can construct a mathematical statement in F, whose
truth is the direct opposite of its provability, and thus must be True
and Unprovable, as it can't be False but Provably True.

This language seems to be beyond what you can understand, so you just
make up lies to cover your ignorance.

of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.

WHich is irrelevent here, as Formal systems don't have that problem.

Your problem

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/14/25 3:01 PM, olcott wrote:

On 3/14/2025 1:42 PM, Richard Damon wrote:

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web
page?
Without a pointer to it there is no point to mention it. Of course >>>>>> one
can create a language that can express a self reference but why would >>>>>> one?

https://www.researchgate.net/
publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/
publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must be >>>> expressly stated in Minimal Type Theory" but the syntax allows untyped >>>> quantification.

https://www.researchgate.net/
publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the syntax
says that := is used.

None of the articles defines what is a valid proof in Minimal Type
Theory.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.

Until we do this we get confused into believing
that such expressions are in any way undecidable.

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal
language.
Sometimes some symbols and expressions are interpreted to represent >>>>>> themselves or other symbols or expressions. For example, the symbol 0 >>>>>> of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

LP := ~True(LP) obtains its entire semantics from the expression.

But none of your arguments have talked about an expression that
derives itself from that expression

Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

But the p that can be developed as a statement in the languaged, based
on the idea in the metalanguge that must be true if and only if it is
false, doesn't.

Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)

Right, like Godel's expression G specifically derives its semantics
from the natured of the system F and the mathematics the system F
creates. And, in the meta we can construct a mathematical statement in
F, whose truth is the direct opposite of its provability, and thus
must be True and Unprovable, as it can't be False but Provably True.

This language seems to be beyond what you can understand, so you just
make up lies to cover your ignorance.

of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.

WHich is irrelevent here, as Formal systems don't have that problem.

Your problem

In my type theory based system there is no need for
any separate language and meta-language.

Rudolf Carnap meaning postulates are arranged in an
inheritance hierarchy where each unique sense meaning
is assigned its own GUID.

The language is something like Montague Grammar.
LP := ~True(LP) is rejected as semantically incorrect.

but the existing systens aren't built on your "Type Theory" so you need
to show that it works in THOSE systems to use it,

I guess you are just admitting that you don't understand what you are
talking about, and your "logic" assumes you can just make up crap and
call it true,

Sorry, you are just proving you don't understand how logic work, and
nobody should take anything you say seriously.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 2025-03-14 14:27:24 +0000, olcott said:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web page? >>>> Without a pointer to it there is no point to mention it. Of course one >>>> can create a language that can express a self reference but why would
one?

https://www.researchgate.net/ publication/315367846_Minimal_Type_Theory_MTT >>

Does not define any theory.

https://www.researchgate.net/
publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must be
expressly stated in Minimal Type Theory" but the syntax allows untyped
quantification.

https://www.researchgate.net/
publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the syntax
says that := is used.

None of the articles defines what is a valid proof in Minimal Type Theory.

No further discussion about anything above.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.

Until we do this we get confused into believing
that such expressions are in any way undecidable.

Apparently this cannot be expressed concisely and correctly in
any formal logic system.

A self reference cannot be expressed in an uninterpreted formal language. >>>> Sometimes some symbols and expressions are interpreted to represent
themselves or other symbols or expressions. For example, the symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term
S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

LP := ~True(LP) obtains its entire semantics from the expression.

As otherwies is not specified it is reasonable to assume that tne
meanings of :=, ~, (, and ) are as usually. The meaning and even
the syntactic nature of True is something unusual that is not
specified. The usual interpretation of := makes the meaning of
LP the same as the meaning of ~True(LP) but leaves both otherwise
unspecified.

Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

An intepretation may assign meanings to cyclic structures. For example,
there is a similar sycle in x = 6 - x but the expression has a well
defined arithmetic meaning.

Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy. https://en.wikipedia.org/wiki/Ontology_(information_science)

of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.

--
Mikko

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

On 3/14/25 11:54 PM, olcott wrote:

On 3/14/2025 8:57 PM, Richard Damon wrote:

On 3/14/25 3:01 PM, olcott wrote:

On 3/14/2025 1:42 PM, Richard Damon wrote:

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference
can be expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web >>>>>>>> page?
Without a pointer to it there is no point to mention it. Of
course one
can create a language that can express a self reference but why >>>>>>>> would
one?

https://www.researchgate.net/
publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/
publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types
must be
expressly stated in Minimal Type Theory" but the syntax allows
untyped
quantification.

https://www.researchgate.net/
publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the syntax >>>>>> says that := is used.

None of the articles defines what is a valid proof in Minimal Type >>>>>> Theory.

We need such a language so that we don't stupidly
fail to understands how this can convert expressions
of language into non-truth-bearers having no truth value.

Until we do this we get confused into believing
that such expressions are in any way undecidable.

Apparently this cannot be expressed concisely and correctly in >>>>>>>>> any formal logic system.

A self reference cannot be expressed in an uninterpreted formal >>>>>>>> language.
Sometimes some symbols and expressions are interpreted to represent >>>>>>>> themselves or other symbols or expressions. For example, the
symbol 0
of arthmetic can be interpreted to mean the symbol 0 and the term >>>>>>>> S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

LP := ~True(LP) obtains its entire semantics from the expression.

But none of your arguments have talked about an expression that
derives itself from that expression

Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything
else: ~True(~True(~True(~True(~True(~True(...))))))

But the p that can be developed as a statement in the languaged,
based on the idea in the metalanguge that must be true if and only
if it is false, doesn't.

Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)

Right, like Godel's expression G specifically derives its semantics
from the natured of the system F and the mathematics the system F
creates. And, in the meta we can construct a mathematical statement
in F, whose truth is the direct opposite of its provability, and
thus must be True and Unprovable, as it can't be False but Provably
True.

This language seems to be beyond what you can understand, so you
just make up lies to cover your ignorance.

of the set of general knowledge of the world encoded as
Rudolf Carnap meaning postulates using something like Montague
Grammar. Each unique sense meaning has its own GUID.

WHich is irrelevent here, as Formal systems don't have that problem.

Your problem

In my type theory based system there is no need for
any separate language and meta-language.

Rudolf Carnap meaning postulates are arranged in an
inheritance hierarchy where each unique sense meaning
is assigned its own GUID.

The language is something like Montague Grammar.
LP := ~True(LP) is rejected as semantically incorrect.

but the existing systens aren't built on your "Type Theory" so you
need to show that it works in THOSE systems to use it,

Discard all inferior systems.

NOT A VALID OPERATION.

Sorry, but you are just proving you don't understand what you are talkig
about.

"Inferior" can't be precisely defined in this context.

I guess you are just admitting that you don't understand what you are
talking about, and your "logic" assumes you can just make up crap and
call it true,

We axiomatize all the basic facts of the world (facts
that cannot be derived on the basis of other facts).
Then we plug everything else into an inheritance hierarchy
knowledge ontology.

But what about contradictory "facts"? Things that define differents
systems of current logic, thinks like two parrallel lines will never
meet (Plane Gemoetry) vs Two non-conincident lines will allways have two
points of intersection (Spherical Geometry).

Anything that cannot be derived by applying Truth preserving
operations to these basic facts is either untrue or unknown.

And what about things we can't know if we can know?

This gives us a True() predicate that always works except
for unknowns. It certainty does not get totally confused
by self-contradictory expressions. These simply cannot be
derived by applying truth preserving operations to basic facts.

No, it doesn't give one, as it has been shown by Godel and Tarski and
many others, that if you system of logic has enough axioms to create a
system which has the full power of Natural Numbers, which by your
description, yours will, it is possible to derive via the use of a
meta-system, (which is created by a set of valid assumption of
possiblities, a major part of which is assigning a number to every one
of the finite number of axioms and basic symbols of the system) we can construct a statement whose truth value is the opposite of its
provability, and thus must be true but unprovable in the basic system.

You can not bring all these axiom numbering axioms into the original
system, as then you end you with an infinite number of axioms, as for
every axiom you number, you created a new axiom to assign that value.

Under this condition, there are statements that the Truth Predicate can
not answer, as they are truth predicate contradictory.

The only way out is to make the system not able to handle all the
properties of the Natural Numbers, which thus makes it clearly inferior
to the existing system.

Sorry, you are just showing yourself to not really understand what you
are talking about, and that you are too stupid to realize this.

Sorry, you are just proving you don't understand how logic work, and
nobody should take anything you say seriously.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)

Am Fri, 14 Mar 2025 22:54:51 -0500 schrieb olcott:

On 3/14/2025 8:57 PM, Richard Damon wrote:

On 3/14/25 3:01 PM, olcott wrote:

On 3/14/2025 1:42 PM, Richard Damon wrote:

On 3/14/25 10:27 AM, olcott wrote:

On 3/13/2025 6:08 AM, Mikko wrote:

On 2025-03-11 23:26:28 +0000, olcott said:

On 3/11/2025 6:15 AM, Mikko wrote:

On 2025-03-10 15:36:28 +0000, olcott said:

I created Minimal Type Theory such that self-reference can be >>>>>>>>> expressed concisely and correctly.

Have you pbulished that "Minimal Type Theory" or put it to a web >>>>>>>> page?
Without a pointer to it there is no point to mention it. Of
course one can create a language that can express a self
reference but why would one?

https://www.researchgate.net/
publication/315367846_Minimal_Type_Theory_MTT

Does not define any theory.

https://www.researchgate.net/
publication/331859461_Minimal_Type_Theory_YACC_BNF

The article 315367846_Minimal_Type_Theory_MTT says that "Types must >>>>>> be expressly stated in Minimal Type Theory" but the syntax allows
untyped quantification.

https://www.researchgate.net/
publication/317953772_Provability_with_Minimal_Type_Theory

This article uses @ as definition article but a comment in the
syntax says that := is used.
None of the articles defines what is a valid proof in Minimal Type >>>>>> Theory.

We need such a language so that we don't stupidly fail to
understands how this can convert expressions of language into
non-truth-bearers having no truth value.
Until we do this we get confused into believing that such
expressions are in any way undecidable.

So is the Liar sentence false or not?

Apparently this cannot be expressed concisely and correctly in >>>>>>>>> any formal logic system.

A self reference cannot be expressed in an uninterpreted formal >>>>>>>> language.
Sometimes some symbols and expressions are interpreted to
represent themselves or other symbols or expressions. For
example, the symbol 0 of arthmetic can be interpreted to mean the >>>>>>>> symbol 0 and the term S0 the sqence of symbols S and 0.

LP := ~True(LP)
has all of its semantics encoded in its syntax, thus no
interpretation required.

Without decoding no semantics can be extracted from the syntax.

LP := ~True(LP) obtains its entire semantics from the expression.

But none of your arguments have talked about an expression that
derives itself from that expression

Because of the cycle in the directed graph of its evaluation
sequence LP cannot derive its semantic meaning from anything else:
~True(~True(~True(~True(~True(~True(...))))))

But the p that can be developed as a statement in the languaged,
based on the idea in the metalanguge that must be true if and only if
it is false, doesn't.

Normally expressions derive their semantics from a knowledge
ontology inheritance hierarchy.
https://en.wikipedia.org/wiki/Ontology_(information_science)

Right, like Godel's expression G specifically derives its semantics
from the natured of the system F and the mathematics the system F
creates. And, in the meta we can construct a mathematical statement
in F, whose truth is the direct opposite of its provability, and thus
must be True and Unprovable, as it can't be False but Provably True.

of the set of general knowledge of the world encoded as Rudolf
Carnap meaning postulates using something like Montague Grammar.
Each unique sense meaning has its own GUID.

WHich is irrelevent here, as Formal systems don't have that problem.
Your problem

In my type theory based system there is no need for any separate
language and meta-language.

*Need*? You can always construct a metalanguage.

Rudolf Carnap meaning postulates are arranged in an inheritance
hierarchy where each unique sense meaning is assigned its own GUID.
The language is something like Montague Grammar.
LP := ~True(LP) is rejected as semantically incorrect.

but the existing systens aren't built on your "Type Theory" so you need
to show that it works in THOSE systems to use it,

Discard all inferior systems.

I guess you are just admitting that you don't understand what you are
talking about, and your "logic" assumes you can just make up crap and
call it true,

We axiomatize all the basic facts of the world (facts that cannot be
derived on the basis of other facts).
Then we plug everything else into an inheritance hierarchy knowledge ontology.
Anything that cannot be derived by applying Truth preserving operations
to these basic facts is either untrue or unknown.
This gives us a True() predicate that always works except for unknowns.

Wonderful. So not always.

It certainty does not get totally confused by self-contradictory
expressions. These simply cannot be derived by applying truth preserving operations to basic facts.

Yeah, it can't decide their truth value.

--
Am Sat, 20 Jul 2024 12:35:31 +0000 schrieb WM in sci.math:
It is not guaranteed that n+1 exists for every n.

--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)