Prolog already refutes Tarski Undefinability

[PeteOlcott]

Yes it is simply a nutty idea that was tried out because no one had a decent solution for undecidability.

Let me put it in far simpler terms. If you solved decidability - you have necessarily decided if P = NP.

How would finding a way to reject semantically ill-formed expressions
of language reduce the complexity of computation?

I merely made everything decidable, how long it takes to decide is a
whole other issue entirely.

[Logik]

How would finding a way to reject semantically ill-formed expressions
of language reduce the complexity of computation?

Let me translate this for you into English.

You are necessarily claiming that your axioms can detect that I am not saying what I mean to say.
Because the first and foremost property of formal CONSTRUCTIVE semantics is intent.

You are effectively claiming mind-reading.

Now, it may be true that in a particular language with a particular set of rules, a particular expression is invalid, but all that means is your language is prescribing expressiveness.

I merely made everything decidable, how long it takes to decide is a
whole other issue entirely.

What this sounds like to me is that you have found a mechanism to detect/prevent infinite loops at compile-time?

Because that's what "undecidable" means in practice. No exit criterion.

[PeteOlcott]

How would finding a way to reject semantically ill-formed expressions
of language reduce the complexity of computation?

Let me translate this for you into English.

You are necessarily claiming that your axioms can detect that I am not saying what I mean to say.
Because the first and foremost property of formal CONSTRUCTIVE semantics is intent.

You didn't realize that the scope is mathematics, or are you claiming
that equations can have malicious intent to deceive?

[Logik]

You didn't realize that the scope is mathematics, or are you claiming
that equations can have malicious intent to deceive?

I have no idea what that means.

The scope is mathematics. Algorithms are mathematical objects. Programming languages are mathematical notions.

Equations/algorithms have no intent. The person USING or CONSTRUCTING the equation/algorithm has intent.
Intent is difficult to capture in formalism, therefore the semantics of the human are difficult to capture entirely.
That's why we document and comment our code.

You still don't understand Hanlon's razor. It's just a mistake. You interpreted what I said in a way that I didn't mean it.

I'd go as far as to call you paranoid because you keep using language like "deception" and "lying" which suggests malice and intent.

Humans don't go out of their ways to deceive each other (not often anyway). Language/communication is just a mess.

[PeteOlcott]

You are effectively claiming mind-reading.

How is this about math or computer science?

[PeteOlcott]

Now, it may be true that in a particular language with a particular set of rules, a particular expression is invalid, but all that means is your language is prescribing expressiveness.

I merely made everything decidable, how long it takes to decide is a
whole other issue entirely.

What this sounds like to me is that you have found a mechanism to detect/prevent infinite loops at compile-time?

Because that's what "undecidable" means in practice. No exit criterion.

Of course we have to prescribe expressiveness otherwise encoding
and decoding of the communication process could not occur.

http://blog.tnsemployeeinsights.com/wp- ... ocess3.png

[Logik]

How is this about math or computer science?

How is it not?

Languages (even formal ones) are tools for self-expression.

[Logik]

Of course we have to prescribe expressiveness otherwise encoding
and decoding of the communication process could not occur.

That's a very broad claim. So broad as to be meaningless without particular context.

Are you talking about human-to-human communication, or computer-to-computer communication?

I can process (think) in one language and communicate in another.

Computers do too. Quite literally. TCP/IP is language agnostic.

[PeteOlcott]

I merely made everything decidable, how long it takes to decide is a
whole other issue entirely.

What this sounds like to me is that you have found a mechanism to detect/prevent infinite loops at compile-time?

Because that's what "undecidable" means in practice. No exit criterion.

I am not talking about algorithms I am talking about statically specified predicate logic.

The first incompleteness theorem states that in any consistent formal system F within which a certain amount of arithmetic can be carried out, there are statements of the language of F which can neither be proved nor disproved in F.
Raatikainen, Panu, "Gödel's Incompleteness Theorems", The Stanford Encyclopedia of Philosophy (Fall 2018 Edition)

With my slight adaptation to the notion of a formal system the above can no longer be constructed.
Because this becomes true: ~∃F ∈ Formal_Systems ~∃G ∈ WFF(F) (G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G)))

https://www.researchgate.net/publicatio ... ly_Refuted

[Logik]

With my slight adaptation to the notion of a formal system the above can no longer be constructed.
Because this becomes true: ~∃F ∈ Formal_Systems ~∃G ∈ WFF(F) (G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G)))

https://www.researchgate.net/publicatio ... ly_Refuted

Hence the problem! You are trying to define and prescribe what a "formal system is".

To me it's all language.

English. Mathematics. Predicate logic.

It's all Language. All linguistic rules are arbitrary.

I am losing track of all your different threads now, but I am pretty sure I constructed you an algorithm which evaluates G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G))
As true and as false.

And if I haven't - i am sure you get the strategy. Redefine the operator semantics in a way that gives you the answer you want.

[PeteOlcott]

With my slight adaptation to the notion of a formal system the above can no longer be constructed.
Because this becomes true: ~∃F ∈ Formal_Systems ~∃G ∈ WFF(F) (G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G)))

https://www.researchgate.net/publicatio ... ly_Refuted

Hence the problem! You are trying to define and prescribe what a "formal system is".

To me it's all language.

English. Mathematics. Predicate logic.

It's all Language. All linguistic rules are arbitrary.

I am losing track of all your different threads now, but I am pretty sure I constructed you an algorithm which evaluates G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G))
As true and as false.

And if I haven't - i am sure you get the strategy. Redefine the operator semantics in a way that gives you the answer you want.

If the linguistic rules were arbitrary as you claim this conversation would be impossible
because it depends on mutually agreed upon (thus not arbitrary) rules.

I am focusing on this one thread. You could "prove" that this expression
G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G)) is merely an idiom for {get me an ice cream sandwich}
but then this "proof" would contradict (and be refuted by) the axioms that already
assign a different meaning to those symbols.

[Logik]

If the linguistic rules were arbitrary as you claim this conversation would be impossible
because it depends on mutually agreed upon (thus not arbitrary) rules.

This is a very binary viewpoint.

The conversation wouldn't be impossible. It would just be incredibly difficult to understand each other or get to a point on deeply technical matters.
Q.E.D There seems to be some overlap in our linguistic practices, but the divergence is obvious.

I am questioning whether you watched the youtube video I posted on "language as a tool".

Furthermore, the "agreement" you speak of emerges tacitly from back-and-forth interaction, not because some logician sat in a room for 18 months who now suddenly insists that I MUST adhere to the rules he contrived. That's not how things work between humans.

The comic below would certainly apply to "rules and standards" of formal logic.

standards.png

I am focusing on this one thread. You could "prove" that this expression
G ↔ (~(F ⊢ G) ∨ ~(F ⊢ ~G)) is merely an idiom for {get me an ice cream sandwich}
but then this "proof" would contradict (and be refuted by) the axioms that already
assign a different meaning to those symbols.

At no point in this conversation have you bothered to address the argument for the Axiom of Choice.

If you choose a different set of axioms to me we exist in different paradigms.

[PeteOlcott]

If the linguistic rules were arbitrary as you claim this conversation would be impossible
because it depends on mutually agreed upon (thus not arbitrary) rules.

This is a very binary viewpoint.

The conversation wouldn't be impossible. It would just be incredibly difficult to understand each other or get to a point on deeply technical matters.
Q.E.D There seems to be some overlap in our linguistic practices, but the divergence is obvious.

If everyone spoke their own private form of gibberish communication would only be difficult?
Clearly you don't bother to think these things through very well.

[PeteOlcott]

At no point in this conversation have you bothered to address the argument for the Axiom of Choice.

If you choose a different set of axioms to me we exist in different paradigms.

None-the-less a cat is never a dog and a chocolate bar is never a dump truck,
the underlying semantic relations remain immutable unchanged no matter how we encode them.

https://www.researchgate.net/publicatio ... al_Systems

[Logik]

None-the-less a cat is never a dog and a chocolate bar is never a dump truck,
the underlying semantic relations remain immutable unchanged no matter how we encode them.

A cat is similar to a dog in some ways and different in others.

A chocolate bar is similar to a dump trick in some ways and different in others.

Depending on the questions you are asking and the answers you are seeking their similarities or differences may be relevant or irrelevant to your ontology.