experchange > comp.theory

peteolcott (11-05-18, 04:00 AM)
A world class expert provided some coaching. They have published very much
in the field of Incompleteness and many related fields.

They changed this:
?F ? Formal_Systems (?G ? F (G ? ?? ? F ~(? ? G)))

into this:
?F (F ? Formal_Systems & Q ? F) ? ?G ? L(F) (G ? ~(F ? G))
Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)

I realized that Q is not needed if the following expression evaluates to False:
?F ? Formal_Systems ?G ? L(F) (G ? ~(F ? G))

The following analysis seems to refute Gdel 1931 Incompleteness as long as
the term "satisfiable" is interpreted using the conventional meanings of the
symbols within symbolic logic.

If G was Provable in F this contradicts its assertion: G is not Provable in F
If ~G was Provable in F this contradicts its assertion: G is Provable in F.
Since G is neither Provable nor Refutable in F it forms a Gdel sentence in F.

Because G is not satisfiable in any Formal System F, the Gdel sentence does not exist.

Copyright 2018 Pete Olcott
peteolcott (11-05-18, 04:07 AM)
On 11/4/2018 8:00 PM, peteolcott wrote:
> A world class expert provided some coaching. They have published very much
> in the field of Incompleteness and many related fields.
> They changed this:
> ?F ? Formal_Systems (?G ? F (G ? ?? ? F ~(? ? G)))
> into this:


L(F) means the language of formal system F.
[..]
Peter Percival (11-05-18, 04:58 PM)
sci.lang removed

peteolcott wrote:
> A world class expert provided some coaching. They have published very much


Does he or she have a name?

[..]
> False:
> ?F ? Formal_Systems ?G ? L(F) (G ? ~(F ? G))
> The following analysis seems to refute Gdel 1931 Incompleteness as long as


Does he or she know that you have "refuted" the incompleteness theorem?
[..]
peteolcott (11-05-18, 05:37 PM)
On 11/5/2018 8:58 AM, Peter Percival wrote:
> sci.lang removed
> peteolcott wrote:
> Does he or she have a name?
> Does he or she know that you have "refuted" the incompleteness theorem?


All that I had them do is verify that my formalized simplification of the
incompleteness theorem accurately represents a correct simplification of the
original theorem.

As long as my formalized simplification correctly sums up the essence of
the original theorem then refuting the simplification refutes the original
theorem by analogy.

The only semantic change that they made is the restriction that F must be
at least as expressive as Q. All of the other changes are purely syntactic,
making what I am saying easier to understand by using existing conventions,
yet not changing the meanings that I am conveying.
[..]
peteolcott (11-05-18, 05:51 PM)
On 11/5/2018 8:58 AM, Peter Percival wrote:
> sci.lang removed sci.lang added back in.


Refuting Tarski / Gdel validates my ?x True(x).
A complete and consistent True(x) anchors Truth Conditional Semantics.
Truth Conditional Semantics provides the basis for formalizing natural language.




> peteolcott wrote:
> Does he or she have a name?
> Does he or she know that you have "refuted" the incompleteness theorem?


All that I had them do is verify that my formalized simplification of the
incompleteness theorem accurately represents a correct simplification of the
original theorem.

As long as my formalized simplification correctly sums up the essence of
the original theorem then refuting the simplification refutes the original
theorem by analogy.

The only semantic change that they made is the restriction that F must be
at least as expressive as Q. All of the other changes are purely syntactic,
making what I am saying easier to understand by using existing conventions,
yet not changing the meanings that I am conveying.
[..]
Peter Percival (11-05-18, 05:52 PM)
peteolcott wrote:
[..]
> at least as expressive as Q. All of the other changes are purely syntactic,
> making what I am saying easier to understand by using existing conventions,
> yet not changing the meanings that I am conveying.


So you are claiming, are you, that this nameless "world class expert"
agrees with you except for the bit about Q?
peteolcott (11-05-18, 06:31 PM)
On 11/5/2018 9:52 AM, Peter Percival wrote:
> peteolcott wrote:
> So you are claiming, are you, that this nameless "world class expert" agrees with you except for the bit about Q?

I am claiming that they adapted my formalization of a correct simplification
of the 1931 GIT from this: ?F ? Formal_Systems (?G ? F (G ? ?? ? F ~(? ? G)))

into this:
"We need to distinguish the language of formal system L(F) and the formal system F"
....
"?F (F ? Formal_Systems & Q ? F) ? ?G ? L(F) (G ? ~(F ? G))"

"Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)"

All three lines are cut-and-paste verbatim direct quotes.
Peter Percival (11-05-18, 06:34 PM)
sci.lang removed

peteolcott wrote:
> On 11/5/2018 8:58 AM, Peter Percival wrote:
>> sci.lang removed

> sci.lang added back in.
> Refuting Tarski / Gdel validates my ?x True(x).


If your definition of True(x) is such that ?x True(x), then it's useless
as a truth predicate.

> A complete and consistent True(x) anchors Truth Conditional Semantics.
> Truth Conditional Semantics provides the basis for formalizing natural
> language.
>
>


I'd still like to know.
[..]
peteolcott (11-05-18, 06:42 PM)
On 11/5/2018 9:53 AM, exflaso.quodlibet wrote:
> On Sunday, November 4, 2018 at 9:00:07 PM UTC-5, peteolcott wrote:
> Your "world class expert" made an error. This formula is missing the parentheses needed to correctly mark the scope of the universal quantifier. As written, it only scopes over the antecedent, leaving the various instances of F in the consequent unbound.


Here is their cut-and-paste full reply:

We need to distinguish the language of formal system L(F) and the formal system F (often equated with the set of its theorems). Distinct systems may share the same language.

So the correct formalization would be something like:

∀F (F ∈ Formal_Systems & Q ⊆ F) → ∃G ∈ L(F) (G ↔ ~(F ⊢ G))

Q here is Robinson Arithmetic (the theorem fails for some weaker formal systems)

So does my reformulated adaptation of their reformulation have correct scoping?
∃F ∈ Formal_Systems ∃G ∈ L(F) (G ↔ ~(F ⊢ G))

Or do I need to say it this way?
∃F ∈ Formal_Systems (∃G ∈ L(F) (G ↔ ~(F ⊢ G)))
Peter Percival (11-05-18, 06:56 PM)
peteolcott wrote:
> On 11/5/2018 9:52 AM, Peter Percival wrote:
> I am claiming that they adapted my formalization of a correct
> simplification
> of the 1931 GIT from this: ?F ? Formal_Systems (?G ? F (G ? ?? ? F ~(? ?
> G)))
> into this:
> "We need to distinguish the language of formal system L(F) and the
> formal system F"


Me, two days ago: 'what do _you_ mean by a formal system?'
> ...
> "?F (F ? Formal_Systems & Q ? F) ? ?G ? L(F) (G ? ~(F ? G))"
> "Q here is Robinson Arithmetic (the theorem fails for some weaker formal
> systems)"


Me, yesterday: 'When logicians write of something being provable they
mean provable in some theory. What theory does your Provable refer to?'
Peter Percival (11-07-18, 06:10 PM)
sci.lang removed

peteolcott wrote:
> A world class expert provided some coaching. They have published very much
> in the field of Incompleteness and many related fields.
> They changed this:
> ?F ? Formal_Systems (?G ? F (G ? ?? ? F ~(? ? G)))
> into this:
> ?F (F ? Formal_Systems & Q ? F) ? ?G ? L(F) (G ? ~(F ? G))
> Q here is Robinson Arithmetic (the theorem fails for some weaker formal
> systems)


I would have you ask them something - why Q, why not Robinson's R?

> I realized that Q is not needed if the following expression evaluates to


What is the significance of Q, that you know it is not needed?
[..]
Peter Percival (11-07-18, 06:23 PM)
Peter Percival wrote:
> peteolcott wrote:


I'd still like to know. It may be that he or she has asked not to be
named because they would be embarrassed to have their name associated
with your twaddle. I sympathise. But if that's so, tell us that it's
so. Is it like a super injunction
( not
only can't they be named but why they can't be named can't be revealed
either?
[..]
Peter Percival (11-08-18, 07:42 PM)
Peter Percival wrote:
> Peter Percival wrote:
> I'd still like to know.  It may be that he or she has asked not to be
> named because they would be embarrassed to have their name associated
> with your twaddle.  I sympathise.  But if that's so, tell us that it's
> so.  Is it like a super injunction
> ( not
> only can't they be named but why they can't be named can't be revealed
> either?


Well?
peteolcott (11-08-18, 08:18 PM)
On 11/8/2018 11:42 AM, Peter Percival wrote:
> Peter Percival wrote:
> Well?


You asked for it:


I respect the privacy of world class experts. (Not Doug Lenat)
Doug Lenat the founder of the largest AI project in the world sent me his cell phone number.
Peter Percival (11-08-18, 08:31 PM)
peteolcott wrote:
> On 11/8/2018 11:42 AM, Peter Percival wrote:
> You asked for it:
>
> I respect the privacy of world class experts. (Not Doug Lenat)
> Doug Lenat the founder of the largest AI project in the world sent me
> his cell phone number.


I hope you weren't caused too much embarrassment when you wet yourself
with the excitement of it.

Similar Threads