Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]
Groups > comp.lang.lisp > #32764 > unrolled thread
| Started by | peteolcott <Here@Home> |
|---|---|
| First post | 2019-04-26 09:58 -0500 |
| Last post | 2019-05-06 05:51 -0700 |
| Articles | 20 on this page of 74 — 17 participants |
Back to article view | Back to comp.lang.lisp
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) Siebe de Vos <siebe@de-vos.de> - 2019-04-26 17:24 +0200
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) 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:10 -0500
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) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 14:44 -0700
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-28 03:40 +0000
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 16:48 -0500
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 14:52 -0700
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) Jeff Barnett <jbb@notatt.com> - 2019-04-27 17:12 -0600
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 18:41 -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) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 17:10 -0700
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) Jeff Barnett <jbb@notatt.com> - 2019-04-27 19:26 -0600
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-27 18:52 -0700
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) 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) taruss@google.com - 2019-04-30 09:23 -0700
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) "Pascal J. Bourguignon" <pjb@informatimago.com> - 2019-04-30 18:47 +0200
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-30 11:55 -0500
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-27 21:28 -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) Spiros Bousbouras <spibou@gmail.com> - 2019-04-28 00:16 +0000
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) paul wallich <pw@panix.com> - 2019-04-29 17:53 -0400
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) luserdroog <mijoryx@yahoo.com> - 2019-04-29 17:22 -0700
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) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-04-30 00:18 +0000
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Paul Rubin <no.email@nospam.invalid> - 2019-04-29 18:11 -0700
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-04-29 21:58 -0500
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Stefan Monnier <monnier@iro.umontreal.ca> - 2019-05-02 15:11 -0400
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Jeff Barnett <jbb@notatt.com> - 2019-05-02 16:46 -0600
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Kaz Kylheku <847-115-0292@kylheku.com> - 2019-05-02 23:21 +0000
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 22:04 -0500
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Jeff Barnett <jbb@notatt.com> - 2019-05-02 21:13 -0600
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 22:42 -0500
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Halting Problem) peteolcott <Here@Home> - 2019-05-02 22:46 -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:49 -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) 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) 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
Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Rabican <gavinschuette@gmail.com> - 2019-05-06 05:51 -0700
Page 1 of 4 [1] 2 3 4 Next page →
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-26 09:58 -0500 |
| Subject | Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) |
| Message-ID | <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com> |
Prolog already implements the sound deductive inference model. The Prolog Database is equivalent to a formal system. Prolog Facts are equivalent to the Axioms of a formal system. Prolog Rules are equivalent to the rules-of-inference of a formal system. Prolog Queries are equivalent to the logic sentences of a formal system. https://en.wikipedia.org/wiki/Prolog#Execution If a the query of a Prolog goal returns Yes then the query is True: (F ⊢ X) If a the query of the negation of a Prolog goal returns Yes then the query is False: (F ⊢ ¬X) Otherwise the goal is neither provable nor refutable on the basis of the Facts and Rules in the Prolog Database: ¬(True(F, X) ∨ False(F, X)) Here is the simplest way to explain how the formal proofs of symbolic logic have been made to conform to the sound deductive inference model: (1) If there is a (connected sequence of valid deductions from true premises to a true conclusion) then X is TRUE: (F ⊢ X). (2) If there is a (connected sequence of valid deductions from true premises to the negation of the conclusion) then X is FALSE: (F ⊢ ¬X). (3) otherwise X UNSOUND We use the Axioms of formal systems in place of true premises and the conclusion of a formal proof is called a consequence. This simple little system shows that Gödel's Incompleteness Theorem and the Tarski Undefinability Theorem are false. https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [next] | [standalone]
| From | Siri Cruise <chine.bleu@yahoo.com> |
|---|---|
| Date | 2019-04-26 08:20 -0700 |
| Message-ID | <chine.bleu-7C0B92.08201326042019@reader.eternal-september.org> |
| In reply to | #32764 |
In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>, peteolcott <Here@Home> wrote: > If a the query of the negation of a Prolog goal returns Yes then the query is > False: (F ? ﾂX) No. A successful negated goal is that it is unproveable with the resources provided. The problem is Prolog cannot always implement the excluded middle. -- :-<> Siri Seal of Disavowal #000-001. Disavowed. Denied. Deleted. @ 'I desire mercy, not sacrifice.' /|¥ The first law of discordiamism: The more energy This post / ¥ to make order is nore energy made into entropy. insults Islam. Mohammed
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-26 10:48 -0500 |
| Message-ID | <DKCdnb4BVabItV7BnZ2dnUU7-VvNnZ2d@giganews.com> |
| In reply to | #32765 |
On 4/26/2019 10:20 AM, Siri Cruise wrote: > In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>, > peteolcott <Here@Home> wrote: > >> If a the query of the negation of a Prolog goal returns Yes then the query is >> False: Provable(F, ~X) > > No. A successful negated goal is that it is unproveable with the resources > provided. The problem is Prolog cannot always implement the excluded middle. > That is not a problem at all. That is simply sound deductive inference working correctly. In this case the resources provided (Facts and Rules) are the formal system of symbolic logic. Not provable or refutable in the formal system is UNSOUND in this formal system. The formal proofs of symbolic logic are not discerning enough to see that every closed WFF that is neither True nor False is semantically unsound. -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | paul wallich <pw@panix.com> |
|---|---|
| Date | 2019-04-26 13:40 -0400 |
| Message-ID | <q9vfpm$qqa$1@reader2.panix.com> |
| In reply to | #32767 |
On 4/26/19 11:48 AM, peteolcott wrote: > On 4/26/2019 10:20 AM, Siri Cruise wrote: >> In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>, >> peteolcott <Here@Home> wrote: >> >>> If a the query of the negation of a Prolog goal returns Yes then the >>> query is >>> False: Provable(F, ~X) >> >> No. A successful negated goal is that it is unproveable with the >> resources >> provided. The problem is Prolog cannot always implement the excluded >> middle. >> > > That is not a problem at all. That is simply sound deductive inference > working correctly. In this case the resources provided (Facts and Rules) > are the formal system of symbolic logic. Not provable or refutable in > the formal system is UNSOUND in this formal system. > > The formal proofs of symbolic logic are not discerning enough to see that > every closed WFF that is neither True nor False is semantically unsound. What you've done is to define the cases that give you trouble out of existence. By doing so, you've gotten rid of incompleteness for your system, but that says more about your system than about Goedel. (I'd argue that you've provided a meta-proof of Goedel, but the margin of this point is too small to contain it.) paul
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-01 15:10 -0500 |
| Message-ID | <xaCdnYk8ZvLfYFTBnZ2dnUU7-fOdnZ2d@giganews.com> |
| In reply to | #32769 |
On 4/26/2019 12:40 PM, paul wallich wrote: > On 4/26/19 11:48 AM, peteolcott wrote: >> On 4/26/2019 10:20 AM, Siri Cruise wrote: >>> In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>, >>> peteolcott <Here@Home> wrote: >>> >>>> If a the query of the negation of a Prolog goal returns Yes then the query is >>>> False: Provable(F, ~X) >>> >>> No. A successful negated goal is that it is unproveable with the resources >>> provided. The problem is Prolog cannot always implement the excluded middle. >>> >> >> That is not a problem at all. That is simply sound deductive inference >> working correctly. In this case the resources provided (Facts and Rules) >> are the formal system of symbolic logic. Not provable or refutable in >> the formal system is UNSOUND in this formal system. >> >> The formal proofs of symbolic logic are not discerning enough to see that >> every closed WFF that is neither True nor False is semantically unsound. > > What you've done is to define the cases that give you trouble out of existence. By doing so, you've gotten rid of incompleteness for your system, but that says more about your system than about Goedel. (I'd argue that you've provided a meta-proof of > Goedel, but the margin of this point is too small to contain it.) > > paul > [Deductively Sound Formal Proofs] 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]
| From | Siebe de Vos <siebe@de-vos.de> |
|---|---|
| Date | 2019-04-26 17:24 +0200 |
| Message-ID | <q9v7qv$ga5$1@gioia.aioe.org> |
| In reply to | #32764 |
(It's Friday evening, so I allow myself this little reply:) You might be a good example of your own bottom quote. On 26/04/2019 16.58, peteolcott wrote: > [Prolog, etc.] > > This simple little system shows that Gödel's Incompleteness Theorem > and the Tarski Undefinability Theorem are false. > > https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems > > -- > Copyright 2019 Pete Olcott All rights reserved > > "Great spirits have always encountered violent > opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-26 10:51 -0500 |
| Message-ID | <DKCdnbkBVaZCtV7BnZ2dnUU7-VudnZ2d@giganews.com> |
| In reply to | #32766 |
On 4/26/2019 10:24 AM, Siebe de Vos wrote: > (It's Friday evening, so I allow myself this little reply:) You might be a good example of your own bottom quote. > > On 26/04/2019 16.58, peteolcott wrote: >> [Prolog, etc.] >> >> This simple little system shows that Gödel's Incompleteness Theorem >> and the Tarski Undefinability Theorem are false. >> >> https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems >> >> -- >> Copyright 2019 Pete Olcott All rights reserved >> >> "Great spirits have always encountered violent >> opposition from mediocre minds." Albert Einstein > The only way to know for sure is to find at least one valid counter-example to my assertion. -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Kaz Kylheku <847-115-0292@kylheku.com> |
|---|---|
| Date | 2019-04-26 17:48 +0000 |
| Message-ID | <20190426104732.755@kylheku.com> |
| In reply to | #32768 |
["Followup-To:" header set to comp.lang.lisp.] On 2019-04-26, peteolcott <Here@Home> wrote: > The only way to know for sure is to find at least one valid > counter-example to my assertion. Warning: numerous past debates with Peter Olcott have convinced me that he doesn't know what a counter-example is, and such.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-26 17:10 -0500 |
| Message-ID | <9PmdnWnPA8xIHF7BnZ2dnUU7-SudnZ2d@giganews.com> |
| In reply to | #32770 |
On 4/26/2019 12:48 PM, Kaz Kylheku wrote: > ["Followup-To:" header set to comp.lang.lisp.] > On 2019-04-26, peteolcott <Here@Home> wrote: >> The only way to know for sure is to find at least one valid >> counter-example to my assertion. > > Warning: numerous past debates with Peter Olcott have convinced me that > he doesn't know what a counter-example is, and such. > Heh I was wondering where you had gone, great to talk to you again. -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-26 17:22 -0500 |
| Message-ID | <rsqdnaWxiMopGV7BnZ2dnUU7-KvNnZ2d@giganews.com> |
| In reply to | #32770 |
On 4/26/2019 12:48 PM, Kaz Kylheku wrote: > ["Followup-To:" header set to comp.lang.lisp.] > On 2019-04-26, peteolcott <Here@Home> wrote: >> The only way to know for sure is to find at least one valid >> counter-example to my assertion. > > Warning: numerous past debates with Peter Olcott have convinced me that > he doesn't know what a counter-example is, and such. > I have come a very long way since the last time that we talked four years ago. Converting formal proofs of symbolic logic to conform to the sound deductive inference model: Then True(X) means Provable(X) and False(X) mean Provable(¬X) Leaving everything else as Unsound(X). This simple little system correctly refutes Gödel Incompleteness and Tarski Undefinability. Eliminating Undecidability and Incompleteness in Formal Systems https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Kaz Kylheku <847-115-0292@kylheku.com> |
|---|---|
| Date | 2019-04-27 01:13 +0000 |
| Message-ID | <20190426174714.286@kylheku.com> |
| In reply to | #32773 |
["Followup-To:" header set to comp.lang.lisp.] On 2019-04-26, peteolcott <Here@Home> wrote: > On 4/26/2019 12:48 PM, Kaz Kylheku wrote: >> ["Followup-To:" header set to comp.lang.lisp.] >> On 2019-04-26, peteolcott <Here@Home> wrote: >>> The only way to know for sure is to find at least one valid >>> counter-example to my assertion. >> >> Warning: numerous past debates with Peter Olcott have convinced me that >> he doesn't know what a counter-example is, and such. >> > > I have come a very long way since the last time that we talked four > years ago. If you aren't doing this in some kind of Lisp, though, it's off topic in comp.lang.lisp. > Converting formal proofs of symbolic logic to conform to the sound > deductive inference model: > > Then True(X) means Provable(X) and False(X) mean Provable(¬X) Leaving > everything else as Unsound(X). If all truths are provable, and anything not provable is false, then the system has been weakened; it is incomplete. Gödel's work is not restricted to examining the properties of a system which conforms to these constraints; it speaks about a more general system in which a truth can be unprovable. (You can wish that that system didn't exist, but that doesn't make it go away.) Similarly, in computing, we could restrict ourselves to a programming language that has only bounded loops and no recursion. Then claim, look, everything halts! Everything surely halts in that language which conforms to those restrictions, but not in a model of computation that doesn't have those restrictions. That's all I'm going to say on the subject, except for this: If True(X) means Provable(X), and only *only* True(X) means that, then that means your system has no axioms; how can it exist and do anything useful? Formal systems require axioms: the basic propositions that are painted as true rather than proven, from which other things follow. "Provable" is synonymous with "derivable from axioms". How could you have forgotten these? Gödel's work informs us, essentially, that the syntax of formal systems is capable of expressing new axioms. These are well-formed statements which do not conflict with any of the existing axioms, yet which we are not able to derive from those axioms either: they relate to the existing axioms in the same way that those axioms to each other. (Just like Euclid's Fifth Postulate can't be proven from the other four. It either has to be accepted, rejected (resulting in a weaker form of geometry) or replaced with different versions (leading to alternative geometries). Contrary to your past claims, you have not found a devastating mistake in Gödel's work; nobody has. It stands.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 11:23 -0500 |
| Message-ID | <SIOdnf4c_uZsHFnBnZ2dnUU7-QfNnZ2d@giganews.com> |
| In reply to | #32774 |
On 4/26/2019 8:13 PM, Kaz Kylheku wrote: > ["Followup-To:" header set to comp.lang.lisp.] > On 2019-04-26, peteolcott <Here@Home> wrote: >> On 4/26/2019 12:48 PM, Kaz Kylheku wrote: >>> ["Followup-To:" header set to comp.lang.lisp.] >>> On 2019-04-26, peteolcott <Here@Home> wrote: >>>> The only way to know for sure is to find at least one valid >>>> counter-example to my assertion. >>> >>> Warning: numerous past debates with Peter Olcott have convinced me that >>> he doesn't know what a counter-example is, and such. >>> >> >> I have come a very long way since the last time that we talked four >> years ago. > > If you aren't doing this in some kind of Lisp, though, it's off topic in > comp.lang.lisp. > >> Converting formal proofs of symbolic logic to conform to the sound >> deductive inference model: >> >> Then True(X) means Provable(X) and False(X) mean Provable(¬X) Leaving >> everything else as Unsound(X). > > If all truths are provable, and anything not provable is false, then the > system has been weakened; it is incomplete. > That is nothing like what I just said. > Gödel's work is not restricted to examining the properties of > a system which conforms to these constraints; it speaks about a more > general system in which a truth can be unprovable. > Truth cannot possibly be unprovable in the sound deductive inference model. Within the sound deductive inference model there is a (connected sequence of valid deductions from true premises to a true conclusion) thus unlike the formal proofs of symbolic logic provability cannot diverge from truth. > (You can wish that that system didn't exist, but that doesn't make > it go away.) > > Similarly, in computing, we could restrict ourselves to a programming > language that has only bounded loops and no recursion. Then claim, > look, everything halts! > > Everything surely halts in that language which conforms to those > restrictions, but not in a model of computation that doesn't have those > restrictions. > > That's all I'm going to say on the subject, except for this: > > If True(X) means Provable(X), and only *only* True(X) means that, then > that means your system has no axioms; how can it exist and do anything > useful? > > Formal systems require axioms: the basic propositions that are painted > as true rather than proven, from which other things follow. "Provable" > is synonymous with "derivable from axioms". How could you have > forgotten these? Formalizing the Sound Deductive Inference Model in Symbolic Logic Axiom(0) Stipulates** this definition of Axiom: Expressions of language defined to have the semantic value of Boolean True. Provides the symbolic logic equivalent of true premises. Stipulating** this specification of True and False: (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥) 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)) Thus stipulating** that consequences are provable from axioms. Stipulating** that formal systems are Boolean: Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x)) Screens out semantically unsound sentences as not belonging to the formal system. > > Gödel's work informs us, essentially, that the syntax of formal systems is > capable of expressing new axioms. These are well-formed statements > which do not conflict with any of the existing axioms, yet which we are > not able to derive from those axioms either: they relate to the existing > axioms in the same way that those axioms to each other. (Just like > Euclid's Fifth Postulate can't be proven from the other four. It either > has to be accepted, rejected (resulting in a weaker form of geometry) or > replaced with different versions (leading to alternative geometries). > > Contrary to your past claims, you have not found a devastating mistake > in Gödel's work; nobody has. It stands. > -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Kaz Kylheku <847-115-0292@kylheku.com> |
|---|---|
| Date | 2019-04-27 18:26 +0000 |
| Message-ID | <20190427112403.568@kylheku.com> |
| In reply to | #32776 |
On 2019-04-27, peteolcott <Here@Home> wrote: > Truth cannot possibly be unprovable in the sound deductive inference model. Again, only if it that model contains no axioms. Axioms are not provable; they are declared true as part of the basis of the system. You're really still not brushed up on even a second year university level understanding of this stuff.
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2019-04-27 14:44 -0700 |
| Message-ID | <87bm0rced5.fsf@nightsong.com> |
| In reply to | #32777 |
Kaz Kylheku <847-115-0292@kylheku.com> writes: >> Truth cannot possibly be unprovable in the sound deductive inference model. > Again, only if it that model contains no axioms. Axioms are not > provable; they are declared true as part of the basis of the system. Kaz, can you stop responding to that guy?
[toc] | [prev] | [next] | [standalone]
| From | Kaz Kylheku <847-115-0292@kylheku.com> |
|---|---|
| Date | 2019-04-28 03:40 +0000 |
| Message-ID | <20190427204016.643@kylheku.com> |
| In reply to | #32778 |
On 2019-04-27, Paul Rubin <no.email@nospam.invalid> wrote: > Kaz Kylheku <847-115-0292@kylheku.com> writes: >>> Truth cannot possibly be unprovable in the sound deductive inference model. >> Again, only if it that model contains no axioms. Axioms are not >> provable; they are declared true as part of the basis of the system. > > Kaz, can you stop responding to that guy? Done.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 16:48 -0500 |
| Message-ID | <kamdna0CMN-tU1nBnZ2dnUU7-UvNnZ2d@giganews.com> |
| In reply to | #32777 |
On 4/27/2019 1:26 PM, Kaz Kylheku wrote: > On 2019-04-27, peteolcott <Here@Home> wrote: >> Truth cannot possibly be unprovable in the sound deductive inference model. > > Again, only if it that model contains no axioms. Axioms are not > provable; they are declared true as part of the basis of the system. > > You're really still not brushed up on even a second year university > level understanding of this stuff. > I have spent 22 years and 12,000 hours on this. You are not picking apart my reasoning to see that it is correct. You are only assuming that I must be wrong because that is what you were taught to believe. -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2019-04-27 14:52 -0700 |
| Message-ID | <877ebfcdzc.fsf@nightsong.com> |
| In reply to | #32779 |
peteolcott <Here@Home> writes: > I have spent 22 years and 12,000 hours on this. http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 17:44 -0500 |
| Message-ID | <XIKdnYH1mOzZRlnBnZ2dnUU7-LXNnZ2d@giganews.com> |
| In reply to | #32780 |
On 4/27/2019 4:52 PM, Paul Rubin wrote: > peteolcott <Here@Home> writes: >> I have spent 22 years and 12,000 hours on this. > > http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf > IT ELIMINATES INCOMPLETENESS AND INCONSISTENCY OF FORMAL SYSTEMS NO VALID COUNTER-EXAMPLE EXISTS SHOWING OTHERWISE I DARE YOU TO FIND ONE All that I do is translate the formal proofs to theorem consequences of symbolic logic to conform to the sound deductive inference model. Axioms are merely expressions of language that have been defined to have the semantic value of Boolean true. I made this much simpler for people that do not know symbolic logic: True(X) is Provable(X) from Axioms. False(X) is Provable(¬X) from Axioms. Otherwise Unsound(X). Here it is in symbolic logic: 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)) Eliminating Undecidability and Incompleteness in Formal Systems https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Jeff Barnett <jbb@notatt.com> |
|---|---|
| Date | 2019-04-27 17:12 -0600 |
| Message-ID | <qa2nle$fk8$1@dont-email.me> |
| In reply to | #32780 |
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. PO fits the article's profile to a tee: he claims to be in his 60's, to have spent thousands of hours, keeps cleaning and pushing the same mistakes over and over again, and is basically a very poor mathematician who believes that PROLOG represents real and deep logic systems. I have been leaning towards troll rather than ignoramus but the article gives me a third choice: trisector! I'll keep it in mind. The thing I find interesting is that most people, including me, find it so hard to not respond to his gibberish. The first reaction is to help a lost soul back onto the path of truth (caps?) while the second reaction is mostly a reaction to a hard challenge like trying to stare down a lizard. -- Jeff Barnett
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 18:41 -0500 |
| Message-ID | <-4OdncjBPcoXdVnBnZ2dnUU7-bGdnZ2d@giganews.com> |
| In reply to | #32786 |
On 4/27/2019 6:12 PM, Jeff Barnett 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. > > PO fits the article's profile to a tee: he claims to be in his 60's, to have spent thousands of hours, keeps cleaning and pushing the same mistakes over and over again, and is basically a very poor mathematician who believes that PROLOG represents real and > deep logic systems. I never said that dingle berry. I said that the Prolog inference model corresponds to the sound deductive inference model. > I have been leaning towards troll rather than ignoramus but the article gives me a third choice: trisector! I'll keep it in mind. > > The thing I find interesting is that most people, including me, find it so hard to not respond to his gibberish. The first reaction is to help a lost soul back onto the path of truth (caps?) while the second reaction is mostly a reaction to a hard > challenge like trying to stare down a lizard. -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
Page 1 of 4 [1] 2 3 4 Next page →
Back to top | Article view | comp.lang.lisp
csiph-web