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 | 14 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 4 of 4 — ← Prev page 1 2 3 [4]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-02 22:04 -0500 |
| Message-ID | <Idydna8IQP0_MlbBnZ2dnUU7-QHNnZ2d@giganews.com> |
| In reply to | #32845 |
On 5/2/2019 6:21 PM, Kaz Kylheku wrote: > On 2019-05-02, Jeff Barnett <jbb@notatt.com> wrote: >> Stefan Monnier wrote on 5/2/2019 1:11 PM: >>>>> I have spent 22 years and 12,000 hours on this. >>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf >>> >>> OK, I'll bite: how do we do the equivalent of showing a "computer >>> printout giving the errors in the construction for angles of various >>> sizes"? >> >> Steps in a construction are representable by an algebraic formula. These >> formulas can be evaluated for specific sets of values (such as each >> angle between 0 and 360 degrees). The total imprecision caused by >> floating point is very small in comparison to the error when one asks >> "Is this a third of the input angle?". Of course if you were using Lisp, >> you might be able to do most things with rationals and get more exact >> answers. Dudley was just trying to show his correspondents that they >> were mistaken. > > I suspect Stefan might mean "how do we do the equivalent of ... in this > present situation, in the domain of incompleteness and halting." > Can you suggest any better places where I can get decent peer review? -- 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-05-02 21:13 -0600 |
| Message-ID | <qagbkh$sn4$1@dont-email.me> |
| In reply to | #32845 |
Kaz Kylheku wrote on 5/2/2019 5:21 PM: > On 2019-05-02, Jeff Barnett <jbb@notatt.com> wrote: >> Stefan Monnier wrote on 5/2/2019 1:11 PM: >>>>> I have spent 22 years and 12,000 hours on this. >>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf >>> >>> OK, I'll bite: how do we do the equivalent of showing a "computer >>> printout giving the errors in the construction for angles of various >>> sizes"? >> >> Steps in a construction are representable by an algebraic formula. These >> formulas can be evaluated for specific sets of values (such as each >> angle between 0 and 360 degrees). The total imprecision caused by >> floating point is very small in comparison to the error when one asks >> "Is this a third of the input angle?". Of course if you were using Lisp, >> you might be able to do most things with rationals and get more exact >> answers. Dudley was just trying to show his correspondents that they >> were mistaken. > > I suspect Stefan might mean "how do we do the equivalent of ... in this > present situation, in the domain of incompleteness and halting." A while ago PO stated he had written a Turing Machine that did what one of the impossibility Lemmas said was (you guessed it) impossible. So we asked to see it since it would be trivial to code up a TM interpreter and see how his puppy played. That would satisfy Stefan's quest I think. However, this PO announcement like all of the PO claims was bogus. In fact after everybody said "show it to me" and he couldn't, he started starting maybe five or more new threads a day trying to bury his phony bologna. Every few days someone asks to see the TM definition and PO dances all around and doesn't admit his claim was premature. The situation would be rather humorous if we all weren't witnessing a human life totally wasted -- Jeff Barnett
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-02 22:42 -0500 |
| Message-ID | <OoqdnVAli4wLJVbBnZ2dnUU7-W-dnZ2d@giganews.com> |
| In reply to | #32847 |
On 5/2/2019 10:13 PM, Jeff Barnett wrote: > Kaz Kylheku wrote on 5/2/2019 5:21 PM: >> On 2019-05-02, Jeff Barnett <jbb@notatt.com> wrote: >>> Stefan Monnier wrote on 5/2/2019 1:11 PM: >>>>>> I have spent 22 years and 12,000 hours on this. >>>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf >>>> >>>> OK, I'll bite: how do we do the equivalent of showing a "computer >>>> printout giving the errors in the construction for angles of various >>>> sizes"? >>> >>> Steps in a construction are representable by an algebraic formula. These >>> formulas can be evaluated for specific sets of values (such as each >>> angle between 0 and 360 degrees). The total imprecision caused by >>> floating point is very small in comparison to the error when one asks >>> "Is this a third of the input angle?". Of course if you were using Lisp, >>> you might be able to do most things with rationals and get more exact >>> answers. Dudley was just trying to show his correspondents that they >>> were mistaken. >> >> I suspect Stefan might mean "how do we do the equivalent of ... in this >> present situation, in the domain of incompleteness and halting." > > A while ago PO stated he had written a Turing Machine that did what one of the impossibility Lemmas said was (you guessed it) impossible. So we asked to see it since it would be trivial to code up a TM interpreter and see how his puppy played. That would > satisfy Stefan's quest I think. However, this PO announcement like all of the PO claims was bogus. In fact after everybody said "show it to me" and he couldn't, he started starting maybe five or more new threads a day trying to bury his phony bologna. > Every few days someone asks to see the TM definition and PO dances all around and doesn't admit his claim was premature. The situation would be rather humorous if we all weren't witnessing a human life totally wasted Here is the gist: Releasing the key results of my life's work before these results are in their most credible form seriously risks total failure that these results will ever be seriously reviewed. Here are more details: On 5/2/2019 11:12 AM, peteolcott wrote: I have both TM H and TM Ĥ such that H decides halting for input pair: (Ĥ, Ĥ) for a long time now, ever since I first claimed it. What I don't have is a fully operational UTM interpreter that can actually execute TM H on input pair: (Ĥ, Ĥ) providing an full execution trace. I will begin working on this full time as soon as my other higher priority things have been completed. Because programming requires such sustained continuous concentration: I refrain from working on this at all because it would cause me to fail on my other higher priority things. I would not be able to break myself away from the programming fearing that I would lose far too much productivity. On 5/2/2019 6:01 PM, Ben Bacarisse wrote: > peteolcott <Here@Home> writes: > >> On 5/2/2019 5:23 PM, Ben Bacarisse wrote: >>> peteolcott <Here@Home> writes: >>> >>>> On 5/2/2019 10:45 AM, Ben Bacarisse wrote: >>> <cut> >>>>> You don't have the TM do you? You never did, did you? It was just a >>>>> vain boast. Anyway, 20 weeks and counting... >>>> >>>> I have both TM H and TM Ĥ such that H decides halting for input pair: >>>> (Ĥ, Ĥ) for a long time now, ever since I first claimed it. >>> >>> Yet you don't post it. You don't post it because >> >> I TOTALLY DISTRUST YOU. >> YOU ARE GOING TO RIP IT TO SHREDS EVEN IF IT IS INFALLIBLE. > > There is a world beyond me. In reality you should not bother posting > here at all. The TM you claim needs to be published in a major journal. (1) I have significant negative credibility. (2) I don't write like a PhD at all this gets whatever I say dismissed out-of-hand without review. (3) I am not yet ever understood. My way around this is to communicate an increasingly clearer perspective until it is unequivocally understood that I am self-evidently correct. > The fact that you waste you time taking to people like me is just > another proof that you a crank with nothing worth saying. Unfortunately I must have feedback to increase the clarity of my words because all of my words have always seemed perfectly clear to me. > the only thing you have to make you feel worthwhile is posting on > Usenet, so you have no choice. > > But now we know: you won't post this remarkable work because you are > scared of what I'll say. I am flattered. > At the point in time when I am infallibly correct 99.9% of reviewers will dismiss whatever I say out-of-hand merely because what I am doing is itself totally unbelievable. I only need one very credible reviewer to bless my work to be able to get more reviews. If before I release my final results the preliminary results have a serious negative review, then releasing even infallible results later on will never be reviewed at all. Releasing the key results of my life's work before these results are in their most credible form seriously risks total failure that these results will ever be seriously reviewed. -- 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-05-02 22:46 -0500 |
| Subject | Re: Eliminating Undecidability and Incompleteness in Formal Systems (Halting Problem) |
| Message-ID | <AvOdncqHUMc-JFbBnZ2dnUU7-eHNnZ2d@giganews.com> |
| In reply to | #32848 |
On 5/2/2019 10:42 PM, peteolcott wrote: > On 5/2/2019 10:13 PM, Jeff Barnett wrote: >> Kaz Kylheku wrote on 5/2/2019 5:21 PM: >>> On 2019-05-02, Jeff Barnett <jbb@notatt.com> wrote: >>>> Stefan Monnier wrote on 5/2/2019 1:11 PM: >>>>>>> I have spent 22 years and 12,000 hours on this. >>>>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf >>>>> >>>>> OK, I'll bite: how do we do the equivalent of showing a "computer >>>>> printout giving the errors in the construction for angles of various >>>>> sizes"? >>>> >>>> Steps in a construction are representable by an algebraic formula. These >>>> formulas can be evaluated for specific sets of values (such as each >>>> angle between 0 and 360 degrees). The total imprecision caused by >>>> floating point is very small in comparison to the error when one asks >>>> "Is this a third of the input angle?". Of course if you were using Lisp, >>>> you might be able to do most things with rationals and get more exact >>>> answers. Dudley was just trying to show his correspondents that they >>>> were mistaken. >>> >>> I suspect Stefan might mean "how do we do the equivalent of ... in this >>> present situation, in the domain of incompleteness and halting." >> >> A while ago PO stated he had written a Turing Machine that did what one of the impossibility Lemmas said was (you guessed it) impossible. So we asked to see it since it would be trivial to code up a TM interpreter and see how his puppy played. That would >> satisfy Stefan's quest I think. However, this PO announcement like all of the PO claims was bogus. In fact after everybody said "show it to me" and he couldn't, he started starting maybe five or more new threads a day trying to bury his phony bologna. >> Every few days someone asks to see the TM definition and PO dances all around and doesn't admit his claim was premature. The situation would be rather humorous if we all weren't witnessing a human life totally wasted > > Here is the gist: > Releasing the key results of my life's work before these results are in > their most credible form seriously risks total failure that these results > will ever be seriously reviewed. > > Here are more details: This is where the Linz proof is defined: http://liarparadox.org/Peter_Linz_HP(Pages_315-320).pdf > On 5/2/2019 11:12 AM, peteolcott wrote: > I have both TM H and TM Ĥ such that H decides halting for input pair: > (Ĥ, Ĥ) for a long time now, ever since I first claimed it. > > What I don't have is a fully operational UTM interpreter that can actually > execute TM H on input pair: (Ĥ, Ĥ) providing an full execution trace. > > I will begin working on this full time as soon as my other higher priority > things have been completed. Because programming requires such sustained > continuous concentration: > > I refrain from working on this at all because it would cause me to fail on > my other higher priority things. I would not be able to break myself away > from the programming fearing that I would lose far too much productivity. > -- 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-27 16:58 -0500 |
| Message-ID | <BJKdnVblWs_7TVnBnZ2dnUU7-UXNnZ2d@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. > THESE FOUR AXIOMS PROVIDE THE BASIS FOR COMPLETE CONSISTENT FORMAL SYSTEMS AND NO VALID COUNTER-EXAMPLE CAN BE FORMED TO SHOW OTHERWISE 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. 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 | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 17:13 -0500 |
| Message-ID | <EISdnZcPlq-ASVnBnZ2dnUU7-ePNnZ2d@giganews.com> |
| In reply to | #32777 |
On 4/27/2019 4:56 PM, Ike Naar wrote: > On 2019-04-27, Kaz Kylheku <847-115-0292@kylheku.com> 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. > > But this is wordplay. > If 'provable' means "can be derived from axioms" then it would seem sensible > to classify the axioms themselves as being provable. > No that would form a cyclic directed graph forming an infinite evaluation loop. To prove that an expression of language is an axiom merely requires looking it up on a finite list or matching it to an axiom schema, in other words any infinite set of axioms can be algorithmically compressed into a finite set of schema. 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 | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 17:28 -0500 |
| Message-ID | <WNudnc1gJs3xSlnBnZ2dnUU7-TnNnZ2d@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. > Axioms are merely expressions of language that have been defined to have the semantic value of Boolean true. A sound deductive inference model must have no contradictory axioms. True(X) is Provable(X) from True Premises. False(X) is Provable(¬X) from True Premises. Otherwise Unsound(X). This simple little system refutes Gödel's 1931 Incompleteness Theorem ∃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. Its refutation of the Tarski Undefinability Theorem requires the basis of the Tarski Undefinability Proof to be understood: http://liarparadox.org/Tarski_Proof_275_276.pdf The third step of the proof: (3) x ∉ Pr if and only if x ∈ Tr is refuted by this version of Axiom(1) x ∈ Pr ↔ x ∈ Tr -- 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-27 17:49 -0500 |
| Message-ID | <QYidnVnYH7IPQVnBnZ2dnUU7-L_NnZ2d@giganews.com> |
| In reply to | #32777 |
On 4/27/2019 4:33 PM, j4n bur53 wrote:
> Axioms are provable. Undecided sentences are not
> provable. Axioms are those things in a theory,
> that have the shortest proofs. Namely:
>
> Axiom |- Axiom
>
> Ever looked up the definition what a proof is? A proof
> is a sequence D1, ..., Dn, where Di is either an axiom
> or the result of applying an inference rule to some
>
http://liarparadox.org/Provable_Mendelson.pdf
> already derived statements. Now take n=1.
>
> Whats wrong with you guys?
>
Prolog people might know provable, other software engineers, not as much,
so I gave them this much simpler form:
Summing it up:
True(X) is Provable(X) from True Premises.
False(X) is Provable(¬X) from True Premises.
Otherwise Unsound(X).
When we define this as an Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Then we can replace the above "True Premises" with {Axiom}.
> Am Samstag, 27. April 2019 20:26:08 UTC+2 schrieb Kaz Kylheku:
>> 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.
>
--
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-05-01 15:10 -0500 |
| Message-ID | <xaCdnY48ZvKGYFTBnZ2dnUU7-fOdnZ2d@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. > [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 | Richard Damon <Richard@Damon-Family.org> |
|---|---|
| Date | 2019-05-04 15:05 -0400 |
| Message-ID | <polzE.414$fq3.286@fx07.iad> |
| In reply to | #32776 |
On 4/27/19 12:23 PM, peteolcott wrote: > 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. I will admit that I haven't followed this thread closely, but to me this seems to imply that this 'sound deductive inference model' must be somewhat weak in what it can express to be able to make such a claim. Yes, there are many statements which are provable true, and this can be shown with a valid proof from true premises and valid inferences leading to the conclusion. There are also many statements which are provable false, as you can prove their converse. If the logic system is sufficiently rich in capability, it would seem like, in general, proving that something can not be proven true or false is not easy, so it would seem hard to determine that something is 'unsound'. The issue is that there can be an incredibly large number of possible paths to combine known true premises with valid deductions to get more statements that are provably true, which can be combined with each other to get even more provably true statement. To be able to say that it will be impossible to find a path to the specified statement seems hard, unless the logic system is naturally weak and able to prove only a very limited set of statements. A great example of this would be the Four Color Map Theorem. For a very long time it was 'Unproved' and thus would seem to be declared 'Unsound' by this logic, but was eventually proved true.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-04 15:07 -0500 |
| Message-ID | <97WdnZYZv9mHbFDBnZ2dnUU7-RvNnZ2d@giganews.com> |
| In reply to | #32852 |
On 5/4/2019 2:05 PM, Richard Damon wrote: > On 4/27/19 12:23 PM, peteolcott wrote: >> 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. > > I will admit that I haven't followed this thread closely, but to me this > seems to imply that this 'sound deductive inference model' must be > somewhat weak in what it can express to be able to make such a claim. > Deductively Sound Formal Proofs https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs It simply filters out semantically incoherent expressions of language. These expressions were not filtered out previously because formal systems ignored semantic constraints. > Yes, there are many statements which are provable true, and this can be > shown with a valid proof from true premises and valid inferences leading > to the conclusion. There are also many statements which are provable > false, as you can prove their converse. > Every closed WFF left over is semantically incoherent. > If the logic system is sufficiently rich in capability, it would seem > like, in general, proving that something can not be proven true or false > is not easy, so it would seem hard to determine that something is > 'unsound'. Its all in my linked one page paper. > The issue is that there can be an incredibly large number of > possible paths to combine known true premises with valid deductions to > get more statements that are provably true, which can be combined with > each other to get even more provably true statement. To be able to say > that it will be impossible to find a path to the specified statement > seems hard, unless the logic system is naturally weak and able to prove > only a very limited set of statements. > If we simply leap to the chase: ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G))) The above logic sentence asserts that there are some closed WFF that are neither true or false. Axiom Schema(3) Deductively_Sound_Consequence(x) ↔ (True(x) ∨ False(x)) excludes expressions of language that do not evaluate to true or false as not belonging to the set of deductively sound consequences. > A great example of this would be the Four Color Map Theorem. For a very > long time it was 'Unproved' and thus would seem to be declared 'Unsound' > by this logic, but was eventually proved true. > -- Copyright 2019 Pete Olcott All rights reserved "Great spirits have always encountered violent opposition from mediocre minds." Albert Einstein
[toc] | [prev] | [next] | [standalone]
| From | Keith Thompson <kst-u@mib.org> |
|---|---|
| Date | 2019-04-26 19:43 -0700 |
| Message-ID | <ln7ebgyxq4.fsf@kst-u.example.com> |
| In reply to | #32764 |
peteolcott <Here@Home> writes:
> Prolog already implements the sound deductive inference model.
[...]
> This simple little system shows that Gödel's Incompleteness Theorem
> and the Tarski Undefinability Theorem are false.
[...]
Please restrict followups to relevant newsgroups. In particular,
this is off topic in comp.lang.c++ and comp.lang.c, and probably
in comp.lang.lisp as well.
--
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]
| From | Bonita Montero <Bonita.Montero@gmail.com> |
|---|---|
| Date | 2019-05-01 17:56 +0200 |
| Message-ID | <qacfje$75i$1@news.albasani.net> |
| In reply to | #32764 |
Is this a second "Amine Moulay Ramdane"? According to his manic posting-frequency he might be.
[toc] | [prev] | [next] | [standalone]
| From | Rabican <gavinschuette@gmail.com> |
|---|---|
| Date | 2019-05-06 05:51 -0700 |
| Message-ID | <ace3199c-feac-4600-b622-e0ee43564784@googlegroups.com> |
| In reply to | #32764 |
On Friday, April 26, 2019 at 10:58:40 AM UTC-4, peteolcott wrote: > 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 prolog for thewin!
[toc] | [prev] | [standalone]
Page 4 of 4 — ← Prev page 1 2 3 [4]
Back to top | Article view | comp.lang.lisp
csiph-web