Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.lang.prolog > #9159 > unrolled thread

Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this)

Back to article view | Back to comp.lang.prolog

Contents

  Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 09:58 -0500
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Siri Cruise <chine.bleu@yahoo.com> - 2019-04-26 08:20 -0700
      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 10:48 -0500
        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) paul wallich <pw@panix.com> - 2019-04-26 13:40 -0400
          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:10 -0500
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 10:51 -0500
      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-26 10:38 -0700
      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-26 17:48 +0000
        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-26 17:22 -0500
          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-27 01:13 +0000
            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 11:23 -0500
              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-27 18:26 +0000
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-27 14:33 -0700
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:49 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 16:58 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:13 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:28 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 17:44 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 18:59 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 19:44 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 19:48 -0500
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-27 18:10 -0700
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 20:27 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 21:38 -0500
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-28 03:37 -0700
                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-28 04:36 -0700
                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 21:53 -0500
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-04-30 07:08 +0200
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 00:41 -0500
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 11:55 -0500
                            Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-30 12:02 -0500
                              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 07:50 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-05-01 14:53 +0200
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 09:29 -0500
                                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-05-01 18:37 +0200
                                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 13:53 -0500
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 13:56 -0500
                                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Keith Thompson <kst-u@mib.org> - 2019-05-01 10:48 -0700
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Bonita Montero <Bonita.Montero@gmail.com> - 2019-05-01 20:25 +0200
                                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (HP Proof refutation) peteolcott <Here@Home> - 2019-05-01 15:01 -0500
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 14:01 -0500
                                    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) David Brown <david.brown@hesbynett.no> - 2019-05-01 23:28 +0200
                                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:14 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 18:43 -0500
                  Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 22:06 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:10 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:12 -0500
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 15:12 -0500
              Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Richard Damon <Richard@Damon-Family.org> - 2019-05-04 15:05 -0400
                Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-04 15:07 -0500
          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) j4n bur53 <bursejan@gmail.com> - 2019-04-27 03:17 -0700
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Keith Thompson <kst-u@mib.org> - 2019-04-26 19:43 -0700
    Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Bonita Montero <Bonita.Montero@gmail.com> - 2019-05-01 17:56 +0200

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

#9181

On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:
> On Sat, 27 Apr 2019 17:12:45 -0600
> Jeff Barnett <jbb@notatt.com> wrote:
>> Paul Rubin wrote on 4/27/2019 3:52 PM:
>>> peteolcott <Here@Home> writes:
>>>> I have spent 22 years and 12,000 hours on this.
>>>
>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
>>
>> Thanks for the pointer. It seems I missed that article - it came in a
>> crack between regularly reading the Intelligencer in the USC/ISI library
>> where I was employed and starting my own subscription which I kept for
>> two decades. The Intelligencer went from wildly entertaining to hard to
>> read during the latter period. The article by Dudley has a wider appeal
>> today than when he wrote it in 1983; we have lots of computer systems to
>> shield cranks and save then postage.
> 
> Dudley has written a whole book on the subject , "A budget of trisections".
> 

The huge difference in this case is that deriving a complete and consistent
formulation of the notion of True finally anchors Truth Conditional Semantics.
https://en.wikipedia.org/wiki/Truth-conditional_semantics



-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9182

Looks like your turntable is broken. Do these many 
nonsense posts point to a tourette syndrom of yours?

Best of Tourette
https://www.youtube.com/watch?v=O0ex9xwNo3g

Am Sonntag, 28. April 2019 02:48:05 UTC+2 schrieb peteolcott:
> On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:
> > On Sat, 27 Apr 2019 17:12:45 -0600
> > Jeff Barnett <jbb@notatt.com> wrote:
> >> Paul Rubin wrote on 4/27/2019 3:52 PM:
> >>> peteolcott <Here@Home> writes:
> >>>> I have spent 22 years and 12,000 hours on this.
> >>>
> >>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
> >>
> >> Thanks for the pointer. It seems I missed that article - it came in a
> >> crack between regularly reading the Intelligencer in the USC/ISI library
> >> where I was employed and starting my own subscription which I kept for
> >> two decades. The Intelligencer went from wildly entertaining to hard to
> >> read during the latter period. The article by Dudley has a wider appeal
> >> today than when he wrote it in 1983; we have lots of computer systems to
> >> shield cranks and save then postage.
> > 
> > Dudley has written a whole book on the subject , "A budget of trisections".
> > 
> 
> The huge difference in this case is that deriving a complete and consistent
> formulation of the notion of True finally anchors Truth Conditional Semantics.
> https://en.wikipedia.org/wiki/Truth-conditional_semantics
> 
> 
> 
> -- 
> Copyright 2019 Pete Olcott All rights reserved
> 
> "Great spirits have always encountered violent
> opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9183

On 4/27/2019 8:10 PM, j4n bur53 wrote:
> Looks like your turntable is broken. Do these many
> nonsense posts point to a tourette syndrom of yours?
> 

Says the guy that calls a Boolean function stuck in an infinite
loop deductively sound. That little bit of Prolog that you
listed showed that you are not totally clueless.

In fact I bet that you may know Prolog 100 times better than me.


> Best of Tourette
> https://www.youtube.com/watch?v=O0ex9xwNo3g
> 
> Am Sonntag, 28. April 2019 02:48:05 UTC+2 schrieb peteolcott:
>> On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:
>>> On Sat, 27 Apr 2019 17:12:45 -0600
>>> Jeff Barnett <jbb@notatt.com> wrote:
>>>> Paul Rubin wrote on 4/27/2019 3:52 PM:
>>>>> peteolcott <Here@Home> writes:
>>>>>> I have spent 22 years and 12,000 hours on this.
>>>>>
>>>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
>>>>
>>>> Thanks for the pointer. It seems I missed that article - it came in a
>>>> crack between regularly reading the Intelligencer in the USC/ISI library
>>>> where I was employed and starting my own subscription which I kept for
>>>> two decades. The Intelligencer went from wildly entertaining to hard to
>>>> read during the latter period. The article by Dudley has a wider appeal
>>>> today than when he wrote it in 1983; we have lots of computer systems to
>>>> shield cranks and save then postage.
>>>
>>> Dudley has written a whole book on the subject , "A budget of trisections".
>>>
>>
>> The huge difference in this case is that deriving a complete and consistent
>> formulation of the notion of True finally anchors Truth Conditional Semantics.
>> https://en.wikipedia.org/wiki/Truth-conditional_semantics
>>
>>
>>
>> -- 
>> Copyright 2019 Pete Olcott All rights reserved
>>
>> "Great spirits have always encountered violent
>> opposition from mediocre minds." Albert Einstein
> 


-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9184

On 4/27/2019 8:52 PM, Paul Rubin wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>>> I liked Enderton's "A Mathematical Introduction to Logic"
>> High school books would be a great help but, then, he'd think we'd
>> think he's a dumb bunny. Some of us think that anyway.
> 
> Enderton's book is undergrad college level and goes over some basic
> proof theory and model theory, including the completeness and
> incompleteness theorems, Tarski's definition of truth, etc.
> 
> I read Hofstadter's "Gödel, Escher, Bach: An Eternal Golden Braid" in HS
> and liked it a lot.  It develops a version of the incompleteness theorem
> in a fun and quirky way.  OP might like that one too.
> 

Only this one single idea of logic is prerequisite:

     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.

All dogs are mammals
All mammals breath
Therefore all dogs breath

Only because symbolic logic diverges for this simple model
is it possible to prove Gödel's Incompleteness or Tarski's Undefinability.

-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9185

Yes the consequence relation |- from a theory T, is 
not the same as satisfisbility in a model M. For 
the later you have definitness, see Zermelo 1908 

set theory:

    X e M, is either true or false

no undecided, and no inconsistency. The Gödel
completness theorem says, that if T is consistent,
then there is at least one M, that decides

also the undecided sentences of T.

"Am 06.7.1929 promoviert Goedel bei Hans Hahn in
Wien mit der Arbeit Ueber die Vollstaendigkeit des ”
Logikkalkuels“. Es gilt als wahrscheinlich, dass 
Goedel durch Carnap (der Schueler von Frege war) 
auf das Vollst aendigkeitsproblem aufmerksam 
gemacht wurde."

Ein Beweis eines Satzes φ aus einem Axiomensystem 
(d. h. einer Menge von Saetzen) Γ ist eine endliche 
Folge von Saetzen mit letztem Glied φ, wobei jeder 
dieser Saetze entweder Axiom aus Γ ist oder mittels 
einer Regel eines fest gegebenen Logikkalkuels aus 
frueheren Saetzen hervorgeht.

Hilbert und Ackermann hatten das Vollstaendigkeits- 
problem deutlich formuliert. Aus heutiger Sicht gibt 
es Argumente bei Skolem aus den fruehen 20er Jahren, 
die den Beweis des Vollstaendigkeitssatzes fast 
vorwegnehmen, denen aber doch der platonistische 
Mut zur erforderlichen Modellkonstruktion fehlt.

Goedel selbst erwaehnt ein unveroeffentlichtes 
Manuskript von Carnap, das einen verwandten 
Vollstaendigkeitssatz praesentiert. Am 6. 9. 1929 
traegt Goedel auf einer Tagung in Koenigsberg ueber 
seinen Vollstaendigkeitssatz vor; man sieht nicht 
unmittelbar die Tragweite seines Ergebnisses." 

https://ivv5hpp.uni-muenster.de/u/rds/goedel_deutsch.pdf

https://en.wikipedia.org/wiki/G%C3%B6del's_completeness_theorem#Model_existence_theorem

Am Sonntag, 28. April 2019 04:38:51 UTC+2 schrieb peteolcott:
> On 4/27/2019 8:52 PM, Paul Rubin wrote:
> > Jeff Barnett <jbb@notatt.com> writes:
> >>> I liked Enderton's "A Mathematical Introduction to Logic"
> >> High school books would be a great help but, then, he'd think we'd
> >> think he's a dumb bunny. Some of us think that anyway.
> > 
> > Enderton's book is undergrad college level and goes over some basic
> > proof theory and model theory, including the completeness and
> > incompleteness theorems, Tarski's definition of truth, etc.
> > 
> > I read Hofstadter's "Gödel, Escher, Bach: An Eternal Golden Braid" in HS
> > and liked it a lot.  It develops a version of the incompleteness theorem
> > in a fun and quirky way.  OP might like that one too.
> > 
> 
> Only this one single idea of logic is prerequisite:
> 
>      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.
> 
> All dogs are mammals
> All mammals breath
> Therefore all dogs breath
> 
> Only because symbolic logic diverges for this simple model
> is it possible to prove Gödel's Incompleteness or Tarski's Undefinability.
> 
> -- 
> Copyright 2019 Pete Olcott All rights reserved
> 
> "Great spirits have always encountered violent
> opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9186

Pure Prolog is not able to enumerate a model M,
because it uses depth first. negation of failure 
subsequently also does cannot enumerate a model M.

If you need models M, you might want to have
a look at Answer Set Programming (ASP). Sometimes
it can be implemented with a modified 

Davis–Putnam–Logemann–Loveland (DPLL) algorithm:

https://en.wikipedia.org/wiki/Answer_set_programming

https://en.wikipedia.org/wiki/DPLL_algorithm

Am Sonntag, 28. April 2019 12:37:50 UTC+2 schrieb j4n bur53:
> Yes the consequence relation |- from a theory T, is 
> not the same as satisfisbility in a model M. For 
> the later you have definitness, see Zermelo 1908 
> 
> set theory:
> 
>     X e M, is either true or false
> 
> no undecided, and no inconsistency. The Gödel
> completness theorem says, that if T is consistent,
> then there is at least one M, that decides
> 
> also the undecided sentences of T.
> 
> "Am 06.7.1929 promoviert Goedel bei Hans Hahn in
> Wien mit der Arbeit Ueber die Vollstaendigkeit des ”
> Logikkalkuels“. Es gilt als wahrscheinlich, dass 
> Goedel durch Carnap (der Schueler von Frege war) 
> auf das Vollst aendigkeitsproblem aufmerksam 
> gemacht wurde."
> 
> Ein Beweis eines Satzes φ aus einem Axiomensystem 
> (d. h. einer Menge von Saetzen) Γ ist eine endliche 
> Folge von Saetzen mit letztem Glied φ, wobei jeder 
> dieser Saetze entweder Axiom aus Γ ist oder mittels 
> einer Regel eines fest gegebenen Logikkalkuels aus 
> frueheren Saetzen hervorgeht.
> 
> Hilbert und Ackermann hatten das Vollstaendigkeits- 
> problem deutlich formuliert. Aus heutiger Sicht gibt 
> es Argumente bei Skolem aus den fruehen 20er Jahren, 
> die den Beweis des Vollstaendigkeitssatzes fast 
> vorwegnehmen, denen aber doch der platonistische 
> Mut zur erforderlichen Modellkonstruktion fehlt.
> 
> Goedel selbst erwaehnt ein unveroeffentlichtes 
> Manuskript von Carnap, das einen verwandten 
> Vollstaendigkeitssatz praesentiert. Am 6. 9. 1929 
> traegt Goedel auf einer Tagung in Koenigsberg ueber 
> seinen Vollstaendigkeitssatz vor; man sieht nicht 
> unmittelbar die Tragweite seines Ergebnisses." 
> 
> https://ivv5hpp.uni-muenster.de/u/rds/goedel_deutsch.pdf
> 
> https://en.wikipedia.org/wiki/G%C3%B6del's_completeness_theorem#Model_existence_theorem
> 
> Am Sonntag, 28. April 2019 04:38:51 UTC+2 schrieb peteolcott:
> > On 4/27/2019 8:52 PM, Paul Rubin wrote:
> > > Jeff Barnett <jbb@notatt.com> writes:
> > >>> I liked Enderton's "A Mathematical Introduction to Logic"
> > >> High school books would be a great help but, then, he'd think we'd
> > >> think he's a dumb bunny. Some of us think that anyway.
> > > 
> > > Enderton's book is undergrad college level and goes over some basic
> > > proof theory and model theory, including the completeness and
> > > incompleteness theorems, Tarski's definition of truth, etc.
> > > 
> > > I read Hofstadter's "Gödel, Escher, Bach: An Eternal Golden Braid" in HS
> > > and liked it a lot.  It develops a version of the incompleteness theorem
> > > in a fun and quirky way.  OP might like that one too.
> > > 
> > 
> > Only this one single idea of logic is prerequisite:
> > 
> >      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.
> > 
> > All dogs are mammals
> > All mammals breath
> > Therefore all dogs breath
> > 
> > Only because symbolic logic diverges for this simple model
> > is it possible to prove Gödel's Incompleteness or Tarski's Undefinability.
> > 
> > -- 
> > Copyright 2019 Pete Olcott All rights reserved
> > 
> > "Great spirits have always encountered violent
> > opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9190

On 4/28/2019 6:36 AM, j4n bur53 wrote:
> Pure Prolog is not able to enumerate a model M,
> because it uses depth first. negation of failure
> subsequently also does cannot enumerate a model M.
> 

I am not talking about every aspect of Prolog.
I am only talking about the aspect of Prolog that "understands"
that Provable(X) is True(X), Provable (¬X) is False(X).

 From this much we can build:
(¬Provable(X) ∧ ¬Provable(¬X)) ↔ Unsound(X)
Which means that a sentence must be true or false.

 From this we can determine that this sentence is false:
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
There is no sentence G of Formal System F that is neither True nor False in F.

Thus making this paragraph false:
First incompleteness theorem
Any consistent formal system F within which a certain amount of elementary
arithmetic can be carried out is incomplete; i.e., there are statements
of the language of F which can neither be proved nor disproved in F.
https://plato.stanford.edu/entries/goedel-incompleteness/#Int

Thus refuting the 1931 Incompleteness Theorem.


-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9192

peteolcott <Here@Home> writes:

> On 4/28/2019 6:36 AM, j4n bur53 wrote:
>> Pure Prolog is not able to enumerate a model M,
>> because it uses depth first. negation of failure
>> subsequently also does cannot enumerate a model M.
>>
>
> I am not talking about every aspect of Prolog.
> I am only talking about the aspect of Prolog that "understands"
> that Provable(X) is True(X), Provable (¬X) is False(X).
>
> From this much we can build:
> (¬Provable(X) ∧ ¬Provable(¬X)) ↔ Unsound(X)
> Which means that a sentence must be true or false.

The problem is that it's not interesting to have no unsound sentences.
What's interesting is to have no inconsistency.
That is that you have not True(X) ∧ False(X),
ie that you don't have (Provable(X) ∧ Provable(¬X)) for any X.

And what Gödel proved, is that if you have a non-trivial formal system
that is not unsound, then it is inconsistent.

So, bravo, you've built a useless formal system!

-- 
__Pascal J. Bourguignon__
http://www.informatimago.com

[toc] | [prev] | [next] | [standalone]

#9193

On 4/30/2019 12:08 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 4/28/2019 6:36 AM, j4n bur53 wrote:
>>> Pure Prolog is not able to enumerate a model M,
>>> because it uses depth first. negation of failure
>>> subsequently also does cannot enumerate a model M.
>>>
>>
>> I am not talking about every aspect of Prolog.
>> I am only talking about the aspect of Prolog that "understands"
>> that Provable(X) is True(X), Provable (¬X) is False(X).
>>
>>  From this much we can build:
>> (¬Provable(X) ∧ ¬Provable(¬X)) ↔ Unsound(X)
>> Which means that a sentence must be true or false.
> 
> The problem is that it's not interesting to have no unsound sentences.
> What's interesting is to have no inconsistency.
> That is that you have not True(X) ∧ False(X),
> ie that you don't have (Provable(X) ∧ Provable(¬X)) for any X.
> 
> And what Gödel proved, is that if you have a non-trivial formal system
> that is not unsound, then it is inconsistent.
> 
> So, bravo, you've built a useless formal system!
> 

Based on these three axioms Gödel's Incompleteness is refuted:
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
There is no sentence G of Formal System F that is neither True nor False in F.


-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9198

On 4/30/2019 11:23 AM, taruss@google.com wrote:
> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
> 
>> Based on these three axioms Gödel's Incompleteness is refuted:
>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
> 
> Not sure why these are axioms. It would seem that these are properties of
> your formal system, which if satisfied would admit it into your system. I don't
> see how asserting that all formal systems obey these axioms work. For arbitrary
> formal systems, it is clear that these axioms do not hold.
>   
>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>> There is no sentence G of Formal System F that is neither True nor False in F.
> 
> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
> statement.
> 
> Instead, the claim that you have is that if you create a suitably constrained
> formal system, then in *that* system you can have complete inference. This is
> well-recognized result. The interesting question is whether the constraints
> needed to achieve this complete inference will leave you with enough expressive
> power to be able to perform interesting inference in your system.
> 
> Certainly one of Gödel's results is that if you have a formal system that is
> expressive enough to include arithmetic, you run into incompleteness. 

Only because the mathematical system that he used to form this proof was too
weak to discern semantic ill formedness:

In the same way that not all finite strings are well-formed formula
(when semantic criteria is applied) not all closed WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.


>A
> consequence of that is that your system, therefore, cannot use arithmetic. As
> long as you don't need arithmetic for the inferences of interest, then you may
> find your formal system adequate.
> 
> For an interesting discussion of some issue having to do with decidability and
> efficiency of reasoning, you may want to look at the Description Logic
> research. There are a number of variants of description logic with different
> expressive power and consequently different decisions regarding what can be
> computed, ranging from tractable complete inference to undecidability.
> 
> Overview: https://en.wikipedia.org/wiki/Description_logic
> Complexity: http://www.cs.man.ac.uk/~ezolin/dl/
> 


-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9199

On 4/30/2019 11:47 AM, Pascal J. Bourguignon wrote:
> taruss@google.com writes:
> 
>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>
>>> Based on these three axioms Gödel's Incompleteness is refuted:
>>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
>>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
>>
>> Not sure why these are axioms. It would seem that these are properties of
>> your formal system, which if satisfied would admit it into your system. I don't
>> see how asserting that all formal systems obey these axioms work. For arbitrary
>> formal systems, it is clear that these axioms do not hold.
>>   
>>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>>> There is no sentence G of Formal System F that is neither True nor False in F.
>>
>> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
>> statement.
>>
>> Instead, the claim that you have is that if you create a suitably constrained
>> formal system, then in *that* system you can have complete inference. This is
>> well-recognized result. The interesting question is whether the constraints
>> needed to achieve this complete inference will leave you with enough expressive
>> power to be able to perform interesting inference in your system.
>>
>> Certainly one of Gödel's results is that if you have a formal system that is
>> expressive enough to include arithmetic, you run into incompleteness. A
>> consequence of that is that your system, therefore, cannot use arithmetic. As
>> long as you don't need arithmetic for the inferences of interest, then you may
>> find your formal system adequate.
> 
> And note that arithmetic is a consequence of Turing Completeness.  So if
> your formals sytem is any useful to a programmer (ie. is Turing
> Equivalent), then it will have arithmetic, and therefore it will be
> inconsistent or incomplete, choose of of two.
> 
> (Ie. correct programs will produce wrong results, or there will be
> programs that you won't be able to prove if it is correct or incorrect).
> 

My system can express anything including arithmetic, it simply does not
do so erroneously:

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the semantic
property of Boolean true (thus anchoring formal proofs in the semantics of
Boolean values) then the theorem consequences of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.



-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9202

On 5/1/2019 5:21 AM, bert wrote:
> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>> On 4/30/2019 1:06 PM, bert wrote:
>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>> etcetera
>>>
>>> One of the hallmarks of a crank is being the
>>> author of nearly all of the posts in a thread.
>>
>> What if I am a crank and I am correct?
> 
> Then other distribution and publicity routes
> would be more appropriate for your theories.
> 

I have to first get someone to consider the possibility that I am correct
so that they can test my actual reasoning and thus prove that I am correct.
Because my result is unbelievable I am simply dismissed out-of-hand.

In sound deductive inference there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

If we simply construe Axioms as expressions of language having
the semantic property of Boolean true this would anchor the syntax
of formal proofs to the semantics of Boolean values.

Now we have: [Deductively Sound Formal Proofs] True(x) ↔ (⊢x)
[a connected sequence of inference from axioms to a true consequence].
AKA the same universal truth predicate that Tarski "proved" was impossible.

he 1936 Tarski Undefinability Proof
http://liarparadox.org/Tarski_Proof_275_276.pdf

-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9203

peteolcott <Here@Home> writes:

> On 5/1/2019 5:21 AM, bert wrote:
>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>> On 4/30/2019 1:06 PM, bert wrote:
>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>> etcetera
>>>>
>>>> One of the hallmarks of a crank is being the
>>>> author of nearly all of the posts in a thread.
>>>
>>> What if I am a crank and I am correct?
>>
>> Then other distribution and publicity routes
>> would be more appropriate for your theories.
>>
>
> I have to first get someone to consider the possibility that I am correct
> so that they can test my actual reasoning and thus prove that I am correct.
> Because my result is unbelievable I am simply dismissed out-of-hand.

Or you could show us a non-trivial formal system that is both consistent
and complete.

-- 
__Pascal J. Bourguignon__
http://www.informatimago.com

[toc] | [prev] | [next] | [standalone]

#9204

On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 5/1/2019 5:21 AM, bert wrote:
>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>> etcetera
>>>>>
>>>>> One of the hallmarks of a crank is being the
>>>>> author of nearly all of the posts in a thread.
>>>>
>>>> What if I am a crank and I am correct?
>>>
>>> Then other distribution and publicity routes
>>> would be more appropriate for your theories.
>>>
>>
>> I have to first get someone to consider the possibility that I am correct
>> so that they can test my actual reasoning and thus prove that I am correct.
>> Because my result is unbelievable I am simply dismissed out-of-hand.
> 
> Or you could show us a non-trivial formal system that is both consistent
> and complete.
> 

I just did and you trimmed it from your reply.
Go back to my message and analyze the part that you trimmed point-by-point.

-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9206

peteolcott <Here@Home> writes:

> On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
>> peteolcott <Here@Home> writes:
>>
>>> On 5/1/2019 5:21 AM, bert wrote:
>>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>>> etcetera
>>>>>>
>>>>>> One of the hallmarks of a crank is being the
>>>>>> author of nearly all of the posts in a thread.
>>>>>
>>>>> What if I am a crank and I am correct?
>>>>
>>>> Then other distribution and publicity routes
>>>> would be more appropriate for your theories.
>>>>
>>>
>>> I have to first get someone to consider the possibility that I am correct
>>> so that they can test my actual reasoning and thus prove that I am correct.
>>> Because my result is unbelievable I am simply dismissed out-of-hand.
>>
>> Or you could show us a non-trivial formal system that is both consistent
>> and complete.
>>
>
> I just did and you trimmed it from your reply.
> Go back to my message and analyze the part that you trimmed point-by-point.

Well, if I trimmed it, it was trivial…
Could I have missed arithmetic?

-- 
__Pascal J. Bourguignon__
http://www.informatimago.com

[toc] | [prev] | [next] | [standalone]

#9209

On 5/1/2019 11:37 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
>>> peteolcott <Here@Home> writes:
>>>
>>>> On 5/1/2019 5:21 AM, bert wrote:
>>>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>>>> etcetera
>>>>>>>
>>>>>>> One of the hallmarks of a crank is being the
>>>>>>> author of nearly all of the posts in a thread.
>>>>>>
>>>>>> What if I am a crank and I am correct?
>>>>>
>>>>> Then other distribution and publicity routes
>>>>> would be more appropriate for your theories.
>>>>>
>>>>
>>>> I have to first get someone to consider the possibility that I am correct
>>>> so that they can test my actual reasoning and thus prove that I am correct.
>>>> Because my result is unbelievable I am simply dismissed out-of-hand.
>>>
>>> Or you could show us a non-trivial formal system that is both consistent
>>> and complete.
>>>
>>
>> I just did and you trimmed it from your reply.
>> Go back to my message and analyze the part that you trimmed point-by-point.
> 
> Well, if I trimmed it, it was trivial…
> Could I have missed arithmetic?
> 

That is exactly what I mean by dismissed out-of-hand

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.





-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9210

On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
> 
>> On 5/1/2019 5:21 AM, bert wrote:
>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott  wrote:
>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott  wrote:
>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>> etcetera
>>>>>
>>>>> One of the hallmarks of a crank is being the
>>>>> author of nearly all of the posts in a thread.
>>>>
>>>> What if I am a crank and I am correct?
>>>
>>> Then other distribution and publicity routes
>>> would be more appropriate for your theories.
>>>
>>
>> I have to first get someone to consider the possibility that I am correct
>> so that they can test my actual reasoning and thus prove that I am correct.
>> Because my result is unbelievable I am simply dismissed out-of-hand.
> 
> Or you could show us a non-trivial formal system that is both consistent
> and complete.
> 

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.


-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

#9207

peteolcott <Here@Home> writes:
[...]

One last try.

Pete, as far as I can tell you have written nothing relevant to
C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
(I would have emailed you if you had provided a valid email address.)

I do not intend to post again in this thread.

-- 
Keith Thompson (The_Other_Keith) kst-u@mib.org  <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

[toc] | [prev] | [next] | [standalone]

#9208

Am 01.05.2019 um 19:48 schrieb Keith Thompson:
> peteolcott <Here@Home> writes:
> [...]
> 
> One last try.
> 
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
> I do not intend to post again in this thread.

Look at this thread - he seems to be manic.
Arguing is a waste of time here.

[toc] | [prev] | [next] | [standalone]

#9212 — Re: Eliminating Undecidability and Incompleteness in Formal Systems (HP Proof refutation)

On 5/1/2019 1:25 PM, Bonita Montero wrote:
> Am 01.05.2019 um 19:48 schrieb Keith Thompson:
>> peteolcott <Here@Home> writes:
>> [...]
>>
>> One last try.
>>
>> Pete, as far as I can tell you have written nothing relevant to
>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>> (I would have emailed you if you had provided a valid email address.)
>> I do not intend to post again in this thread.
> 
> Look at this thread - he seems to be manic.
> Arguing is a waste of time here.
> 

I check each group individually. If respondent were to trim
the other group form their response I would have beet feedback
regrading which groups are relevant.

Although I am not manic I am very excited that I completed
my 22 year 12,000 hour research project with a formalization
of the the notion of True, thus refuting Tarski:

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.

=====================================================================
The Refutation of Peter Linz Halting Problem Proof is complete.
This refutation applies to the other conventional (self-referential) Halting
Problem proofs. This algorithm was completed December 13th 2018 7:00PM

Peter Linz Halting Problem Proof (1993) with Turing Machines H and Ĥ.
http://liarparadox.org/Peter_Linz_HP(Pages_318-319).pdf

Every detail of the design of virtual machines implementing the Peter
Linz H deciding halting for the Peter Linz input pair: (Ĥ, Ĥ) is complete.

The only step remaining is the C++ encoding of the UTM that executes
these virtual machine descriptions.

When this last step is complete I will provide the full execution trace
of H actually deciding halting for input pair: (Ĥ, Ĥ).

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 years.

-- 
Copyright 2019 Pete Olcott All rights reserved

"Great spirits have always encountered violent
opposition from mediocre minds." Albert Einstein

[toc] | [prev] | [next] | [standalone]

Page 2 of 3 — ← Prev page 1 [2] 3  Next page →

Back to top | Article view | comp.lang.prolog

csiph-web