Discussion:
Refuting Incompleteness and Undefinability Version(6)
Add Reply
peteolcott
2018-10-27 22:35:31 UTC
Reply
Permalink
This universal Truth predicate rejects as malformed any expressions of language that would otherwise show Incompleteness or Undefinability.

∀x ∈ L True(L, x) ↔ Theorem(L, x).
For all expressions x in language L, x is True in L if and only if x is a Theorem of L

https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness
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 Fall 2018)

Formalized as: G ↔ G ∈ F ~Provable(F, G)
True(F, G) ↔ Theorem(F, G)
False(F, G) ↔ Theorem(F, ~G)

“This sentence is not provable”
G ↔ ~Provable(G) // To avoid clutter F is implied rather than stated

If G was a Theorem then since G is ~Provable(G)
Provable(G) would be contradicted therefore G is not a Theorem.

If ~G was a Theorem then since ~G is Provable(G)
Provable(~G) would be contradicted therefore ~G is not a Theorem.

Copyright 2018 Pete Olcott
peteolcott
2018-10-28 01:46:19 UTC
Reply
Permalink
Post by peteolcott
This universal Truth predicate rejects as malformed any expressions of language that would otherwise show Incompleteness or Undefinability.
∀x ∈ L True(L, x) ↔ Theorem(L, x).
For all expressions x in language L, x is True in L if and only if x is a Theorem of L
Oh sweetie. Bless your heart.
Post by peteolcott
True(F, G) ↔ Theorem(F, G)
False(F, G) ↔ Theorem(F, ~G)
Presumably, you intend "True()" and "False()" to be predicates in F, rather than from a higher metalanguage M, where truth is actually evaluated.
Simply labelling the provability predicate and its negation as "True()" and "False()" in F is not a proof that they correspond to actual truth and falsity as evaluated in M.
Labels are not proofs. Without a proof of equivalence, it would be just as meaningful to label your predicates "Fuzzy()" and "Smooth()", or "Predicate1()" and "Predicate2()", or "Intelligent()" and "Olcott()".
You have a good point EXCEPT:

When we hypothesize that True(L, x) ↔ Theorem(L, x)
and thus False(L, x) ↔ Theorem(L, ~x) we find that we now
have a corresponding pair of predicates in L that reject
all expressions of L that previously "proved"
Incompleteness or Undefinability in L.

∀L ∈ Formal_System ∀x ∈ L True(L, x) ↔ Theorem(L, x)

Copyright 2018 Pete Olcott
peteolcott
2018-10-28 02:58:56 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
This universal Truth predicate rejects as malformed any expressions of language that would otherwise show Incompleteness or Undefinability.
∀x ∈ L True(L, x) ↔ Theorem(L, x).
For all expressions x in language L, x is True in L if and only if x is a Theorem of L
Oh sweetie. Bless your heart.
Post by peteolcott
True(F, G) ↔ Theorem(F, G)
False(F, G) ↔ Theorem(F, ~G)
Presumably, you intend "True()" and "False()" to be predicates in F, rather than from a higher metalanguage M, where truth is actually evaluated.
Simply labelling the provability predicate and its negation as "True()" and "False()" in F is not a proof that they correspond to actual truth and falsity as evaluated in M.
Labels are not proofs. Without a proof of equivalence, it would be just as meaningful to label your predicates "Fuzzy()" and "Smooth()", or "Predicate1()" and "Predicate2()", or "Intelligent()" and "Olcott()".
When we hypothesize that True(L, x) ↔ Theorem(L, x)
and thus False(L, x) ↔ Theorem(L, ~x) we find that we now
have a corresponding pair of predicates in L
No, there is only one predicate in L: Provable(). You just assigned it a second label in L "True()". You literally defined them to be equivalent in L.. They have exactly the same extensional meaning.
As I pointed out, this relabelling tells us nothing at all about actual truth, since that is evaluated in the metalanguage M.
EFQ
I keep seeing the validity of where you are coming from.

Theorem(L, x) ⊆ Provable(L, x)

All that I have done is taken the subset of Provable expressions x of language
L such that the Mendelson members of Γ are called the hypotheses or premisses
of the proof are empty and labeled this subset of expressions True(L, x).

This by itself really tells us nothing much at all.
This by itself is nothing more than a dictatorial decree.

The interesting part comes in when we test the hypothesis of:
∀x ∈ L True(L, x) ↔ Theorem(L, x)

Does the corresponding pair of predicates:
True(L, x) ↔ Theorem(L, x)
False(L, x) ↔ Theorem(L, ~x)
always reject expressions of language that have previously been shown
to "prove" Incompleteness and Undefinability ?

LP ↔ ~Theorem(L, LP)

Here is the simplest possible example:
LP ↔ ~Theorem(LP) // L is implied rather than specified to avoid clutter

If LP was a Theorem then since LP is ~Theorem(LP) then
Theorem(LP) would be contradicted therefore LP is not a Theorem.

If ~LP was a Theorem then since ~LP is Theorem(LP) then
Theorem(~LP) would be contradicted therefore ~LP is not a Theorem.

Since it is neither True nor False that LP is a Theorem,
then LP is decided to be a malformed logical proposition.

At least many of the set of "undecidable" decision problems
can be decided this same way.

Copyright 2018 Pete Olcott
peteolcott
2018-10-28 06:09:52 UTC
Reply
Permalink
Post by peteolcott
All that I have done is taken the subset of Provable expressions x of language
L such that the Mendelson members of Γ are called the hypotheses or premisses
of the proof are empty and labeled this subset of expressions True(L, x).
That subset already has a name: theorems. Giving it another name is pointless, and it certain doesn't magically imbue that subset with the property suggested by the second name.
Post by peteolcott
LP ↔ ~Theorem(LP) // L is implied rather than specified to avoid clutter
You still haven't specified the syntax of ↔ in your formal language, nor its compositional truth in the metalanguage.
This has already been done for standard logical notation, but when you introduce your own idiosyncratic connective, you *must* define its syntax and semantics. Until you do, it's just gibberish.
The problem is, you've set this u in such a way that you're going to need WFFs to have the ability to directly reference themselves, which is a no-no. This is why Gödel numbering is so crucial.
Post by peteolcott
If LP was a Theorem then since LP is ~Theorem(LP) then
Theorem(LP) would be contradicted therefore LP is not a Theorem.
This is a hopeless confusing of syntax and semantics, ad formal language and metalanguage.
No it is a formalization of the Liar Paradox substituting ~Theorem(LP) for ~True(LP).
Being a theorem in a formal language doesn't INHERENTLY tell you anything about its truth in the metalanguage. Theorems and nontheorems can be true or false, depending on how the truth values are computed in the metalanguage. It is useful to have, at minimum, a metalanguage in which all theorems are true, but that isn't an requirement on metalanguages.
What is actually going on is that LP says it isn't a theorem in the formal language. LP is either true or false in the metalanguage, so we have two cases to consider.
Case #1: Suppose LP is false. Then LP would be a theorem. But we don't want a formal language in which theorems are interpreted as true (that isn't a contradiction, just not a useful formal language).
Case #2: Suppose LP is true. Then LP would not be a theorem, as you just proved above. No contradiction.
Of the two cases, one isn't very useful and the other is perfectly okay, so there is no problem. If we want a useful formal language, then LP is clearly true but also not a theorem.
EFQ
The whole idea of requiring a separate meta-language for formal languages was always misdirection and incorrect.

Every language speaks for itself. Its own Axioms and rules-of-inference provide everything required to decide True(L,x) entirely on the basis of Theorem(L, x).

G ∈ Peano_Arithmetic ~Provable(Peano_Arithmetic, G) // error no such predicate in PA

Universal Truth Predicate:
∀L ∈ Formal_Systems ∀x ∈ L True(L, x) ↔ Theorem(L, x)

∀L ∈ Formal_Systems
∀x ∈ L (~Theorem(L, x) ∧ ~Theorem(L, ~x)) ↔ ~Boolean_Proposition(L, x)

Copyright 2018 Pete Olcott
peteolcott
2018-10-29 21:53:49 UTC
Reply
Permalink
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
EFQ
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x) that
decides whether or not x (or ~x) is a Theorem of L.

∀L ∈ Formal_System ∀x ∈ L
(Theorem(L, x) ∨ Theorem(L, ~x)) ↔ Boolean_Proposition(L, x)

We don't even need True and False the above formula accepts every
Boolean_Proposition and thus rejects every expression of language
that would otherwise show either Incompleteness or Undefinability.

LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

If LiarParadox was a theorem of F this contradicts its assertion: ~Theorem(F, LiarParadox)
If ~LiarParadox was a theorem of F this contradicts its assertion: Theorem(F, LiarParadox)
∴ ~Boolean_Proposition(F, LiarParadox)

Copyright 2018 Pete Olcott
peteolcott
2018-10-29 23:15:04 UTC
Reply
Permalink
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
EFQ
G ↔ ∃G ∈ F ~Provable(F, G)

Ah but you are wrong:
Once L decides that closed WFF x is Gibberish(L, x) it concludes:

~True(L, x) ∧ ~False(L, x) ∧ ~Provable(L, x) ∧ ~Refutable(L, x)

∀L ∈ Formal_System ∀x ∈ L
(~Theorem(L, x) ∧ ~Theorem(L, ~x)) ↔ Gibberish(L, x)

Copyright 2018 Pete Olcott
peteolcott
2018-10-29 23:35:49 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
EFQ
G ↔ ∃G ∈ F ~Provable(F, G)
~True(L, x) ∧ ~False(L, x) ∧ ~Provable(L, x) ∧ ~Refutable(L, x)
∀L ∈ Formal_System ∀x ∈ L
(~Theorem(L, x) ∧ ~Theorem(L, ~x)) ↔ Gibberish(L, x)
Copyright 2018 Pete Olcott
Although incomplete formal systems are possible they are not necessary.

https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem#More_general_form
...it follows that T ⊨ s ↔ T ⊢ s, and thus that syntactic and semantic
consequence are equivalent for first-order logic...
peteolcott
2018-10-30 19:01:03 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
EFQ
G ↔ ∃G ∈ F ~Provable(F, G)
~True(L, x) ∧ ~False(L, x) ∧ ~Provable(L, x) ∧ ~Refutable(L, x)
∀L ∈ Formal_System ∀x ∈ L
(~Theorem(L, x) ∧ ~Theorem(L, ~x)) ↔ Gibberish(L, x)
Copyright 2018 Pete Olcott
Although incomplete formal systems are possible they are not necessary.
https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem#More_general_form
...it follows that T ⊨ s ↔ T ⊢ s, and thus that syntactic and semantic
consequence are equivalent for first-order logic...
Yes, you've been told this many times.
We already know this because we have read the literature and actually understand it.
EFQ
I said it better this time:

You know that
G ↔ ∃G ∈ F ~Provable(F, G)

Can be decided on the basis of the satisfaction of its Gibberish(F, G) predicate:
∀Closed-WFF(G) ∈ F (~Theorem(F, G) ∧ ~Theorem(F, ~G)) ↔ Gibberish(F, G)

Gibberish(F, G) ↔ ~True(F, G) ∧ ~False(F, G) ∧ ~Provable(F, G) ∧ ~Refutable(F, G)

It seems that you are diligently searching for some little thing to disagree
with and ignoring the rest of what I say. This would be dishonest.

Copyright 2018 Pete Olcott
peteolcott
2018-10-30 18:52:38 UTC
Reply
Permalink
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
N, you still don't get it.
Tarksi's undefinability theorem says that there is no predicate in L that corresponds exactly to the standard notion of truth in the metalanguage (model).
You can't "refute" Tarksi by creating a new predicate in the metalanguage that is different from standard truth.
You can't "refute" Tarksi by just ignoring the standard notion of truth in the metalanguage.
In order to refute Tarski Undefinability we must also refute his
fundamental underlying assumptions.

As long as a language L contains the following predicate Theorem(L, x)
for every closed WFF x in L, then L is sufficiently expressive to make
Incompleteness and Undefinability impossible.

If the above hypothesis is true, then it also correctly rejects the notion
of the requirement of a separate metalanguage, thus correcting the erroneous
standard model of Truth.

Copyright 2018 Pete Olcott
peteolcott
2018-10-31 04:34:48 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
N, you still don't get it.
Tarksi's undefinability theorem says that there is no predicate in L that corresponds exactly to the standard notion of truth in the metalanguage (model).
You can't "refute" Tarksi by creating a new predicate in the metalanguage that is different from standard truth.
You can't "refute" Tarksi by just ignoring the standard notion of truth in the metalanguage.
In order to refute Tarski Undefinability we must also refute his
fundamental underlying assumptions.
No, if there is a proof from X to Y, you can't "refute" that proof by choosing Z instead of X. The only way to refute that proof is to use the same starting assumptions (X) and derive ~Y.
If you change the starting assumptions, you are not saying anything at all about the original proof.
How do you STILL not understand this basic concept?
EFQ
Technically you are correct. If he started with false premises and
used correct inference on the basis of these false premises then I
would not be actually refuting his proof.

If I show that his final conclusion is contradicted, then it does
not matter where his error lies, I have proved him to be incorrect.
peteolcott
2018-10-31 15:38:11 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
Which can be enormously simplified by saying that the syntax,
rules-of-inference, and axioms of arithmetic prove: Theorem(arithmetic, "2+2=4") is satisfied.
You HAVE to specify the metalanguage you are interpreting truth in, and how it is being interpreted. You haven't done that.
You continue to hold on to a false basis. The only actual metalanguage
that is ever needed (if any) is the single predicate Theorem(L, x)
If that's in the metalanguage, then it has absolutely nothing to do with Tarksi's undefinability.
The whole point of Tarski's claim is that you can't have a predicate ***** IN L ***** that corresponds to truth in the metalanguage.
Clearly, you STILL don't understand what your'e talking about.
N, you still don't get it.
Tarksi's undefinability theorem says that there is no predicate in L that corresponds exactly to the standard notion of truth in the metalanguage (model).
You can't "refute" Tarksi by creating a new predicate in the metalanguage that is different from standard truth.
You can't "refute" Tarksi by just ignoring the standard notion of truth in the metalanguage.
In order to refute Tarski Undefinability we must also refute his
fundamental underlying assumptions.
No, if there is a proof from X to Y, you can't "refute" that proof by choosing Z instead of X. The only way to refute that proof is to use the same starting assumptions (X) and derive ~Y.
If you change the starting assumptions, you are not saying anything at all about the original proof.
How do you STILL not understand this basic concept?
Technically you are correct.
I and every one else here have been correct every single time we've told you this.
Post by peteolcott
If he started with false premises
.... then you would be able to derive the opposite of his conclusion, thus refuting him.
That's why you have to start with his assumptions, and see what you can derive from that.
Changing the assumptions of a proof tells you nothing about the validity of the proof.
Post by peteolcott
If I show that his final conclusion is contradicted,
.... USING HIS STARTING ASSUMPTIONS ...
Post by peteolcott
then it does
not matter where his error lies, I have proved him to be incorrect.
EFQ
It seem to you do not comprehend the crucial distinction between sound deduction and valid deduction:

Validity and Soundness https://www.iep.utm.edu/val-snd/
A deductive argument is said to be valid if and only if it takes a form that makes it
impossible for the premises to be true and the conclusion nevertheless to be false.
Otherwise, a deductive argument is said to be invalid.

A deductive argument is sound if and only if it is both valid, and all of its premises
are actually true. Otherwise, a deductive argument is unsound.

As long as I show that Tarski's conclusion is contradicted then I have proven him to be incorrect no matter what his premises or reasoning was.

Introduction to Mathematical logic Sixth edition Elliott Mendelson
1.4 An Axiom System for the Propositional Calculus
A wf C is said to be a consequence in S of a set Γ of wfs if and only if there is a
sequence B1, …, Bk of wfs such that C is Bk and, for each i, either Bi is an axiom
or Bi is in Γ, or Bi is a direct consequence by some rule of inference of some of
the preceding wfs in the sequence. Such a sequence is called a proof (or deduction)
of C from Γ. The members of Γ are called the hypotheses or premisses of the proof.
We use Γ ⊢ C as an abbreviation for “C is a consequence of Γ”...

If Γ is the empty set ∅, then ∅ ⊢ C if and only if C is a theorem. It is customary
to omit the sign “∅” and simply write ⊢ C. Thus, ⊢ C is another way of asserting that
C is a theorem.

Even if Γ ⊢ C is satisfied, I only have to prove ⊢~C to prove that Tarski is wrong.

Copyright 2018 Pete Olcott
peteolcott
2018-10-31 18:27:07 UTC
Reply
Permalink
Post by peteolcott
As long as I show that Tarski's conclusion is contradicted
BY ASSUMING HIS STARTING ASSUMPTIONS!!!
You can't just create a random proof with completely different assumptions.
"Tarksi proved that assuming X leads to Y. But I'm assuming ~Y, and from that, I can derive ~Y. Therefore, I have proved him wrong by deriving a contradiction!"
Even you should be able to see how useless that is.
EFQ
It seems that you are failing to understand a fundamental aspect of formal proof:

if Γ ⊢ C is satisfied, and ⊢~C is satisfied ∴ ~True(Γ), and thus Unsound(Γ ⊢ C)

A deductive argument is sound if and only if it is both valid, and all of its premises
are actually true. Otherwise, a deductive argument is unsound.

Copyright 2018 Pete Olcott

I am so happy that I finally totally understand the conventional terms of
the art and notation so that I can say exactly and precisely what I have
been diligently striving to say in many thousands of posts since 1997,
using these terms and symbols 100% exactly according to their conventional
meaning.

This would have never happened if my reviewers did not form such an excellent
genetic algorithm fitness function to evolve my hit and miss ideas into their
current form.
peteolcott
2018-10-31 19:10:09 UTC
Reply
Permalink
Post by peteolcott
As long as I show that Tarski's conclusion is contradicted
BY ASSUMING HIS STARTING ASSUMPTIONS!!!
You can't just create a random proof with completely different assumptions.
"Tarksi proved that assuming X leads to Y. But I'm assuming ~Y, and from that, I can derive ~Y. Therefore, I have proved him wrong by deriving a contradiction!"
Even you should be able to see how useless that is.
I understand it very well.
if Γ ⊢ C is satisfied, and ⊢~C is satisfied ∴ ~True(Γ), and thus Unsound(Γ ⊢ C)
This isn't applicable, because you are making different assumptions Γ'..
Tarksi has Γ ⊢ C, you have Γ' ⊢ ~C, where, crucially, your Γ' basically contains ~C already.
EFQ
⊢Tarski(~C) is satisfied ∴ Tarski(Γ ⊢ C) is unsatisfied

See if you can directly find any fault what-so-ever with the following
simplest possible formalization of the simplest possible concrete example:

LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

If LiarParadox was a theorem of F this contradicts its assertion: ~Theorem(F, LiarParadox)

If ~LiarParadox was a theorem of F this contradicts its assertion: Theorem(F, LiarParadox)

∴ ~Boolean_Proposition(F, LiarParadox)

Copyright 2018 Pete Olcott
peteolcott
2018-10-31 21:40:31 UTC
Reply
Permalink
Post by peteolcott
See if you can directly find any fault what-so-ever
I have, and I've pointed out the faults numerous times.
Just because you don't understand them, or just ignore them, doesn't invalidate them.
EFQ
Yet since this is something new you have not yet shown any faults in its
actual reasoning. The best that you have done is simply state that we do
not typically look at these things in this way.

Since this is the simplest possible formalization of the simplest possible
example of Incompleteness / Undefinability I must keep a single-minded focus
on requesting specific rebuttals of its specific reasoning.

LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

If LiarParadox was a theorem of F this contradicts its assertion: ~Theorem(F, LiarParadox)

If ~LiarParadox was a theorem of F this contradicts its assertion: Theorem(F, LiarParadox)

∴ ~Boolean_Closed_WFF(F, LiarParadox)

Copyright 2018 Pete Olcott
peteolcott
2018-11-01 01:07:49 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
See if you can directly find any fault what-so-ever
I have, and I've pointed out the faults numerous times.
Just because you don't understand them, or just ignore them, doesn't invalidate them.
Yet since this is something new
The faults are the same. You are trying to "refute" a proof by fundamentally changing the crucial definitions and assumptions of the original proof.
That simply isn't how refutation of a proof works. It CAN'T work that way. Otherwise, you'd just define your desired conclusion to be true (which is, essentially, what you have done).
Tarksi proves that you cannot create a predicate in L that corresponds to how truth works in the standard model M. You cannot refute him by completely ignoring how truth works in M. You are just trying to redefine the word "truth" to mean something else entirely, so you aren't saying anything at all about Tarski.
If you want to refute Tarksi, you HAVE TO USE HIS NOTION OF TRUTH, because that is what his proof is about.
If you don't want to work with his notion of truth, then you can't refute him.
EFQ
Forget that I am trying to refute anything, simply examine the following
reasoning in isolation and see if you can find any mistakes:

LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

If LiarParadox was a theorem of F this contradicts its assertion: ~Theorem(F, LiarParadox)

If ~LiarParadox was a theorem of F this contradicts its assertion: Theorem(F, LiarParadox)

∴ ~Boolean_Closed_WFF(F, LiarParadox)

Copyright 2018 Pete Olcott
peteolcott
2018-11-01 04:02:30 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
See if you can directly find any fault what-so-ever
I have, and I've pointed out the faults numerous times.
Just because you don't understand them, or just ignore them, doesn't invalidate them.
Yet since this is something new
The faults are the same. You are trying to "refute" a proof by fundamentally changing the crucial definitions and assumptions of the original proof.
That simply isn't how refutation of a proof works. It CAN'T work that way. Otherwise, you'd just define your desired conclusion to be true (which is, essentially, what you have done).
Tarksi proves that you cannot create a predicate in L that corresponds to how truth works in the standard model M. You cannot refute him by completely ignoring how truth works in M. You are just trying to redefine the word "truth" to mean something else entirely, so you aren't saying anything at all about Tarski.
If you want to refute Tarksi, you HAVE TO USE HIS NOTION OF TRUTH, because that is what his proof is about.
If you don't want to work with his notion of truth, then you can't refute him.
Forget that I am trying to refute anything,
Good.
Post by peteolcott
simply examine the following reasoning
I can't. You haven't provided a model in which to interpret your syntax. You are presumably not using the standard model, since you seem adverse to Tarski's notion of truth, so you have to define your model.
EFQ
LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

LiarParadox is a propositional variable.
~ means Boolean negation.
↔ means logical equivalence.
∈ means member of.
, separates arguments of a predicate
() delimits the argument portion of a predicate
F is any arbitrary formal language having a Theorem predicate()

Theorem is the Mendelson meaning of Theorem thus specifying
the semantics of the satisfaction of the Theorem predicate.

You are telling me that you had no idea of any of this?
peteolcott
2018-11-01 04:21:17 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
Post by peteolcott
See if you can directly find any fault what-so-ever
I have, and I've pointed out the faults numerous times.
Just because you don't understand them, or just ignore them, doesn't invalidate them.
Yet since this is something new
The faults are the same. You are trying to "refute" a proof by fundamentally changing the crucial definitions and assumptions of the original proof.
That simply isn't how refutation of a proof works. It CAN'T work that way. Otherwise, you'd just define your desired conclusion to be true (which is, essentially, what you have done).
Tarksi proves that you cannot create a predicate in L that corresponds to how truth works in the standard model M. You cannot refute him by completely ignoring how truth works in M. You are just trying to redefine the word "truth" to mean something
else entirely, so you aren't saying anything at all about Tarski.
If you want to refute Tarksi, you HAVE TO USE HIS NOTION OF TRUTH, because that is what his proof is about.
If you don't want to work with his notion of truth, then you can't refute him.
Forget that I am trying to refute anything,
Good.
Post by peteolcott
simply examine the following reasoning
I can't. You haven't provided a model in which to interpret your syntax. You are presumably not using the standard model, since you seem adverse to Tarski's notion of truth, so you have to define your model.
EFQ
LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)
LiarParadox is a propositional variable.
~ means Boolean negation.
↔ means logical equivalence.
∈ means member of.
, separates arguments of a predicate
() delimits the argument portion of a predicate
F is any arbitrary formal language having a Theorem predicate()
Theorem is the Mendelson meaning of Theorem thus specifying
the semantics of the satisfaction of the Theorem predicate.
You are telling me that you had no idea of any of this?
X ↔ Theorem(English, "a dog is not a type of cat")

Theorem(English, "a dog is not a type of cat") is true
"a dog is not a type of cat" ∈ English is true
"a dog is not a type of cat" ∈ Declarative_Sentence(English) is true
"what time is it?" ∈ English is true
"what time is it?" ∈ Declarative_Sentence(English) is false
"how are are are?" ∈ English is false

Copyright 2018 Pete Olcott
DKleinecke
2018-11-01 17:37:34 UTC
Reply
Permalink
Theorem(English, "a dog is not a type of cat") is true
"a dog is not a type of cat" ∈ English is true
"a dog is not a type of cat" ∈ Declarative_Sentence(English) is true
"what time is it?" ∈ English is true
"what time is it?" ∈ Declarative_Sentence(English) is false
"how are are are?" ∈ English is false
We cannot understand the first three sentences until
you define what YOU mean by "type" - they are
not comprehensible English otherwise.

I gather you mean to say that "English" is a set of
sentences and "Declarative_Sentence(English)" is a
subset of English. Your last "sentence" shows you
believe there are sentences(?) that are not in
English. Perhaps what you are working with is strings
of words rather than sentences. That is, English is
a set of word strings, etc. Of course a definition of
word must proceed all this.
peteolcott
2018-11-01 19:12:47 UTC
Reply
Permalink
Post by DKleinecke
Theorem(English, "a dog is not a type of cat") is true
"a dog is not a type of cat" ∈ English is true
"a dog is not a type of cat" ∈ Declarative_Sentence(English) is true
"what time is it?" ∈ English is true
"what time is it?" ∈ Declarative_Sentence(English) is false
"how are are are?" ∈ English is false
We cannot understand the first three sentences until
you define what YOU mean by "type" - they are
not comprehensible English otherwise.
I gather you mean to say that "English" is a set of
sentences and "Declarative_Sentence(English)" is a
subset of English. Your last "sentence" shows you
believe there are sentences(?) that are not in
English.
Syntactically incorrect expressions of English.
Post by DKleinecke
Perhaps what you are working with is strings
of words rather than sentences. That is, English is
a set of word strings, etc. Of course a definition of
word must proceed all this.
I said all the above stuff so that an intuitive understanding
of my proposal would be provided.
DKleinecke
2018-11-02 01:04:13 UTC
Reply
Permalink
Post by peteolcott
Post by DKleinecke
Theorem(English, "a dog is not a type of cat") is true
"a dog is not a type of cat" ∈ English is true
"a dog is not a type of cat" ∈ Declarative_Sentence(English) is true
"what time is it?" ∈ English is true
"what time is it?" ∈ Declarative_Sentence(English) is false
"how are are are?" ∈ English is false
We cannot understand the first three sentences until
you define what YOU mean by "type" - they are
not comprehensible English otherwise.
I gather you mean to say that "English" is a set of
sentences and "Declarative_Sentence(English)" is a
subset of English. Your last "sentence" shows you
believe there are sentences(?) that are not in
English.
Syntactically incorrect expressions of English.
Post by DKleinecke
Perhaps what you are working with is strings
of words rather than sentences. That is, English is
a set of word strings, etc. Of course a definition of
word must proceed all this.
I said all the above stuff so that an intuitive understanding
of my proposal would be provided.
OK - what is your proposal?
peteolcott
2018-11-01 05:16:09 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
Post by peteolcott
Post by peteolcott
See if you can directly find any fault what-so-ever
I have, and I've pointed out the faults numerous times.
Just because you don't understand them, or just ignore them, doesn't invalidate them.
Yet since this is something new
The faults are the same. You are trying to "refute" a proof by fundamentally changing the crucial definitions and assumptions of the original proof.
That simply isn't how refutation of a proof works. It CAN'T work that way. Otherwise, you'd just define your desired conclusion to be true (which is, essentially, what you have done).
Tarksi proves that you cannot create a predicate in L that corresponds to how truth works in the standard model M. You cannot refute him by completely ignoring how truth works in M. You are just trying to redefine the word "truth" to mean something else entirely, so you aren't saying anything at all about Tarski.
If you want to refute Tarksi, you HAVE TO USE HIS NOTION OF TRUTH, because that is what his proof is about.
If you don't want to work with his notion of truth, then you can't refute him.
Forget that I am trying to refute anything,
Good.
Post by peteolcott
simply examine the following reasoning
I can't. You haven't provided a model in which to interpret your syntax.. You are presumably not using the standard model, since you seem adverse to Tarski's notion of truth, so you have to define your model.
LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)
LiarParadox is a propositional variable.
Then the above string is not well-formed. WFFs must have all variables bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.

LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
Jeff Barnett
2018-11-01 17:42:47 UTC
Reply
Permalink
[]
Post by peteolcott
Then the above string is not well-formed. WFFs must have all variables
bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
So what is "FORMAL_SYSTEMS" bound to? No free variables means no free
variables. Get to work and we'll see your hopeless answer 30 years from
now. Get to it.
--
Jeff Barnett
peteolcott
2018-11-01 19:28:43 UTC
Reply
Permalink
 []
Post by peteolcott
Then the above string is not well-formed. WFFs must have all variables bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
So what is "FORMAL_SYSTEMS" bound to? No free variables means no free variables. Get to work and we'll see your hopeless answer 30 years from now. Get to it.
Misspelling of the Latin: ex falso (sequitur) quodlibet (EFQ)
Resulted in the following simplifications:

∀x True(x) ↔ φ(x) // Tarski's Formal correctness of True

These three formulas follow this same pattern:
(1) ∀x ~True(x) ↔ ~⊢x
(2) ∀x True(x) ↔ ⊢x
(3) ∀x False(x) ↔ ⊢~x

∀x Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x)

∀LP ↔ ~⊢LP
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)

Coptright 2018 Pete Olcott
peteolcott
2018-11-01 19:44:30 UTC
Reply
Permalink
 []
Post by peteolcott
Then the above string is not well-formed. WFFs must have all variables bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
So what is "FORMAL_SYSTEMS" bound to? No free variables means no free variables. Get to work and we'll see your hopeless answer 30 years from now. Get to it.
∀x True(x) ↔ φ(x) // Tarski’s Formal correctness of True

These three formulas follow this same pattern: (Simple English follows)
(1) ∀x ~True(x) ↔ ~⊢x // x cannot be proven True from known facts.
(2) ∀x True(x) ↔ ⊢x // x can be proven True from known facts.
(3) ∀x False(x) ↔ ⊢~x // x can be proven False from known facts.

∀x Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x)

∀LP ↔ ~⊢LP
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)

Copyright 2018 Pete Olcott
peteolcott
2018-11-03 16:42:00 UTC
Reply
Permalink
 []
Post by peteolcott
Then the above string is not well-formed. WFFs must have all variables bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
So what is "FORMAL_SYSTEMS" bound to? No free variables means no free variables. Get to work and we'll see your hopeless answer 30 years from now. Get to it.
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 Fall 2018)

The following expression formalizes the above English equivalent:
∀F ∈ Formal_Systems
(
∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)

(G) F ⊢ GF ↔ ~ProvF(⌈GF⌉). (Raatikainen Fall 2018)
Could it be that Kurt Gödel simply forgot the existential quantifier?

∀F ∈ Formal_Systems
(
Z ↔ ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
~Z ↔ ~∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)

(1) ∀x (~True(x) ↔ ~⊢x)
(2) ∀x (True(x) ↔ ⊢x)
(3) ∀x (False(x) ↔ ⊢~x)

If Z is a Theorem in F then there exists G in F that is logically equivalent to its own unprovability.
If ~Z is a Theorem in F then there does not exist G in F that is logically equivalent to its own unprovability.

If G was Provable in F this contradicts its assertion: G is not Provable in F

∴ False(Z) ∧ True(~Z)


Copyright 2018 Pete Olcott

Raatikainen, Panu, "Gödel's Incompleteness Theorems",
The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.),
URL = <https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/>.
Peter Percival
2018-11-03 17:22:15 UTC
Reply
Permalink
Post by Jeff Barnett
  []
Post by peteolcott
Then the above string is not well-formed. WFFs must have all
variables bound by quantifiers. Free variables are not allowed.
EFQ
OK finally some feedback that I can use. I was wondering about that.
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
So what is "FORMAL_SYSTEMS" bound to? No free variables means no free
variables. Get to work and we'll see your hopeless answer 30 years
from now. Get to it.
    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 Fall 2018)
∀F ∈ Formal_Systems
(
  ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it doesn't. You haven't captured "a certain amount of arithmetic" or
"nor disproved". Also, you need to explain your notation - F seems to
be a set (it has elements and subsets) but it is also a formal system.
At the very least you should say what a formal system is.
(G) F ⊢ GF ↔ ~ProvF(⌈GF⌉). (Raatikainen Fall 2018)
Could it be that Kurt Gödel simply forgot the existential quantifier?
Gödel's language didn't allow quantifiers to bind formal systems.
∀F ∈ Formal_Systems
(
   Z ↔  ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
  ~Z ↔ ~∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
(1) ∀x (~True(x) ↔ ~⊢x)
(2) ∀x (True(x)    ↔ ⊢x)
(1) and (2) are the same. Do you not get that?
(3) ∀x (False(x)   ↔ ⊢~x)
If Z is a Theorem in F then there exists G in F that is logically
equivalent to its own unprovability.
If ~Z is a Theorem in F then there does not exist G in F that is
logically equivalent to its own unprovability.
If G was Provable in F this contradicts its assertion: G is not Provable in F
∴ False(Z) ∧ True(~Z)
Copyright 2018 Pete Olcott
Raatikainen, Panu, "Gödel's Incompleteness Theorems",
The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.),
URL =
<https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/>.
peteolcott
2018-11-01 18:53:41 UTC
Reply
Permalink
Post by peteolcott
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
If you want to get rid of "clutter", get rid of the pointless references to "Formal_Systems" and "F", and use the standard symbol ⊢ instead of "Theorem". If you really need to specify theoremhood in a particular formal system, you can put F as a subscript on ⊢, but it's not really necessary, unless you intend to modify the rules of deduction.
Even still, the rest of your weird formula just doesn't work.
∀x True(x) ↔ φ(x) // Tarski's Formal correctness of True
The above example would seem to indicate that the scope of the ∀ applies
equally to the LHS and the RHS, thus ∀x ~True(x) ↔ φ(x) would also be correct.

These three formulas follow this same pattern:
(1) ∀x ~True(x) ↔ ~⊢x
(2) ∀x True(x) ↔ ⊢x
(3) ∀x False(x) ↔ ⊢~x

If we hypothesize that these last two formalize the notion of True(x) and False(x)

and further hypothesize that this is correct
Sentence (mathematical logic) https://en.wikipedia.org/wiki/Sentence_(mathematical_logic)
A sentence ... must be true or false.

Then we can derive this formula on the basis of the above assumptions:
∀x Logic_Sentence(x) ↔ (True(x) ∨ false(x)) ↔ (⊢x ∨ ⊢~x)

Within these assumptions we can determine that any expression of
language x that satisfies this predicate Logic_Sentence(x) are
sentences of logic.

Within these assumptions we can further determine that any expression
of language x that satisfies this predicate ~Logic_Sentence(x) are
not sentences of logic even if they are closed WFF.

∀LP ↔ ~⊢LP
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)


Copyright 2018 Pete Olcott
For example, ∃LiarParadox ∈ F is nonsense, because formal systems aren't sets, so they don't have elements.
And your use of universal quantification over all formal systems (∀F ∈ Formal_Systems) is doomed to failure. Your formula superficially attempts to state that every single formal system has a liar paradox proposition (∀...∃...), but that's obvious nonsense, since nothing relevant to the liar's paradox (self-reference, a provability predicate) can exist in propositional logic, for example.
EFQ
peteolcott
2018-11-01 19:58:21 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
I was trying to minimize clutter. It is obvious that you are correct.
Syntax error. I really wish that sin was not taxed.
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
If you want to get rid of "clutter", get rid of the pointless references to "Formal_Systems" and "F", and use the standard symbol ⊢ instead of "Theorem". If you really need to specify theoremhood in a particular formal system, you can put F as a subscript on ⊢, but it's not really necessary, unless you intend to modify the rules of deduction.
Even still, the rest of your weird formula just doesn't work.
∀x True(x) ↔ φ(x) // Tarski's Formal correctness of True
The above example would seem to indicate that the scope of the ∀ applies
equally to the LHS and the RHS,
In order for ∀x True(x) ↔ φ(x) to be a WFF, at minimum, the two xs both need to be in the scope of the quantifier: ∀x (True(x) ↔ φ(x)).
So Tarski screwed up?

(1) ∀x (~True(x) ↔ ~⊢x) // x cannot be proven True from known facts.
(2) ∀x (True(x) ↔ ⊢x) // x can be proven True from known facts.
(3) ∀x (False(x) ↔ ⊢~x) // x can be proven False from known facts.

∀x (Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x))

∀LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)
But I expect that φ is also intended to be a variable (here, ranging over one-place predicates), so it also needs to be bound by some appropriate quantifier.
Post by peteolcott
thus ∀x ~True(x) ↔ φ(x) would also be correct.
I don't know what you mean by "correct". Do you mean WFF, true in a model (which model?), a theorem...?
You really should use standard terminology and notation. You are constantly reinventing and reinterpreting existing terms and symbols in ways that make it difficult to interpret your intention.
EFQ
There are some apparently very subtle nuances of previously undetectable error in some of the preexisting conventional perspectives.
peteolcott
2018-11-01 20:48:54 UTC
Reply
Permalink
Post by peteolcott
So Tarski screwed up?
No. You screwed up in trying to translate Tarksi's theorem to your non-standard formal notation. Tarksi's theorem is a theorem in the metalanguage. It is not a theorem in a formal language.
You STILL don't seem to understand this crucial difference.
Tarksi also uses Gödel numbering, which you have totally abandoned. Again, if you modify the assumptions of the proof and derive a different result, you have not said anything at all about the original proof. If you do not want to deal with Gödel numbering, then you cannot deal wit Tarksi's proof.
Post by peteolcott
You really should use standard terminology and notation. You are constantly reinventing and reinterpreting existing terms and symbols in ways that make it difficult to interpret your intention.
There are some apparently very subtle nuances
Yes, and you need to understand them. Ignoring them and "simplifying" them just makes you wrong.
EFQ
If we totally forget Tarski and examine the following in isolation,
you cannot point out any semantic errors:

The simple English on the RHS approximates the formalization on the LHS
is only provided to communicate the gist of these ideas.

(1) ∀x (~True(x) ↔ ~⊢x) // x cannot be proven True from known facts.
(2) ∀x (True(x) ↔ ⊢x) // x can be proven True from known facts.
(3) ∀x (False(x) ↔ ⊢~x) // x can be proven False from known facts.

∀x (Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x))

∀LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)

∃LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~∃LP


Copyright 2018 Pete Olcott
Peter Percival
2018-11-01 21:19:25 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
So Tarski screwed up?
No. You screwed up in trying to translate Tarksi's theorem to your
non-standard formal notation. Tarksi's theorem is a theorem in the
metalanguage. It is not a theorem in a formal language.
You STILL don't seem to understand this crucial difference.
Tarksi also uses Gödel numbering, which you have totally abandoned.
Again, if you modify the assumptions of the proof and derive a
different result, you have not said anything at all about the original
proof. If you do not want to deal with Gödel numbering, then you
cannot deal wit Tarksi's proof.
Post by peteolcott
You really should use standard terminology and notation. You are
constantly reinventing and reinterpreting existing terms and symbols
in ways that make it difficult to interpret your intention.
There are some apparently very subtle nuances
Yes, and you need to understand them. Ignoring them and "simplifying"
them just makes you wrong.
EFQ
If we totally forget Tarski and examine the following in isolation,
What you are doing is dogmatically equating truth with provability even
though the two are known to sometimes be co-extensive and sometimes not
co-extensive.
Post by peteolcott
The simple English on the RHS approximates the formalization on the LHS
is only provided to communicate the gist of these ideas.
(1) ∀x (~True(x) ↔ ~⊢x)   //  x cannot be proven True from known facts.
⊢ is the deducibility relation in some formal calculus. Which one in
your case?
Post by peteolcott
(2) ∀x (True(x) ↔ ⊢x)       //  x can be proven True from known facts.
(3) ∀x (False(x) ↔ ⊢~x)   //  x can be proven False from known facts.
∀x (Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x))
∀LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)
∃LP (LP ↔ ~⊢LP)
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~∃LP
Copyright 2018 Pete Olcott
peteolcott
2018-11-01 21:36:00 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
So Tarski screwed up?
No. You screwed up in trying to translate Tarksi's theorem to your non-standard formal notation. Tarksi's theorem is a theorem in the metalanguage.. It is not a theorem in a formal language.
You STILL don't seem to understand this crucial difference.
Tarksi also uses Gödel numbering, which you have totally abandoned.. Again, if you modify the assumptions of the proof and derive a different result, you have not said anything at all about the original proof. If you do not want to deal with Gödel numbering, then you cannot deal wit Tarksi's proof.
Post by peteolcott
You really should use standard terminology and notation. You are constantly reinventing and reinterpreting existing terms and symbols in ways that make it difficult to interpret your intention.
There are some apparently very subtle nuances
Yes, and you need to understand them. Ignoring them and "simplifying" them just makes you wrong.
If we totally forget Tarski
And work with what formal language and what model of it?
Post by peteolcott
and examine the following in isolation,
The simple English on the RHS approximates the formalization on the LHS
is only provided to communicate the gist of these ideas.
(1) ∀x (~True(x) ↔ ~⊢x) // x cannot be proven True from known facts.
(2) ∀x (True(x) ↔ ⊢x) // x can be proven True from known facts.
(3) ∀x (False(x) ↔ ⊢~x) // x can be proven False from known facts.
Your translations on the right are nonsense. ⊢x has nothing to do with whether x can be "proven True". ⊢x just means there is a deductive proof in which x is the last line and all preceding lines are either axioms or the result of using rules of inference on previous lines.
Sure and linguists and every high school student would know exactly what all that means.

What math guys have never quite accomplished is nailing down the
precise meaning of Axiom. According to Math an Axiom is sort of Truth-ish.

When I said that we should think of Axioms as the set of expressions of
language that have been (within this language) defined to have the
semantic property of True, we finally anchor the the notion of what
an Axiom might best be construed as in the common English meaning of
the word fact.

Unless we have an ultimate ground-of-being of the notion of Truth
anchored somewhere there is no chance of further elaboration.
As for the left, what language are these statements in, and what language are they talking about? Since formal languages can't have a predicate that talks about the truth of their own WFFs, there must be two different languages represented here (assuming your "True(x)" is equivalent to V(x)=1, and "False(x)" is equivalent to V(x)=0). You haven't defined either one, let alone both, so these are impossible to interpret as is.
EFQ
I am formalizing the conventional intuitive notion of Truth. True(x) and
V(x)=1 are merely notational conventions for an underlying semantic meaning.
It has always been this underlying (intuitive notion of) semantic meaning
that I am referring to, not the purely arbitrary notational conventions.

Copyright 2018 Pete Olcott
Shobe, Martin
2018-11-01 22:57:52 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
So Tarski screwed up?
No. You screwed up in trying to translate Tarksi's theorem to your
non-standard formal notation. Tarksi's theorem is a theorem in the
metalanguage. It is not a theorem in a formal language.
You STILL don't seem to understand this crucial difference.
Tarksi also uses Gödel numbering, which you have totally abandoned.
Again, if you modify the assumptions of the proof and derive a
different result, you have not said anything at all about the original
proof. If you do not want to deal with Gödel numbering, then you
cannot deal wit Tarksi's proof.
Post by peteolcott
You really should use standard terminology and notation. You are
constantly reinventing and reinterpreting existing terms and symbols
in ways that make it difficult to interpret your intention.
There are some apparently very subtle nuances
Yes, and you need to understand them. Ignoring them and "simplifying"
them just makes you wrong.
EFQ
If we totally forget Tarski and examine the following in isolation,
The simple English on the RHS approximates the formalization on the LHS
is only provided to communicate the gist of these ideas.
(1) ∀x (~True(x) ↔ ~⊢x)   //  x cannot be proven True from known facts.
Semantic error. True and provable are not the same thing (and no, your
"gist" is not particularly close)
Post by peteolcott
(2) ∀x (True(x) ↔ ⊢x)       //  x can be proven True from known facts.
Semantic error. True and provable are not the same thing (and no, your
"gist" is not particularly close)
Post by peteolcott
(3) ∀x (False(x) ↔ ⊢~x)   //  x can be proven False from known facts.
Semantic error. False and not-provable are not the same thing (and no,
your "gist" is not particularly close)

Martin Shobe
Peter Percival
2018-11-01 23:09:00 UTC
Reply
Permalink
Post by peteolcott
(1) ∀x (~True(x) ↔ ~⊢x)   //  x cannot be proven True from known facts.
(2) ∀x (True(x) ↔ ⊢x)       //  x can be proven True from known facts.
∀x (~True(x) ↔ ~⊢x) and ∀x (True(x) ↔ ⊢x) are materially equivalent to
one another. Do you wish to claim that 'x cannot be proven True from
known facts' and 'x can be proven True from known facts' are materially
equivalent to one another?

To see that ∀x (~True(x) ↔ ~⊢x) and ∀x (True(x) ↔ ⊢x) are materially
equivalent to one another one doesn't even need to know what True(x) and
⊢x are. Truth tables will tell you that ~P <-> ~Q and P <-> Q are
materially equivalent to one another. Have you learned to draw truth
tables yet? First few pages of Mendelson. That you don't even need to
know what True(x) and ⊢x are should be good from your point of view.
peteolcott
2018-11-01 19:42:12 UTC
Reply
Permalink
Post by peteolcott
LiarParadox ↔ ∀F ∈ Formal_Systems ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
You still haven't bound the "propositional variable", which is the variable I was talking about.
LiarParadox ↔ ∃LiarParadox ∈ F ~Theorem(F, LiarParadox)
You STILL haven't bound your so-called "propositional variable", so this is STILL not a WFF.
∀x True(x) ↔ φ(x) // Tarski’s Formal correctness of True

These three formulas follow this same pattern: (Simple English follows)
(1) ∀x ~True(x) ↔ ~⊢x // x cannot be proven True from known facts.
(2) ∀x True(x) ↔ ⊢x // x can be proven True from known facts.
(3) ∀x False(x) ↔ ⊢~x // x can be proven False from known facts.

∀x Logic_Sentence(x) ↔ (True(x) ∨ False(x)) ↔ (⊢x ∨ ⊢~x)

∀LP ↔ ~⊢LP
If LP was a theorem this contradicts its assertion: ~⊢LP
If ~LP was a theorem this contradicts its assertion: ⊢LP
∴ ~Logic_Sentence(LP)

Copyright 2018 Pete Olcott
peteolcott
2018-11-03 17:16:19 UTC
Reply
Permalink
WFFs must have all variables bound by quantifiers. Free variables are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed formula) requires all variables to be bound. I've been making that slip-up ever since I first learned logic, and it always finds a way to creep back in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)

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 Fall 2018)

Formalized as:
∀F ∈ Formal_Systems
(
∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)

Copyright 2018 Pete Olcott

Raatikainen, Panu, "Gödel's Incompleteness Theorems",
The Stanford Encyclopedia of Philosophy (Fall 2018 Edition), Edward N. Zalta (ed.),
URL = <https://plato.stanford.edu/archives/fall2018/entries/goedel-incompleteness/>.
Peter Percival
2018-11-03 17:23:45 UTC
Reply
Permalink
Post by peteolcott
WFFs must have all variables bound by quantifiers. Free variables are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed formula)
requires all variables to be bound. I've been making that slip-up ever
since I first learned logic, and it always finds a way to creep back
in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
    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 Fall 2018)
∀F ∈ Formal_Systems
(
  ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it isn't. You haven't captured "a certain amount of arithmetic" or
"nor disproved". Also, you need to explain your notation - F seems to
be a set (it has elements and subsets) but it is also a formal system.
At the very least you should say what a formal system is.
peteolcott
2018-11-03 19:48:50 UTC
Reply
Permalink
Post by peteolcott
WFFs must have all variables bound by quantifiers. Free variables are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed formula) requires all variables to be bound. I've been making that slip-up ever since I first learned logic, and it always finds a way to creep back in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
     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 Fall 2018)
∀F ∈ Formal_Systems
(
   ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it isn't.  You haven't captured "a certain amount of arithmetic" or "nor disproved".  Also, you need to explain your notation - F seems to be a set (it has elements and subsets) but it is also a formal system. At the very least you should say what a
formal system is.
(As is the case) since no such G exists in any formal system F then the
subsets of F constrained by "a certain amount of arithmetic" becomes moot,
thus an extraneous detail.

Proved(G) means the satisfaction of: (Γ ⊢ G)
thus the satisfaction of ∃Γ ⊆ F ~(Γ ⊢ G)
If G was Provable in F this contradicts its assertion: G is not Provable in F

Disproved(G) means the satisfaction of: (Γ ⊢ ~G)
thus the satisfaction of ∀Γ ⊆ F (Γ ⊢ G)
If ~G was Provable in F this contradicts its assertion: G is Provable in F

It certainly seems self-evident to me that a formal system is comprised
of a set of WFF and a set of rules-of-inference, with a subset of
the WFF being axioms. It is also self-evident that a possibly empty
set of WFF are always on the LHS of ⊢. (Mendelson 2015)

Thus the conventional context of my somewhat unconventional use of
"⊆" specifies the meaning and use of this symbol.

All that I intended to do is to precisely formalize the English.
Since the English refers to: "any consistent formal system F"
I universally quantify over a set of such systems.

The English does not say what a formal system is, so I too did not.

Copyright 2018 Pete Olcott

(Mendelson 2016)
Introduction to Mathematical logic Sixth edition Elliott Mendelson
1.4 An Axiom System for the Propositional Calculus page 28
Peter Percival
2018-11-03 20:07:14 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
WFFs must have all variables bound by quantifiers. Free variables
are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed
formula) requires all variables to be bound. I've been making that
slip-up ever since I first learned logic, and it always finds a way
to creep back in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
     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 Fall 2018)
∀F ∈ Formal_Systems
(
   ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it isn't.  You haven't captured "a certain amount of arithmetic" or
"nor disproved".  Also, you need to explain your notation - F seems to
be a set (it has elements and subsets) but it is also a formal system.
At the very least you should say what a formal system is.
(As is the case) since no such G exists in any formal system F then the
subsets of F constrained by "a certain amount of arithmetic" becomes moot,
thus an extraneous detail.
Proved(G) means the satisfaction of: (Γ ⊢ G)
thus the satisfaction of ∃Γ ⊆ F ~(Γ ⊢ G)
If G was Provable in F this contradicts its assertion: G is not Provable in F
Disproved(G) means the satisfaction of: (Γ ⊢ ~G)
thus the satisfaction of ∀Γ ⊆ F (Γ ⊢ G)
If ~G was Provable in F this contradicts its assertion:  G is Provable in F
It certainly seems self-evident to me that a formal system is comprised
of a set of WFF and a set of rules-of-inference, with a subset of
the WFF being axioms. It is also self-evident that a possibly empty
set of WFF are always on the LHS of ⊢. (Mendelson 2015)
Thus the conventional context of my somewhat unconventional use of
"⊆" specifies the meaning and use of this symbol.
All that I intended to do is to precisely formalize the English.
Since your way of formalizing the English is not Gödel's way, what you
have done has got nothing to do with his work and hence can't refute it.
Post by peteolcott
Since the English refers to: "any consistent formal system F"
I universally quantify over a set of such systems.
The English does not say what a formal system is, so I too did not.
Then what does "∀F ∈ Formal_Systems" mean? You wrote it, so you should
know what you mean.
Peter Percival
2018-11-03 20:29:41 UTC
Reply
Permalink
Post by peteolcott
Post by peteolcott
WFFs must have all variables bound by quantifiers. Free variables
are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed
formula) requires all variables to be bound. I've been making that
slip-up ever since I first learned logic, and it always finds a way
to creep back in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
     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 Fall 2018)
∀F ∈ Formal_Systems
(
   ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it isn't.  You haven't captured "a certain amount of arithmetic" or
"nor disproved".  Also, you need to explain your notation - F seems to
be a set (it has elements and subsets) but it is also a formal system.
At the very least you should say what a formal system is.
(As is the case) since no such G exists in any formal system F then the
subsets of F constrained by "a certain amount of arithmetic" becomes moot,
The statement of Gödel's theorem refers to a certain amount of
arithmetic, though not in those words. So whatever it is your talking
about, it isn't Gödel's theorem.
Post by peteolcott
thus an extraneous detail.
Proved(G) means the satisfaction of: (Γ ⊢ G)
thus the satisfaction of ∃Γ ⊆ F ~(Γ ⊢ G)
If G was Provable in F this contradicts its assertion: G is not Provable in F
Disproved(G) means the satisfaction of: (Γ ⊢ ~G)
Which I don't see in your formula. Hence my 'You haven't captured [...]
"nor disproved".' Also according to you everything is disproved, take Γ
to be {~G}. How many times does this kind of error need to be pointed
out to you?
Post by peteolcott
thus the satisfaction of ∀Γ ⊆ F (Γ ⊢ G)
If ~G was Provable in F this contradicts its assertion:  G is Provable in F
It certainly seems self-evident to me that a formal system is comprised
of a set of WFF and a set of rules-of-inference, with a subset of
the WFF being axioms. It is also self-evident that a possibly empty
set of WFF are always on the LHS of ⊢. (Mendelson 2015)
Thus the conventional context of my somewhat unconventional use of
"⊆" specifies the meaning and use of this symbol.
All that I intended to do is to precisely formalize the English.
Since the English refers to: "any consistent formal system F"
I universally quantify over a set of such systems.
The English does not say what a formal system is, so I too did not.
https://plato.stanford.edu/entries/goedel-incompleteness/ describes more
than one.
peteolcott
2018-11-03 20:34:24 UTC
Reply
Permalink
Post by peteolcott
WFFs must have all variables bound by quantifiers. Free variables are not allowed.
Free variables are allowed in WFFs. Of course, what he needs here is a
closed WFF, so your criticism about the lack of quantifiers is still
correct.
Oops, yes, I meant that a proposition (aka sentence or closed formula) requires all variables to be bound. I've been making that slip-up ever since I first learned logic, and it always finds a way to creep back in somewhere.
EFQ
I knew what you meant. The reason that I never used quantifiers
is that the (Raatikainen Fall 2018) simplification never used
quantifiers: (G) F ⊢ GF ↔ ~ProvF(⌈GF⌉)
     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 Fall 2018)
∀F ∈ Formal_Systems
(
   ∃G ∈ F (G ↔ ∃Γ ⊆ F ~(Γ ⊢ G))
)
No it isn't.  You haven't captured "a certain amount of arithmetic" or "nor disproved".  Also, you need to explain your notation - F seems to be a set (it has elements and subsets) but it is also a formal system. At the very least you should say what a
formal system is.
Your comment that I had not sufficiently elaborated "disproved" directly
resulted in version(11). Thanks for your help, that was a big missing piece
that is now filled in.

peteolcott
2018-11-01 01:09:25 UTC
Reply
Permalink
Post by peteolcott
Yet since this is something new you have not yet shown
any faults in its actual reasoning. The best that you have
done is simply state that we do not typically look at these
things in this way.
If you said that dogs do not give birth to kittens,
and I answered you that, if we define cats as dogs,
then they do give birth to kittens, how would you
respond?
See if you can find any mistakes in the following reasoning
(and not dodge the question):

LiarParadox ↔ LiarParadox ∈ F ~Theorem(F, LiarParadox)

If LiarParadox was a theorem of F this contradicts its assertion: ~Theorem(F, LiarParadox)

If ~LiarParadox was a theorem of F this contradicts its assertion: Theorem(F, LiarParadox)

∴ ~Boolean_Closed_WFF(F, LiarParadox)

Copyright 2018 Pete Olcott
Franz Gnaedinger
2018-11-01 07:48:02 UTC
Reply
Permalink
Post by peteolcott
Copyright 2018 Pete Olcott
Peter Olcott knows the absolute and complete and total truth, he is the author
of life and creator of life, he has hundred reasons to assume that he is God,
he creates our future minds in order that we can go on existing, he is both
a human being and God, he is the one Creator of the Universe (claims he made
in sci.lang). Goedel denier Allgod and Einstein hater Pencho Valev ('the GPS
works without relativity theory') ruined sci.logic by flooding it with ever
more parallel threads, applying the strategy of the hyperkooks that ruin
sci.math. Five year ago Allgod popped up in sci.lang and run seventeen
parallel threads. I coped with him. Since then he periodically tries to take
over sci.lang in the name of his phantasm of knowing the absolute truth,
using the same strategy of multiplying the number of parallel threads, and so
I cope with him again.
Loading...