Linz Ĥ applied to ⟨Ĥ⟩ is the self-contradictory form of Olcott Ȟ applied to ⟨Ȟ⟩

[olcott]

I am merely using different notational conventions that are easier to
understand because they are more conventional. Linz uses Wm as the
finite string Turing machine description of some arbitrary machine M.

// *Linz Turing machine H --- M applied to w*
// --- Does M halt on w?
H.q0 Wm w ⊢* H.qy // M applied to w halts
H.q0 Wm w ⊢* H.qn // M applied to w does not halt

// *Linz Turing machine H --- M applied to w* (different encoding)
// --- Does M halt on w?
H.q0 ⟨M⟩ w ⊢* H.qy // M applied to w halts
H.q0 ⟨M⟩ w ⊢* H.qn // M applied to w does not halt

// *Linz Turing machine H --- M applied to* ⟨M⟩
// --- Does M halt on ⟨M⟩ ?
H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qy // M applied to ⟨M⟩ halts
H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qn // M applied to ⟨M⟩ does not halt

I am applying the Linz H' and Linz Ĥ in reverse order first transforming
H into Olcott Ȟ as the one parameter version of Linz H where a machine
is applied to its own Turing machine description.

embedded_H ⟨M⟩ ⟨M⟩ means H.q0 ⟨M⟩ ⟨M⟩ shown above.

// *Olcott Turing machine Ȟ --- Ȟ applied to* ⟨M⟩
// --- Does M halt on its own Turing Machine Description?
Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qy // M applied to ⟨M⟩ halts
Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qn // M applied to ⟨M⟩ does not halt

// *Olcott Turing machine Ȟ --- Ȟ applied to* ⟨Ȟ⟩
// --- Do you halt on your own Turing Machine Description?
Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qy // Ȟ applied to ⟨Ȟ⟩ halts
Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qn // Ȟ applied to ⟨Ȟ⟩ does not halt
Ȟ applied to ⟨Ȟ⟩ simply correctly transitions to Ĥ.qy

Linz Turing machine Turing machine Ĥ applied to ⟨Ĥ⟩ is the self-
contradictory form of Olcott Turing machine Ȟ applied to ⟨Ȟ⟩

// *Linz Turing machine Ĥ --- Ĥ applied to* ⟨Ĥ⟩
// --- Do you halt on your own Turing Machine Description?
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn // Ĥ applied to ⟨Ĥ⟩ does not halt
Ĥ applied to ⟨Ĥ⟩ cannot correctly transition to Ĥ.qy or Ĥ.qn
because Ĥ applied to ⟨Ĥ⟩ is self contradictory.

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

[Richard Damon]

On 2/16/24 12:22 PM, olcott wrote:
> I am merely using different notational conventions that are easier to
> understand because they are more conventional. Linz uses Wm as the
> finite string Turing machine description of some arbitrary machine M.
>
> // *Linz Turing machine H --- M applied to w*
> // --- Does M halt on w?
> H.q0 Wm w ⊢* H.qy // M applied to w halts
> H.q0 Wm w ⊢* H.qn // M applied to w does not halt
>
> // *Linz Turing machine H --- M applied to w* (different encoding)
> // --- Does M halt on w?
> H.q0 ⟨M⟩ w ⊢* H.qy // M applied to w halts
> H.q0 ⟨M⟩ w ⊢* H.qn // M applied to w does not halt
>
> // *Linz Turing machine H --- M applied to* ⟨M⟩
> // --- Does M halt on ⟨M⟩ ?
> H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qy // M applied to ⟨M⟩ halts
> H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qn // M applied to ⟨M⟩ does not halt
>
> I am applying the Linz H' and Linz Ĥ in reverse order first transforming
> H into Olcott Ȟ as the one parameter version of Linz H where a machine
> is applied to its own Turing machine description.

Which is something you have never said before.

>
> embedded_H ⟨M⟩ ⟨M⟩ means H.q0 ⟨M⟩ ⟨M⟩ shown above.

And why can't you just say H.q0 ⟨M⟩ ⟨M⟩ instead of embedded_H ⟨M⟩ ⟨M⟩?

Answer: Because you will try to make embedded_H do something that H
doesn't do.

>
> // *Olcott Turing machine  Ȟ --- Ȟ applied to* ⟨M⟩
> // --- Does M halt on its own Turing Machine Description?
> Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qy     // M applied to ⟨M⟩ halts
> Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qn    // M applied to ⟨M⟩ does not halt
>
> // *Olcott Turing machine  Ȟ --- Ȟ applied to* ⟨Ȟ⟩
> // --- Do you halt on your own Turing Machine Description?
> Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qy     // Ȟ applied to ⟨Ȟ⟩ halts
> Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qn    // Ȟ applied to ⟨Ȟ⟩ does not halt
> Ȟ applied to ⟨Ȟ⟩ simply correctly transitions to  Ĥ.qy
>
> Linz Turing machine Turing machine Ĥ applied to ⟨Ĥ⟩ is the self-
> contradictory form of Olcott Turing machine Ȟ applied to ⟨Ȟ⟩
>
> // *Linz Turing machine Ĥ --- Ĥ applied to* ⟨Ĥ⟩
> // --- Do you halt on your own Turing Machine Description?
> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn     // Ĥ applied to ⟨Ĥ⟩ does not
> halt
> Ĥ applied to ⟨Ĥ⟩ cannot correctly transition to  Ĥ.qy or Ĥ.qn
> because Ĥ applied to ⟨Ĥ⟩ is self contradictory.
>

Which means that no "correct" Ȟ can exist, not that the question is
invalid.

The QUESTION, does the machine described Halt or not, has a correct answer.

Thus, all you have proven, is the halting theorem, that no machine
exists that can give the answer

[olcott]

On 2/16/2024 11:39 AM, Richard Damon wrote:
> On 2/16/24 12:22 PM, olcott wrote:
>> I am merely using different notational conventions that are easier to
>> understand because they are more conventional. Linz uses Wm as the
>> finite string Turing machine description of some arbitrary machine M.
>>
>> // *Linz Turing machine H --- M applied to w*
>> // --- Does M halt on w?
>> H.q0 Wm w ⊢* H.qy // M applied to w halts
>> H.q0 Wm w ⊢* H.qn // M applied to w does not halt
>>
>> // *Linz Turing machine H --- M applied to w* (different encoding)
>> // --- Does M halt on w?
>> H.q0 ⟨M⟩ w ⊢* H.qy // M applied to w halts
>> H.q0 ⟨M⟩ w ⊢* H.qn // M applied to w does not halt
>>
>> // *Linz Turing machine H --- M applied to* ⟨M⟩
>> // --- Does M halt on ⟨M⟩ ?
>> H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qy // M applied to ⟨M⟩ halts
>> H.q0 ⟨M⟩ ⟨M⟩ ⊢* H.qn // M applied to ⟨M⟩ does not halt
>>
>> I am applying the Linz H' and Linz Ĥ in reverse order first
>> transforming H into Olcott Ȟ as the one parameter version of Linz H
>> where a machine is applied to its own Turing machine description.
>
> Which is something you have never said before.
>
>>
>> embedded_H ⟨M⟩ ⟨M⟩ means H.q0 ⟨M⟩ ⟨M⟩ shown above.
>
> And why can't you just say H.q0 ⟨M⟩ ⟨M⟩ instead of embedded_H ⟨M⟩ ⟨M⟩?
>

Ȟ:embedded_H is a state of Ȟ and reminds people what it is.
H.q0 is not a state of Ȟ and confuses people what it is.
Both are better than the Linz: Ĥq0 wM wM

> Answer: Because you will try to make embedded_H do something that H
> doesn't do.
>
>>
>> // *Olcott Turing machine  Ȟ --- Ȟ applied to* ⟨M⟩
>> // --- Does M halt on its own Turing Machine Description?
>> Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qy     // M applied to ⟨M⟩ halts
>> Ȟ.q0 ⟨M⟩ ⊢* embedded_H ⟨M⟩ ⟨M⟩ ⊢* Ĥ.qn    // M applied to ⟨M⟩ does not
>> halt
>>
>> // *Olcott Turing machine  Ȟ --- Ȟ applied to* ⟨Ȟ⟩
>> // --- Do you halt on your own Turing Machine Description?
>> Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qy     // Ȟ applied to ⟨Ȟ⟩ halts
>> Ȟ.q0 ⟨Ȟ⟩ ⊢* embedded_H ⟨Ȟ⟩ ⟨Ȟ⟩ ⊢* Ĥ.qn    // Ȟ applied to ⟨Ȟ⟩ does not
>> halt
>> Ȟ applied to ⟨Ȟ⟩ simply correctly transitions to  Ĥ.qy
>>
>> Linz Turing machine Turing machine Ĥ applied to ⟨Ĥ⟩ is the self-
>> contradictory form of Olcott Turing machine Ȟ applied to ⟨Ȟ⟩
>>
>> // *Linz Turing machine Ĥ --- Ĥ applied to* ⟨Ĥ⟩
>> // --- Do you halt on your own Turing Machine Description?
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qy ∞ // Ĥ applied to ⟨Ĥ⟩ halts
>> Ĥ.q0 ⟨Ĥ⟩ ⊢* embedded_H ⟨Ĥ⟩ ⟨Ĥ⟩ ⊢* Ĥ.qn     // Ĥ applied to ⟨Ĥ⟩ does
>> not halt
>> Ĥ applied to ⟨Ĥ⟩ cannot correctly transition to  Ĥ.qy or Ĥ.qn
>> because Ĥ applied to ⟨Ĥ⟩ is self contradictory.
>>
>
> Which means that no "correct" Ȟ can exist, not that the question is
> invalid.

Likewise Tarski concluded that no truth predicate
can exist that correctly answers this question:

Is this sentence: "this sentence is not true" true or false?

It never occurred to Tarski or Gödel that the domain of truth
predicates and formal proofs does not include self-contradictory
expressions.

Using this same reasoning we can say math is incomplete
because there is no square-root of an actual banana.

ONLY when we restrict the domain of math functions to numbers
can we understand that there is not supposed to be any square
root of an actual banana.

[Richard Damon]

But H.q0 iS a state of Ȟ since it included its own copy of H in it.

Youy don't seem to understand the DEFINITION of a program, it includes
ALL the algorithm that is part of it. The "sub-machines" are still part
of it.

Ȟ isn't just a "template" that uses things not part of it, it is an
actual program that has pulled in that code into it.

Except you can't show where they actually do what you claim, because you
are just too ignorant of the logic they are using.

You see words in isolation, and don't understand their context, which
actually proves your assertions to be wrong.

[immibis]

On 16/02/24 18:22, olcott wrote:
> [the exact same thing as before but written with mathematical symbols because everything that is written with mathematical symbols is correct]

In your x86utm version of the problem, the reason it cannot correctly
transition to qy is because it isn't programmed to do that transition.
The reason it can't correctly transition to qn is because that
transition is incorrect since the input halts.

[immibis]

On 16/02/24 19:26, olcott wrote:
>
> Likewise Tarski concluded that no truth predicate
> can exist that correctly answers this question:
>
> Is this sentence: "this sentence is not true" true or false?

He is correct. It can't.

>
> It never occurred to Tarski or Gödel that the domain of truth
> predicates and formal proofs does not include self-contradictory
> expressions.

So can a truth predicate exist that correctly answers the question, or
is Tarski correct to say it can't exist?

>
> Using this same reasoning we can say math is incomplete
> because there is no square-root of an actual banana.

no

>
> ONLY when we restrict the domain of math functions to numbers
> can we understand that there is not supposed to be any square
> root of an actual banana.
>

The halting problem is solvable on some restricted domains. You are
invited to find some domains where the halting problem is solvable.

[olcott]

Until you understand how and why Tarski is incorrect
you will continue to babble on with your false assumption
that I must be incorrect.

That I am correct about Tarski established my credibility.

[Richard Damon]

That you misstate what Tarski said, prove your non-credibility.

[immibis]

On 17/02/24 02:13, olcott wrote:
> On 2/16/2024 7:07 PM, immibis wrote:
>> On 16/02/24 19:26, olcott wrote:
>>>
>>> Likewise Tarski concluded that no truth predicate
>>> can exist that correctly answers this question:
>>>
>>> Is this sentence: "this sentence is not true" true or false?
>>
>> He is correct. It can't.
>>
>>>
>>> It never occurred to Tarski or Gödel that the domain of truth
>>> predicates and formal proofs does not include self-contradictory
>>> expressions.
>>
>> So can a truth predicate exist that correctly answers the question, or
>> is Tarski correct to say it can't exist?
>>
>>>
>>> Using this same reasoning we can say math is incomplete
>>> because there is no square-root of an actual banana.
>>
>> no
>>
>>>
>>> ONLY when we restrict the domain of math functions to numbers
>>> can we understand that there is not supposed to be any square
>>> root of an actual banana.
>>>
>>
>> The halting problem is solvable on some restricted domains. You are
>> invited to find some domains where the halting problem is solvable.
>
> Until you understand how and why Tarski is incorrect

You dishonestly avoided the question. I repeat the question: Can a truth

[olcott]

You assume that I must be misstating Tarski on the basis
that I say that he is wrong and you assume that I am wrong.

[olcott]

A truth predicate exists in the domain of truth bearers.
Tarski was too stupid to understand this.

[immibis]

Can a truth predicate exist that correctly answers the question?

[immibis]

There is a very simple answer to "Can a calculator exist that can
square-root a banana?" so why is it so hard for you to answer "Can a
truth predicate exist that correctly answers the question?"?

[olcott]

You are just playing head games.

[Richard Damon]

No, because you can't point out where he makes his assumption, but keep
on pointing at CONCLUSIONS.

[Richard Damon]

How do you know that a COMPUTABLE truth predicate exists?

You don't understand what computable means, because YOU are the one that
is too stupid.

It seems you don't understand his meaning for a "Definition of Truth",
which is just par for the course with you.

For someone who likes to base things on "the meaning of the words" you
do aweful bad with knowing the applicable "meaning of the words".

(In part because you don't understand how term-of-art definitions work.

[olcott]

You too are only playing head games.

[olcott]

On 2/16/2024 9:02 PM, Richard Damon wrote:

I can see the details of how this all works.
You have already agreed to these details.

[Richard Damon]

Says the person who can't actually prove anything they say.

You are continue to prove your stupidity, and your failure to show the
requested evidence just proves it. If you had ANY grounds for you
claims, you could provide it, instead, you base you logic on unfounded
assumptions and baseless claims.

Then you have the gaul to claim your goal it to make it impossible to
make baseless claims.

[Richard Damon]

WHERE?

You are just blowing smoke out of your ass.

You have shown that you just don't have the understanding of this sort
of material, after all, you have claimed that ENGLISH is a formal logic
system, which just shows how ignorant you are of what things actually mean.

[olcott]

The only reason that any analytic expression of language
is true is that it is semantically linked through a finite
or infinite sequence of steps to the semantic meanings that
make it true.

[Richard Damon]

And determining if such string of steps exists is not computable.

This is especially obvious if the chain of links is infinite, as you
can't step through the infinite chain in the required finite number of
steps and be computable.

So, it is clear that you don't understand something about this.

[immibis]

On 17/02/24 04:19, olcott wrote:

He is right. You have not pointed to any actual mistake. You have only
said you don't like the result.

[immibis]

[Richard Damon]

I have pointed out that he can't point out the mistakd he claims.

HE claims that Tarski and Godel make incorrect statements, but can't
actually point out where they make them.

For Tarski, he points to a conclusion that is made from previous parts
of the proof, and tries to say that the statement is non-sense, but
can't show any actual error in the logic that got him there.

For Godel, Godel makes an off-hand comment that the proof could be
extended by using the form of other epistemological antinomies which PO
assumes means that the truth of such an statement is critical to the
proof. When asked to show where he actually did that, he can't.

Thus, Peter's claim is the equivalent to Russel's teapot, that because
the teapot exists, they must be wrong, but he can't actually show that
the statements that would make them wrong actually exist in the proof.

[immibis]

Actually, the great innovation of mathematics is that the steps can be
formal - symbolic.
For example, if x+1=y is true, then x+2=y+1 is also true. It doesn't
matter what x and y represent. x+2=y+1 is still true.

[olcott]

This is a misconception anchored in the belief that expressions
of language that are semantically unsound must not be rejected
as erroneous.

>
> This is especially obvious if the chain of links is infinite, as you
> can't step through the infinite chain in the required finite number of
> steps and be computable.
>
> So, it is clear that you don't understand something about this.
>
>

Not at all. The sum total of all analytic human knowledge
is computable. Expressions of language requiring infinite
steps are of little consequence.

[olcott]

That you failed to comprehend the mistake that I pointed
out is not any actual rebuttal.

[olcott]

You know that I pointed out the mistake
many hundreds of times WHY LIE ???

[olcott]

Semantic entailment can be and has been formalized for many decades.

[immibis]

A semantically entails B if B is true in all models where A is true.

[immibis]

There are no semantically unsound logical formulas.

[immibis]

A conclusion which follows from true premises by a valid reasoning rule
must be true.

[olcott]

That is not what I mean. There is one model of the
actual world.

[olcott]

Your lack of knowledge is not a rebuttal.

[olcott]

OK you finally got an important one very right.
Good job !
How do you verify that the premises are true?

[immibis]

On 17/02/24 06:04, olcott wrote:

You are the one who lacks knowledge. Logical formulas cannot be
semantically unsound because they do not have semantics. That is the
innovation of mathematics. It is like saying x+1=5 is unsound.

[immibis]

How do YOU verify they are false?

[immibis]

Mathematics does not care about the actual world.

[Richard Damon]

No, there may be only one model that matches what we know of the actual
world, but logic isn't restricted to talking about the actual world.

This seems to be part of your problem, you don't even know the use case
of logic.

[olcott]

That some guy proposed possible worlds to cover hypothetical
possibilities means that they have diverged from truth.

> This seems to be part of your problem, you don't even know the use case
> of logic.

[olcott]

In other words you are saying that A ∧ B is meaningless gibberish.
Using Montague grammar of natural language semantics the full semantics
of natural language can be directly referenced by formalized natural
language expressions.

> That is the
> innovation of mathematics. It is like saying x+1=5 is unsound.

That Tarski anchored his undefinability theorem in the formalized
Liar Paradox proves that some formal expressions are unsound:
x ∉ True if and only if p

[olcott]

I know how I do it and I know how it is done.
No one seems to believe me even though it is the way
that truth really works.

When you must figure this out on your own then you can
see that my way is correct.

Unless you must figure this out on your own you seem to
continually baselessly disagree.

[olcott]

This is the only possible way to create the functional equivalent of a
human mind.

Cyc (pronounced /ˈsaɪk/ SYKE) is a long-term artificial intelligence
project that aims to assemble a comprehensive ontology and knowledge
base that spans the basic concepts and rules about how the world works.
https://en.wikipedia.org/wiki/Cyc

[Richard Damon]

Nope, you just don't understand what ANALYTICAL truth is, which is wha
you claim to be talking about.

What matches the "Real World" is Emperical Truth.

You still don't seem to understand what the words you use mean.

If you start from "Truthmakers", you are talking about an Analytical
system based on what is assumed in that system, which may or may not
match "reality".

[Richard Damon]

Which isn't "Formal Logic".

I guess you just don't know what "Logic" means.

>
>> That is the innovation of mathematics. It is like saying x+1=5 is
>> unsound.
>
> That Tarski anchored his undefinability theorem in the formalized
> Liar Paradox proves that some formal expressions are unsound:
> x ∉ True if and only if p
>

So, find the error in the work that produced that statement. The point
you quote it from refers to work he previously did.

If you can't, you can't make your claim.

[Richard Damon]

Which has WHAT to do with formal logic?

You don't seem to actually understand the basics of AI.

[Richard Damon]

You THINK you know what you do, but it is clear you don't understand
what any of it actually means.

It is clear you just don't understand what TRUTH is, since you misuse
the term so much.

>
> When you must figure this out on your own then you can
> see that my way is correct.
>
> Unless you must figure this out on your own you seem to
> continually baselessly disagree.
>

Until you understand what the words you are saying actually mean, your
statements are just gibberish nonsense, and become lies.

[immibis]

Yes, that's the innovation of mathematics. x+y=4 is meaningless
gibberish but you can still do something with it. If you apply
mathematical rules to the sentences x=1 and x+y=4 you can get other
meaningless gibberish like (x+y)^3=64 and y=3.

"formal" comes from the root "form", meaning "appearance". You can
manipulate mathematical expressions based on just their appearance. You
do not have to know that x is the number of cows that Alice has and y is
the number of cows that Joey has. It is still the case that (x+y)^3=64.

> Using Montague grammar of natural language semantics the full semantics
> of natural language can be directly referenced by formalized natural
> language expressions.

Montague grammar attempts to translate natural language into
mathematics. For sentences already in mathematics there it is irrelevant.

> That Tarski anchored his undefinability theorem in the formalized
> Liar Paradox proves that some formal expressions are unsound:

The Liar Paradox cannot be formalized.

[immibis]

This is irrelevant to the halting problem.

[immibis]

In the actual world, x is a shape made from two straight lines. x=3 is
inconsistent with the actual world since 3 is not a shape made from two
straight lines.

[olcott]

It is indirectly relevant.
The Cyc project proves that English can be mathematically formalized.
This proves that semantics can be directly formalized in the formal
system with no need to separate syntax from semantics.

This proves that expressions of language can be rejected as
semantically unsound thus the convention of not rejecting
semantically unsound expressions has no correct basis.

[olcott]

Tarski did this proving that you are wrong.

x ∉ True if and only if p

where the symbol 'p' represents the whole sentence x

This retains the self-contradictory nature of the Liar Paradox
yet does not include its infinitely recursive nature.

[immibis]

Whether we math can prove things about English is completely irrelevant
to whether there is a Turing machine that answers the halt status of all
Turing machines.

[immibis]

Tarski said that if it can be formalized, the system is inconsistent.
If the system is consistent, then it cannot be formalized.
Once again, you do not understand how proof by contradiction works.

[Richard Damon]

You are just showing that you don't really understand what you are
talking about, in particular here, what "Formal" actually means.

"Formalizing English" in this context means removing the ambquity of the
meaning of the words and the syntax. It doesn't say anything about
determining if a given sentence is actually a "True" sentence or even if
it is statement which has no truth value. It might be able to determine
SOME statements, but not all.

A "Formal Language" is not a "Formal Logic System" and that difference
seems to evade you.

[olcott]

If math can proving things about English then math is expressive enough
that it can perform any analytical proof about anything. It is not
forced to ignore that an expression is self-contradictory because it
does not know what self-contradictory is.

[olcott]

Yes that is correct.

> It doesn't say anything about
> determining if a given sentence is actually a "True" sentence or even if
> it is statement which has no truth value.

Formalized English is as expressive as English thus can see
and understand when an expression is self-contradictory.

> It might be able to determine
> SOME statements, but not all.
>
> A "Formal Language" is not a "Formal Logic System" and that difference
> seems to evade you.

[olcott]

On 2/18/2024 11:25 AM, Mikko wrote:

> If math can prove things about English like something about the lengths
> of words or nesting levels of subordiante clauses that does not mean
> that it can perform an analytical proof about anything.
>

If math fully understands everything that can be expressed in English
then math is expressive enough to reject self-contradictory expressions
as not in the domain of any formal logic system.

[olcott]

On 2/18/2024 11:36 AM, Mikko wrote:

> In a formal language every string either is in the language or is not.
> But people people have different opinions of whether e.g. "Our mission
> so to boldly go where no one has returned from." is syntactically
> correct. People also disagree what "I never gave no money" means.
> To formalize English means to replace it with something that looks
> more or less similar, e.g., COBOL.

[Richard Damon]

And it doesn't.

Just like it shows that mathematics is powerful enough to create some
statements that are complicated enough that they can not be proven in a
finite number of steps.

This is the fundamental property behind all your problems, Halting,
Incompleteness, and lack of a computable Truth Predicate.

You just don't seem to be able to understand that part of Mathematics.
lokely because you can't handle the abstractions of it.

[Richard Damon]

Most Formal Logic System DO exclude actually self-contradictory
expression as outside there language. (There are some systems that
specifically allow self-contradictory expressions to look at what
happens to logic without one or both of the law of the excluded middle
or the law of non-contradiction (allowing a given expression to be
neither True or False, or Both True and False at the same time).

[Richard Damon]

Maybe, but it isn't a formal logic system, which you don't seem to know
what that is, so all your aguements are show to be just your own
misunderstandings.

Some Logical Self-Contradictions go to complexity that just knowing the
meaning of the words doesn't reveal that the statement IS
self-contradictory under the formal logic system.

[Richard Damon]

And, as you have described, it means attaching a qualifying tag to every
word (or at least every word that needs one), so it no longer reads like
English.

[olcott]

You make sure to change the subject from the point that
I make when I make my point. *That is dishonest*

There are formal systems that can recognize and reject
epistemological antinomies. PA is not one of them.

[Richard Damon]

YOU'RE the one that went off on the language tangent.

>
> There are formal systems that can recognize and reject
> epistemological antinomies. PA is not one of them.
>

And why do you say that?

You still haven't pointed out where exactly the error occurs.

Note, NOT as a conclusion, that is used to show that there was a wrong
assumption in the system, but as an input assumption.

[immibis]

PA does not contain any epistemological antinomies.