Prolog already refutes Tarski Undefinability

[Logik]

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).

I don't understand your semantics.

In this case where X+1 becomes too large evaluating N(X+1) would produce an error. An error is neither true nor false.
What does the negation of an error mean?

Here's what Python thinks:
https://repl.it/repls/BeneficialAlphanu ... awarehouse

# Is an error the same as the logical notion of False?
# Answer: False
# Is an error the same as the logical notion of True?
# Answer: False
# What is the negation of an error?
# Answer: False
# Is the double-negation of an error True?
# Answer: True
# Is the double-negation of an error-object the same as itself?
# Answer: False

Either way I have absolutely no idea how to evaluate: error > N(n)

Do you?

[Logik]

A physical computer has some number X that is the largest number that it can represent.

It has a limit on the number it can STORE in memory. It has no limit on the sequence it can generate (express?) via streaming.

Given infinite time, a computer can produce an infinite digit-sequence
Given infinite time + 1, it can produce an bigger infinite digit-sequence

https://en.wikipedia.org/wiki/Stream_(computing)

[PeteOlcott]

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) ?

I only used the phrase (greater expressive power than arithmetic) to meet this specification:
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),

The actual requirement is that the formal systems must directly have a provability
predicate (not faking one using diagonalization). This system would be consistent and
complete as long as it implements the Prolog inference model which is equivalent to
my three axioms of truth.

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

[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) ?

Any formal systems directly having a provability predicate (not faking one using diagonalization)
is consistent and complete as long as it implements the Prolog inference model which is equivalent
to my three axioms of truth.

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

1. You failed to answer my simple yes/no question.
2. You have "diagonalized" the semantics of "provability"

Curry-Howard isomorphism has one conception of "provability"
You are pushing another.

Yours is axiomatic.
Curry-Howard is axiom-less

I am going to go with the more universal system.

[PeteOlcott]

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) ?

Any formal systems directly having a provability predicate (not faking one using diagonalization)
is consistent and complete as long as it implements the Prolog inference model which is equivalent
to my three axioms of truth.

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

1. You failed to answer my simple yes/no question.
2. You have "diagonalized" the semantics of "provability"

Curry-Howard isomorphism has one conception of "provability"
You are pushing another.

Yours is axiomatic.
Curry-Howard is axiom-less

I am going to go with the more universal system.

The expressive power related to arithmetic is not actually required.
THIS IS NOT ALLOWED: 2. You have "diagonalized" the semantics of "provability"
This "⊢" is required.

The key issue with the way that formal systems are defined is that none
of these formal systems can deal with incorrect expressions of language.
Is it a closed WFF that is neither true nor false? then it is incorrect and assigned a Truth value of ~True.

Any formal system implementing these axioms has no undecidable sentences.
(1) True(x) ↔ (x) // A set of facts adds up to X being TRUE.
(2) False(x) ↔ (⊢~x) // A set of facts adds up to X being FALSE.
(3) ~True(x) ↔ ~(⊢x) // No set of facts add up to X being TRUE.
Every otherwise undecidable sentence is decided to be ~True thus making it decidable.

~(~True(x) ↔ True(x)) ∨ (~True(x) ↔ False(x))
(Closed_WFF(x) ∧ ~True(x) ∧ ~False(x)) ↔ Incorrect(x)


∧

[Logik]

The expressive power related to arithmetic is not actually required.
THIS IS NOT ALLOWED: 2. You have "diagonalized" the semantics of "provability"
This "⊢" is required.

The above does not compute for me. Why are you putting limits on me when we are talking about "expressive power"?

To claim that I am not "allowed to say" things is counter-productive.

The key issue with the way that formal systems are defined is that none
of these formal systems can deal with incorrect expressions of language.

This is not true. Compilers are literally there to check grammar/semantics of your expressions.

Unless you are trying to tell me that computer languages are not formal systems.

Is it a closed WFF that is neither true nor false? then it is incorrect and assigned a Truth value of ~True.

This is a stupid rule.

An error is neither true nor false. As demonstrated here:

https://repl.it/repls/BeneficialAlphanu ... awarehouse


Again - your requirement for "closed" WFF makes no sense to me. You are literally arguing for linguistic prescriptivism.

[PeteOlcott]

The expressive power related to arithmetic is not actually required.
THIS IS NOT ALLOWED: 2. You have "diagonalized" the semantics of "provability"
This "⊢" is required.

The above does not compute for me. Why are you putting limits on me when we are talking about "expressive power"?

To claim that I am not "allowed to say" things is counter-productive.

The key issue with the way that formal systems are defined is that none
of these formal systems can deal with incorrect expressions of language.

This is not true. Compilers are literally there to check grammar/semantics of your expressions.

Unless you are trying to tell me that computer languages are not formal systems.

Is it a closed WFF that is neither true nor false? then it is incorrect and assigned a Truth value of ~True.

This is a stupid rule.

An error is neither true nor false. As demonstrated here:

https://repl.it/repls/BeneficialAlphanu ... awarehouse


Again - your requirement for "closed" WFF makes no sense to me. You are literally arguing for linguistic prescriptivism.

I provided the means to make all otherwise undecidable sentences (such as the Tarski x) decidable.
If you don't know the Tarski proof well enough you won't be able to understand what I mean.

Here is the whole proof:
http://liarparadox.org/Tarski_Proof_275_276.pdf

Here is the undecidable Tarski x
http://liarparadox.org/247_248.pdf

His way of doing formal systems cannot decide his x within a single formal system.
My way of doing formal systems decides the Tarksi x in a single formal system.
He "proves" that his x cannot be decided within a single formal system.
I refute this proof by showing how a single formal system decides his x.

[Logik]

His way of doing formal systems cannot decide his x within a single formal system.

Which I agree with and demonstrated.

My way of doing formal systems decides the Tarksi x in a single formal system.

Yes, but then you are prescribing to me a severely crippled formal system with limited expressive power.

Something which has zero practical utility to me.

He "proves" that his x cannot be decided within a single formal system.
I refute this proof by showing how a single formal system decides his x.

So your system necessarily ignores self-reference/recursion.

Is your system Turing-complete then?

[PeteOlcott]

His way of doing formal systems cannot decide his x within a single formal system.

Which I agree with and demonstrated.

My way of doing formal systems decides the Tarksi x in a single formal system.

Yes, but then you are prescribing to me a severely crippled formal system with limited expressive power.

Something which has zero practical utility to me.

My system has all of the expressive power of every other formal system
and the additional expressive power to be able to decide previously
undecidable sentences.

[PeteOlcott]

His way of doing formal systems cannot decide his x within a single formal system.

He "proves" that his x cannot be decided within a single formal system.
I refute this proof by showing how a single formal system decides his x.

So your system necessarily ignores self-reference/recursion.

Is your system Turing-complete then?

Turing complete systems are not required and cannot possibly exist.
The sum total of all currently existing general knowledge does not require
a Turing Complete infinite amount of memory.

My system cannot (for example) count to infinity and a Turing machine can.

It does not ignore either self-reference or recursion. It decides that
expressions of language involving non terminating self-reference / recursion
are incorrect logical sentences.

[Logik]

It does not ignore either self-reference or recursion. It decides that
expressions of language involving non terminating self-reference / recursion
are incorrect logical sentences.

So how do you know if self-reference is terminating?

Here is temporal self-reference for you: I

Are you telling me referring to myself is logically incorrect?

[Logik]

It does not ignore either self-reference or recursion. It decides that
expressions of language involving non terminating self-reference / recursion
are incorrect logical sentences.

Here's a non-terminating algorithm find(Truth)

Has been running since humanity started... still going.

[PeteOlcott]

It does not ignore either self-reference or recursion. It decides that
expressions of language involving non terminating self-reference / recursion
are incorrect logical sentences.

So how do you know if self-reference is terminating?

Here is temporal self-reference for you: I

Are you telling me referring to myself is logically incorrect?

The fact that a closed WFF and its negation are both not provable decides this.

[Logik]

The fact that a closed WFF and its negation are both not provable decides this.

I demonstrated this to be erroneous with my Python code.

An error and its negation are not provable. Your grammar doesn't allow me to talk about grammatical and syntax errors errors.
That's why we need meta-languages.

No meta-languages - no meta-cognition
No meta-cognition - no learning.

https://repl.it/repls/BeneficialAlphanu ... awarehouse
# Is an error the same as the logical notion of False?
# Answer: False
# Is an error the same as the logical notion of True?
# Answer: False
# What is the negation of an error?
# Answer: False
# Is the double-negation of an error True?
# Answer: True
# Is the double-negation of an error-object the same as itself?
# Answer: False

[PeteOlcott]

The fact that a closed WFF and its negation are both not provable decides this.

I demonstrated this to be erroneous with my Python code.

An error and its negation are not provable. Your grammar doesn't allow me to talk about errors.
That's why we need meta-languages.

No meta-languages - no meta-cognition
No meta-cognition - no learning.

I spent 18 months designing this ultimate meta-language.
https://www.researchgate.net/publicatio ... y_YACC_BNF

You can talk about errors. More importantly you can detect ALL errors.

What you cannot do is form undecidable sentences. The whole idea of
undecidable sentences was merely an artifact of insufficiently expressive
formal systems.