Eliminating undecidability in formal systems

[PeteOlcott]

The conventional meaning of the logic symbols.

https://repl.it/repls/AcclaimedJubilantTasks

The notion of "conventional" doesn't work with semantics.

The meaning of "=" doesn't work with non-numbers.

What does it mean to compare one cat to another cat? Are you testing for identity or type?

You are getting off topic. You specified that it was an integer
so going through any assumption that it is not an integer wastes time.
I really don't have that time to waste.

[Logik]

You are getting off topic. You specified that it was an integer
so going through any assumption that it is not an integer wastes time.
I really don't have that time to waste.

OK!

Now tell me how you managed to evaluate an infinite set in 5 seconds.

[PeteOlcott]

https://repl.it/repls/AcclaimedJubilantTasks

The notion of "conventional" doesn't work with semantics.

Although you might not understand how it does, it still does.

OK, if you are going to lecture me on things you have nothing other than academic experience with, I am out.

What does it mean to compare one cat to another cat? Are you testing for identity or type?

You already specified that it was an integer. That it might be a cat
is specified as impossible.

[Logik]

You already specified that it was an integer. That it might be a cat
is specified as impossible.

Because I am trying to make my point gradually,

1. for all x: x = x, x ∈ Integers

You decided it's true in 5 seconds, even though the set of Integers is infinite, because you made some assumptions about the meaning of "="

Now I drop the Integer constraint:

2. for all x: x = x, x ∈ ALL ( https://en.wikipedia.org/wiki/ALL_(complexity) )

What would you say about the truth-value now?

What are the semantics of "=" in a universal context?

[PeteOlcott]

The conventional meaning of the logic symbols.

https://repl.it/repls/AcclaimedJubilantTasks

The notion of "conventional" doesn't work with semantics.

The meaning of "=" doesn't work with non-numbers.

What does it mean to compare one cat to another cat? Are you testing for identity or type?

Sure it does. All that you have to do is associate the conventional
meaning of the logic symbols with their corresponding algorithm
it is really not that hard.

I am simply saying lets just assume that step is already done.
C++ compilers do that all the time. You act like it was an impossibly
difficult task.

[Logik]

Sure it does. All that you have to do is associate the conventional
meaning of the logic symbols with their corresponding algorithm
it is really not that hard.

Ok! Please associate the conventional meaning of "=" with the corresponding algorithm then.

What does it mean for two non-integers to be equal to each other?

I am simply saying lets just assume that step is already done.

Lets not assume it. DO it.

C++ compilers do that all the time. You act like it was an impossibly
difficult task.

Yeah! It is.That's literally why we have Hindley-Milner type systems - with type-checking and type-inference.
C++ didn't do type inference before version 11, and even then it's limited.

So that we can figure out what the fuck it means to compare different types to each other.

https://en.wikipedia.org/wiki/Hindley%E ... ype_system

So once more. Is this decidable:

for all x: x = x, x ∈ ALL

[Logik]

And the last thing I am going to leave you with (because I need sleep).

From Type theory wiki page: In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

Does this mean we need a unique equals (=) operator for each and every type?

Lets make it a function: equal(a,b) -> {True, False}

So it means we have one function for comparing integers: equal_integers(a,b) -> {True, False}
Another function for comparing floats: equal_floats(a,b) -> {True, False}

Is this decidable: equal(equal_integers(), equal_floats()) ?

[PeteOlcott]

Yeah! It is.That's literally why we have Hindley-Milner type systems - with type-checking and type-inference.
C++ didn't do type inference before version 11, and even then it's limited.

So that we can figure out what the fuck it means to compare different types to each other.

https://en.wikipedia.org/wiki/Hindley%E ... ype_system

So once more. Is this decidable:

for all x: x = x, x ∈ ALL

for (int x = 0; x <= 0xffffff; x++)
if (x != x)
printf("C does not understand what the equality operator means\n");

[Logik]

for (int x = 0; x <= 0xffffff; x++)
if (x != x)
printf("C does not understand what the equality operator means\n");

Those are integers. But a tiny subset of ALL ( https://en.wikipedia.org/wiki/ALL_(complexity) )

And you are still dodging the issue of whether the semantics of "=" are the same for integers and cats.

[PeteOlcott]

And the last thing I am going to leave you with (because I need sleep).

From Type theory wiki page: In type theory, every "term" has a "type" and operations are restricted to terms of a certain type.

Does this mean we need a unique equals (=) operator for each and every type?

Lets make it a function: equal(a,b) -> {True, False}

So it means we have one function for comparing integers: equal_integers(a,b) -> {True, False}
Another function for comparing floats: equal_floats(a,b) -> {True, False}

Is this decidable: equal(equal_integers(), equal_floats()) ?

This is totally outside the scope of this post. Only the two-page
Tarski proof and my refutation are in scope.

Good night.

[PeteOlcott]

for (int x = 0; x <= 0xffffff; x++)
if (x != x)
printf("C does not understand what the equality operator means\n");

Those are integers. But a small subset of ALL.

And you are still dodging the issue of whether the semantics of "=" are the same for integers and cats.

Integers and equality and types are all out-of-scope.
Only the two-page Tarski proof and my refutation are in scope.

I explain the very personal reason why I have to keep these
things as succinct as possible in my other reply.

[wtf]

And the last thing I am going to leave you with (because I need sleep).

I explain the very personal reason why I have to keep these
things as succinct as possible

You two guys are clearly punched out.

[Logik]

You two guys are clearly punched out.

This is a boxing match?

I mean - I saw him swinging. That's why I dodged. But I am trying to convince him (like I was trying to convince you) that I am not fighting....

Hypothesis 2: I misunderstood the idiom.

[PeteOlcott]

You two guys are clearly punched out.

This is a boxing match?

I mean - I saw him swinging. That's why I dodged. But I am trying to convince him (like I was trying to convince you) that I am not fighting....

Hypothesis 2: I misunderstood the idiom.

My point can only be understood within the context of these two pages:
http://liarparadox.org/Tarski_Proof_275_276.pdf

Except for the mixing and matching between his meta-theory and his
theory this proof is actually quite easy to understand.

My point can be made without any understanding of the distinction
between his meta-theory and his theory. One merely needs to understand
the sequence of numbered steps from (1) to (9) the rest of the proof
can be ignored.

One need not even understand the sequence of steps very well, only
that if step (3) of the proof is proved false, that the whole proof fails.
We also have to know that "Pr" means Provable and "Tr" means True.

[PeteOlcott]

You two guys are clearly punched out.

This is a boxing match?

I mean - I saw him swinging. That's why I dodged. But I am trying to convince him (like I was trying to convince you) that I am not fighting....

Hypothesis 2: I misunderstood the idiom.

I don't know what: [misunderstood the idiom] means, but after explaining
all the details that you need to know, it seems reasonable to you just
couldn't understand Tarski well enough.

The convolutions of his mixing and matching between his meta-theory and
his theory seems to have confused himself. I evaluate Tarski with a single
language of the same expressive power of his meta-language. I skip the
weaker language all together.