Is there a sentence that proves itself is not provable?

[PeteOlcott]

Like I said OUT-OF-SCOPE. I break his whole proof right here:

What does "out of scope" mean? I have given you an algorithm which satisfies the requirement which you put forth.

True(F, G) ↔ ~(F ⊢ G)

The Ruby algorithm I gave you satisfies the above.

If that's "out of scope" then give me a formal expression that you want satisfied and I will give you an algorithm for it.

Undecidability can no longer be expressed in any
formal system having these Truth Predicate Axioms:
(1) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
(2) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (~True(F, x) ↔ ~(F ⊢ x))

[Scott Mayers]

Like I said OUT-OF-SCOPE. I break his whole proof right here:

What does "out of scope" mean? I have given you an algorithm which satisfies the requirement which you put forth.

True(F, G) ↔ ~(F ⊢ G)

The Ruby algorithm I gave you satisfies the above.

If that's "out of scope" then give me a formal expression that you want satisfied and I will give you an algorithm for it.

Undecidability can no longer be expressed in any
formal system having these Truth Predicate Axioms:
(1) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
(2) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (~True(F, x) ↔ ~(F ⊢ x))

These appear only to 'define' what Truth means: that it is an agreement between asserting that if GIVEN (x is true) and CONCLUDING, (x is a valid conclusion)

If these aren't used of the judging system, then it has to either be assumed apriori or the system you use to judge what is or is not decidable is TRIVIAL. What claim can you make about what is or is not 'true' of your own counter-thesis if you don't have in mind some meaning of 'truth'? The system of judgement must be proved 'sound' by defining its conclusions valid WHEN something input of the premises are considered as 'true'. If not, then you only default to assuming any input as indeterminately true or false hopelessly.

[PeteOlcott]

What does "out of scope" mean? I have given you an algorithm which satisfies the requirement which you put forth.


The Ruby algorithm I gave you satisfies the above.

If that's "out of scope" then give me a formal expression that you want satisfied and I will give you an algorithm for it.

Undecidability can no longer be expressed in any
formal system having these Truth Predicate Axioms:
(1) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
(2) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (~True(F, x) ↔ ~(F ⊢ x))

These appear only to 'define' what Truth means: that it is an agreement between asserting that if GIVEN (x is true) and CONCLUDING, (x is a valid conclusion)

If these aren't used of the judging system, then it has to either be assumed apriori or the system you use to judge what is or is not decidable is TRIVIAL. What claim can you make about what is or is not 'true' of your own counter-thesis if you don't have in mind some meaning of 'truth'? The system of judgement must be proved 'sound' by defining its conclusions valid WHEN something input of the premises are considered as 'true'. If not, then you only default to assuming any input as indeterminately true or false hopelessly.

When-so-ever these axioms are added to any formal system capable of expressing
them and we anchor their notion of formalized truth in these axioms:
(1) We do what Tarski "proved" was impossible.
(2) Utterly eliminate undecidability from being expressed in any of these formal systems.

This simply becomes false:
∃F ∈ Formal_Systems ∃G ∈ WFF(F) (G ↔ ~(F ⊢ G))

[Scott Mayers]

Undecidability can no longer be expressed in any
formal system having these Truth Predicate Axioms:
(1) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
(2) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (~True(F, x) ↔ ~(F ⊢ x))

These appear only to 'define' what Truth means: that it is an agreement between asserting that if GIVEN (x is true) and CONCLUDING, (x is a valid conclusion)

If these aren't used of the judging system, then it has to either be assumed apriori or the system you use to judge what is or is not decidable is TRIVIAL. What claim can you make about what is or is not 'true' of your own counter-thesis if you don't have in mind some meaning of 'truth'? The system of judgement must be proved 'sound' by defining its conclusions valid WHEN something input of the premises are considered as 'true'. If not, then you only default to assuming any input as indeterminately true or false hopelessly.

When-so-ever these axioms are added to any formal system capable of expressing
them and we anchor their notion of formalized truth in these axioms:
(1) We do what Tarski "proved" was impossible.
(2) Utterly eliminate undecidability from being expressed in any of these formal systems.

This simply becomes false:
∃F ∈ Formal_Systems ∃G ∈ WFF(F) (G ↔ ~(F ⊢ G))

This statement doesn't make sense out of context. To be 'fair' it appears to be saying that there EXISTS some G that is defined as "not true" about some 'condition' of some formal system. IF the context was about comparing ALL possible functions, then such an F is just not-complete of all possible Fs.

In (3) above, you have a definition of the "~True" concept to imply "Something 'true' is 'false'", not that something is just "not-true".

(G ↔ ~(F ⊢ G)) is identical to G iff not(if F then G)

not(if F then G) is equal to not-(not-F or G) == not-F & G,

So,

G == ~F & G

Adding 'existence' quantifiers,

There exists some system G that is not one that is a well-formed.

I'd need clarification of what you interpret those statements to mean. If what I interpreted is wrong by you, can you express in English what each of your (1), (2), and (3) mean first?

[Scott Mayers]

It might help if you took a step back to provide a little primary tutorial of the systems Tarski uses. If it happens to be the case your own tutorial is incorrect to the actual Tarski's explanation, we might be able to find agreement to your own interpretation even if it might be in error to the actual explanation. This wouldn't mean that your interpretation of him is wrong but it might help us here to first understand you FROM your perspective FIRST before we could check to see if Tarski's explanation is or is not correct.

[PeteOlcott]

These appear only to 'define' what Truth means: that it is an agreement between asserting that if GIVEN (x is true) and CONCLUDING, (x is a valid conclusion)

If these aren't used of the judging system, then it has to either be assumed apriori or the system you use to judge what is or is not decidable is TRIVIAL. What claim can you make about what is or is not 'true' of your own counter-thesis if you don't have in mind some meaning of 'truth'? The system of judgement must be proved 'sound' by defining its conclusions valid WHEN something input of the premises are considered as 'true'. If not, then you only default to assuming any input as indeterminately true or false hopelessly.

When-so-ever these axioms are added to any formal system capable of expressing
them and we anchor their notion of formalized truth in these axioms:
(1) We do what Tarski "proved" was impossible.
(2) Utterly eliminate undecidability from being expressed in any of these formal systems.

This simply becomes false:
∃F ∈ Formal_Systems ∃G ∈ WFF(F) (G ↔ ~(F ⊢ G))

This statement doesn't make sense out of context. To be 'fair' it appears to be saying that there EXISTS some G that is defined as "not true" about some 'condition' of some formal system. IF the context was about comparing ALL possible functions, then such an F is just not-complete of all possible Fs.

In (3) above, you have a definition of the "~True" concept to imply "Something 'true' is 'false'", not that something is just "not-true".

(G ↔ ~(F ⊢ G)) is identical to G iff not(if F then G)

not(if F then G) is equal to not-(not-F or G) == not-F & G,

So,

G == ~F & G

Adding 'existence' quantifiers,

There exists some system G that is not one that is a well-formed.

I'd need clarification of what you interpret those statements to mean. If what I interpreted is wrong by you, can you express in English what each of your (1), (2), and (3) mean first?

Forget what I said about G that is way too much for you to handle
until after you totally understand this part:

I came up with a slight change to how formal systems are defined
that totally eliminates undecidability in all these formal systems.

In other words it is a slight change that makes all formal systems
both complete and consistent.

[Scott Mayers]

Let me give you a start: What is a well-formed-formula?

A "formula" is any sequence of symbols of a given set. If we have a system of symbols = {S(1), S(2), S(3)}

Then the possible "formulas" are,

S(1)S(2)S(3)
S(1)S(3)S(2)
S(2)S(1)S(3)
S(2)S(3)S(1)
S(3)S(1)S(2)
S(3)S(2)S(1)

We assume some ordered set of linear symbols. We don't allow spaces between the expressions because we treat the 'space' itself as a possible 'symbol'. Thus the symbols need to be 'typed' as either constants, variables, or punctuation. Some systems use no constants except for some minimal set of operators, like those of {and, or, not}. If we used these three in the simpler symbols, {&,v, -} with a simple punctuation set of {;, (, )} and any set of variable letters, {P, Q, R}, we have a full set of symbols,

Symbol set = {&, v, -, ;, (, ), P, Q, R}

Then this set, treating the commas here as only symbol separators, we have nine symbols and these can be expressed in many different sequents. The "well-formed-formulas" are then those unique subset of all possible sequents that are allowed in the system being defined:

Rules of WWF of some system we'll call "System-1"
(1) Each formula must begin with a ";" and end in a ";"
(2) Any P, Q, or R surrounded by the ";" from rule (1) is a well-formed-formula. [Ex: ";P;", ";Q;", or ";R;")
(3) Any well-formed formula that has more than the three symbol forms in (2) have to be surrounded by '(' and ')' but by convention is understood contained in the expressions of (2) without them.
(4) any (2) with a preceding, "-", such as ";-P;" is a well-formed formula
(5) any of (3) with a preceding, "-", such as ";(-P);" is a well-formed formula
(6) any of '&', or 'v' must be expressed in between two other well-formed formulas to be a well-formed-formula

This may not be complete but is just an example of what it means to spell out what is or is not well-formed. It is to differentiate between,

PP;R [not a well-formed-formula]
;(P&P); [a well-formed formula]
etc.

So you can have systems that are well-formed, some well-formed with other formulas possibly expressible that are not, or all that are not well-formed, which just means that the system is undefined.

[Scott Mayers]

Forget what I said about G that is way too much for you to handle
until after you totally understand this part:

I came up with a slight change to how formal systems are defined
that totally eliminates undecidability in all these formal systems.

In other words it is a slight change that makes all formal systems
both complete and consistent.

Sure. I just added the above about 'well-formed-formulas' so that if anyone is wondering what "WFF" is about. Note that that added point seems superfluous and meaningless to readers without this 'tutorial'.

So you define all "formal systems" as ones that REQUIRE the 'well-formed-formula'? I presumed it was essential and why it seems odd to add that unless there are "formal systems" without concern to its 'syntax' and/or 'grammar'. Note also that you can ONLY have a system with at least one 'well-formed' definition and one 'non-well-formed' definition or the system is undefined or without rules.


Can you define a "formal system"?

[PeteOlcott]

Forget what I said about G that is way too much for you to handle
until after you totally understand this part:

I came up with a slight change to how formal systems are defined
that totally eliminates undecidability in all these formal systems.

In other words it is a slight change that makes all formal systems
both complete and consistent.

Sure. I just added the above about 'well-formed-formulas' so that if anyone is wondering what "WFF" is about. Note that that added point seems superfluous and meaningless to readers without this 'tutorial'.

So you define all "formal systems" as ones that REQUIRE the 'well-formed-formula'? I presumed it was essential and why it seems odd to add that unless there are "formal systems" without concern to its 'syntax' and/or 'grammar'. Note also that you can ONLY have a system with at least one 'well-formed' definition and one 'non-well-formed' definition or the system is undefined or without rules.


Can you define a "formal system"?

If you want to get 100% specific, this YACC BNF specifies all the WFF
of a language equivalent to HOL with types and a provability predicate:
https://www.researchgate.net/publicatio ... y_YACC_BNF

Curry calls a formal system a theory:
http://liarparadox.org/Haskell_Curry_45.pdf

[Logik]

Undecidability can no longer be expressed in any
formal system having these Truth Predicate Axioms:
(1) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (True(F, x) ↔ (F ⊢ x))
(2) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (False(F, x) ↔ (F ⊢ ~x))
(3) ∀F ∈ Formal_Systems ∀x ∈ WFF(F) (~True(F, x) ↔ ~(F ⊢ x))

WFF(F) -> {True, False}. Hence: a decision problem.

I am not sure at which point you will recognize that what you are (re)inventing is called a compiler/interpreter.

[Logik]

Curry calls a formal system a theory:
http://liarparadox.org/Haskell_Curry_45.pdf

The moment any "theory" becomes Turing-complete it becomes constructive.

The pre-existing syntax/grammar/semantic rules can simply be bypassed, or used to compose/construct new ones.

Try as hard as you want to enforce arbitrarily-specified rules - reality doesn't care about man-made authorities.