Groups | Search | Server Info | Login | Register
| From | André G. Isaak <agisaak@gm.invalid> |
|---|---|
| Newsgroups | comp.theory, comp.ai.philosophy, comp.ai.nat-lang, sci.lang.semantics |
| Subject | Re: Simply defining Gödel Incompleteness and Tarski Undefinability away V21 |
| Date | 2020-07-05 10:53 -0600 |
| Organization | Christians and Atheists United Against Creeping Agnosticism |
| Message-ID | <rdt0i2$bkg$1@dont-email.me> (permalink) |
| References | (2 earlier) <_MGdnVMFZeIeaZ3CnZ2dnUU7-WHNnZ2d@giganews.com> <rdsjtm$tv0$1@dont-email.me> <P-OdnXX34sv9b5zCnZ2dnUU7-V_NnZ2d@giganews.com> <rdsv3j$2hb$1@dont-email.me> <prGdnfpbksBxn5_CnZ2dnUU7-XPNnZ2d@giganews.com> |
Cross-posted to 4 groups.
On 2020-07-05 10:42, olcott wrote: > 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. The formalist approach doesn't involve 'random strings'. The formalist approach approach refers to a specific way of interpreting formal systems. Formal systems do not consist of 'random strings'. > Here is the next step. every formal system has a corresponding algorithm. I don't see any step at all. I see a link to a google search page. What is the supposed step involved here? André > 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. > > -- To email remove 'invalid' & replace 'gm' with well known Google mail service.
Back to comp.theory | Previous | Next — Previous in thread | Next in thread | Find similar
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