Groups | Search | Server Info | Login | Register

Groups > comp.theory > #21448

Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21

Cross-posted to 4 groups.

Show all headers | View raw

On 7/5/2020 11:28 AM, André G. Isaak wrote:
> On 2020-07-05 09:31, olcott wrote:
>> On 7/5/2020 8:17 AM, André G. Isaak wrote:
>>> On 2020-07-04 15:28, olcott wrote:
>>>> On 7/4/2020 1:21 PM, André G. Isaak wrote:
>>>>> On 2020-07-04 10:36, olcott wrote:
>>>>>> OVERVIEW:
>>>>>> The sentence used in the SEP article to show the essential gist of 
>>>>>> the 1931 Gödel incompleteness sentence
>>>>>>
>>>>>> https://plato.stanford.edu/entries/goedel-incompleteness/#FirIncTheCom 
>>>>>>
>>>>>> (G) F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)
>>>>>>
>>>>>> has been shown to not meet the standard definition of incompleteness:
>>>>>
>>>>> Umm. Of course this doesn't meet the definition of incompleteness. 
>>>>> Incompleteness is a property of *systems*. What you've given above 
>>>>> is a *statement*, not a formal system.
>>>>>
>>>>>> A theory T is incomplete if and only if there is some sentence φ 
>>>>>> such that (T ⊬ φ) and (T ⊬ ¬φ). Because its negation is provable 
>>>>>> in F.
>>>>>>
>>>>>> This is not understood to be any failing of the simplified essence 
>>>>>> to sufficiently correspond to the gist of the orginal Gödel 
>>>>>> sentence. It is understood to mean that the Gödel incompleteness 
>>>>>> sentence does not actually prove incompleteness at all.
>>>>>
>>>>> nor has it been claimed to prove incompleteness.
>>>>>
>>>>> The significance of
>>>>>
>>>>> F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)
>>>>>
>>>>> Is that this statement can only be true if EITHER F is inconsistent 
>>>>> OR if F is incomplete. And since Gödel provides a mechanical 
>>>>> procedure for generating a proposition G_F which satisfies the 
>>>>> above, ONE of these two things must be true.
>>>>>
>>>>> This only proves that F is incomplete once we add the stipulation 
>>>>> that F is consistent. Thus, this only proves that F is incomplete 
>>>>> once we recall Gödel claims his proof only holds true for 
>>>>> CONSISTENT formal systems in which some minimal amount of 
>>>>> arithmetic can be performed.
>>>>
>>>> We are doing way too many steps at once we will never get resolution 
>>>> at the current rate because we always slip-slid into extraneous side 
>>>> issues.
>>>
>>> The problem is we seriously disagree on what count as side issues.
>>>
>>>> Discussing this one step at a time until that step is 100% resolved.
>>>>
>>>> Can you see how this can be existentially quantified:
>>>> F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉) such as this: ∃G_F ∈ WFF(F) ¬Prov_F(⌈G_F⌉)
>>>
>>> Why are you eliminating the biconditional here? Is there some 
>>> justification for that?
>>>
>>> André
>>>
>>
>> This group may may be having network problems.
>> It will not load in Chrome
>>
>>   ∃G_F ∈ WFF(F) ↔ ¬Prov_F(⌈G_F⌉)
> 
> That's not even well formed.
> 
> Also, since G_F refers to a specific expression, you don't want to use 
> that as the name of a variable. I think what you want to say is:
> 
> ∃φ (φ ↔ ¬Prov_F(⌈φ⌉))
> 
> There is no need to include φ ∈ WFF(F) as it serves absolutely no purpose.
> 
> André
> 

Since I view all of these things from the formalist approach of 
operations on finite strings I assume that every variable refers to a
random finite strings unless somehow specified otherwise.

Here is the next step. every formal system has a corresponding algorithm.

Curry–Howard correspondence
https://www.google.com/search?q=curry+hown+corrrespondence&rlz=1C1GCEJ_enUS813US813&oq=curry+hown+corrrespondence&aqs=chrome..69i57j0.8575j0j8&sourceid=chrome&ie=UTF-8

I don't know whether or not I am referring to Curry–Howard 
correspondence or not. What I am referring to is that all of the same 
operations that are applied to the WFF of a formal language to verify 
that a proof exists can be applied by an algorithm on finite strings.

There is no special magical quality of a human mind such that a human 
mind can perform a formal proof that an algorithm cannot.


-- 
Copyright 2020 Pete Olcott

Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 11:36 -0500
  Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-04 12:21 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 16:28 -0500
      Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 07:17 -0600
        Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 10:31 -0500
          Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:28 -0600
            Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 11:42 -0500
              Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 10:53 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:38 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 12:44 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:56 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 13:16 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 15:25 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 André G. Isaak <agisaak@gm.invalid> - 2020-07-05 14:46 -0600
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 16:08 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 David Kleinecke <dkleinecke@gmail.com> - 2020-07-05 15:28 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 17:50 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) Keith Thompson <Keith.S.Thompson+u@gmail.com> - 2020-07-05 17:13 -0700
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) olcott <NoOne@NoWhere.com> - 2020-07-05 20:37 -0500
                Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 (axiomatic basis of truth) André G. Isaak <agisaak@gm.invalid> - 2020-07-05 20:46 -0600
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-04 17:39 -0500
    Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 olcott <NoOne@NoWhere.com> - 2020-07-05 13:15 -0500

csiph-web