Prolog already refutes Tarski Undefinability

[PeteOlcott]

Prolog queries return "Yes" when-so-ever an expression is provable on
the basis of the Facts and Rules in its database and returns "No" otherwise.
Facts correspond to axioms, Rules correspond to rules-of-inference and
the Prolog database corresponds to a formal system.

The above inference model directly refutes the third line of Tarski's proof:
http://liarparadox.org/Tarski_Proof_275_276.pdf
(3) x ∉ Pr if and only if x ∈ Tr

~Provable(x) ↔ True(x)
Because of the way that the Prolog inference model works the above
expression would be false, and its negation: Provable(x) ↔ True(x)
would be true. So the Prolog inference model already refutes Tarski's
line (3) which in turn causes the whole rest of Tarski's proof to fail.

[wtf]

Prolog queries return "Yes" when-so-ever an expression is provable on
the basis of the Facts and Rules in its database and returns "No" otherwise.

Does Prolog satisfy the hypotheses of Tarski's indefinability theorem? Offhand I would doubt it, since any computer language implemented on physical hardware cannot represent arithmetic. Can you clarify this point?

[PeteOlcott]

Prolog queries return "Yes" when-so-ever an expression is provable on
the basis of the Facts and Rules in its database and returns "No" otherwise.

Does Prolog satisfy the hypotheses of Tarski's indefinability theorem? Offhand I would doubt it, since any computer language implemented on physical hardware cannot represent arithmetic. Can you clarify this point?

This is the generalized result of the Tarski Undefinability Theorem:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

The Prolog inference model decides that this third line of Tarski's proof is false:
(3) x ∉ Pr if and only if x ∈ Tr
thus causing the rest of Tarski's proof to fail.

All formal systems having the same inference model as Prolog would prevent
any form of Tarski's proof to succeed because undecidable sentences are
inexpressible within this model.

[wtf]

Prolog queries return "Yes" when-so-ever an expression is provable on
the basis of the Facts and Rules in its database and returns "No" otherwise.

Does Prolog satisfy the hypotheses of Tarski's indefinability theorem? Offhand I would doubt it, since any computer language implemented on physical hardware cannot represent arithmetic. Can you clarify this point?

This is the generalized result of the Tarski Undefinability Theorem:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

The Prolog inference model decides that this third line of Tarski's proof is false:
(3) x ∉ Pr if and only if x ∈ Tr
thus causing the rest of Tarski's proof to fail.

Nice deflection. I will repeat my question since you clearly didn't read it.

Does Prolog satisfy the hypotheses?

[wtf]

double post.

[PeteOlcott]

Does Prolog satisfy the hypotheses of Tarski's indefinability theorem? Offhand I would doubt it, since any computer language implemented on physical hardware cannot represent arithmetic. Can you clarify this point?

This is the generalized result of the Tarski Undefinability Theorem:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

The Prolog inference model decides that this third line of Tarski's proof is false:
(3) x ∉ Pr if and only if x ∈ Tr
thus causing the rest of Tarski's proof to fail.

Nice deflection. I will repeat my question since you clearly didn't read it.

Does Prolog satisfy the hypotheses?

Instead of directly saying that Prolog refutes the hypothesis I explained all of
the details of exactly how Prolog directly refutes the hypothesis. Since Prolog
defines True(x) ↔ Provable(x) anything contradicting this such as
True(x) ↔ ~Provable(x) (which is the third line of Tarski's proof) is decided to be false.

[wtf]

Instead of directly saying that Prolog refutes the hypothesis I explained all of
the details of exactly how Prolog directly refutes the hypothesis. Since Prolog
defines True(x) ↔ Provable(x) anything contradicting this such as
True(x) ↔ ~Provable(x) (which is the third line of Tarski's proof) is decided to be false.

Then it must follow that Prolog does not satisfy the hypotheses of Tarski's theorem.

[PeteOlcott]

Instead of directly saying that Prolog refutes the hypothesis I explained all of
the details of exactly how Prolog directly refutes the hypothesis. Since Prolog
defines True(x) ↔ Provable(x) anything contradicting this such as
True(x) ↔ ~Provable(x) (which is the third line of Tarski's proof) is decided to be false.

Then it must follow that Prolog does not satisfy the hypotheses of Tarski's theorem.

Let's say it in much simpler terms. Prolog proves that Tarski was wrong.

Tarski was using a broken notion of formal system that could not detect
and reject incorrect expressions of language.

[wtf]

Let's say it in much simpler terms. Prolog proves that Tarski was wrong.

So you still can't confirm that Prolog satisfies the hypotheses.

You've said that your objective in posting is to get people to understand and accept your ideas. Repeated avoidance of obvious questions doesn't help your cause.

If you claim that

- IF your system satisfied Tarski's hypotheses ...

- THEN it would disprove Tarski's theorem;

then ANYONE who reads your claim would immediately ask if you can show that your system does in fact satisfy the hypotheses. Because if it does, then maybe you've overthrown 80 years of conventional wisdom.

But if you can't respond clearly and directly and at least a little bit convincingly, then it's clear you have nothing.

[PeteOlcott]

This reply was incorrect.

[PeteOlcott]

Let's say it in much simpler terms. Prolog proves that Tarski was wrong.

If you claim that
- IF your system satisfied Tarski's hypotheses ...
- THEN it would disprove Tarski's theorem;

then ANYONE who reads your claim would immediately ask if you can show that your system does in fact satisfy the hypotheses. Because if it does, then maybe you've overthrown 80 years of conventional wisdom.

I keep rereading what people say to make sure that I responded correctly.

I must have the idea of what you are calling Tarski's hypothesis backwards.
What Hypothesis are you referring to?

I was referring to this:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

[wtf]

I was referring to this:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

Right. What evidence can you advance to show that a physical implementation of the Prolog language on hardware that conforms to the known laws of physics; has the expressive power of arithmetic? I'm no specialist but my sense is that it could not possibly be. It could not satisfy the axiom of mathematical induction; because that axiom gives us an unbounded sequence of possible numbers. No physical hardware could represent such a sequence. Your model is only theoretical. And even so, it's subject to the Halting problem. So you are just not making your case here. Not to me, anyway. I hope I may serve as a datapoint in your quest to be understood. You are not convincing me.

And why Prolog, by the way? Wouldn't any other Turing-complete language do as well? Python, FORTRAN, MUMPS, Pascal, C, C++, Java, you know the drill.

[Logik]

I was referring to this:
All formal systems of greater expressive power than arithmetic necessarily
have undecidable sentences.

I think I am starting to see your intention/objective here and I want to be sure we are on the same page in terms of your criteria for success.

Are you trying to lay down a set of axioms which guarantee that a system which adheres to them has both of these properties:

1. The system is more expressive than arithmetic.
2. The system is decidable.

A yes/no answer to would suffice here.

My second question would be that to which wtf alluded to above.

How do you evaluate "expressive power" ?

Given any two systems A and B, how do you evaluate the truth-value of the proposition: moreExpressive(A,B) ?

[Logik]

It could not satisfy the axiom of mathematical induction; because that axiom gives us an unbounded sequence of possible numbers.

Symbolically it does. Numerically the sequence is a limit-function of time.

Chalk it to unresolvable philosophical differences.

[wtf]

It could not satisfy the axiom of mathematical induction; because that axiom gives us an unbounded sequence of possible numbers.

Symbolically it does.

No it does not. Let the axiom of induction state that for the predicate N(n) meaning "n is a number," we can write the axiom of induction:

N(0) AND (N(n) => N(n+1)

That is a symbolic representation of mathematical induction. But it is FALSE in the system of numbers represented by any physical computer. A physical computer has some number X that is the largest number that it can represent. Then N(X) but not-N(X+1).

Since induction doesn't hold, the hypotheses of Tarski's theorem are not satisfied. So if Peter can prove that in his system the conclusion of Tarski's theorem is false, that does not invalidate Tarski's theorem.

It's like saying All Cretans are Liars; but Fred is not a Cretan and he always tells the truth. That doesn't falsify the fact that all Cretens are liars, because Fred does not satisfy the hypothesis. He's not a Cretan. And Prolog or any other programming language implemented on physically realizable hardware (consistent with known physics) can not implement mathematical induction hence does not satisfy the hypotheses of Tarski's theorem.