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 2 of 4 — ← Prev page 1 [2] 3 4 Next page →
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 18:59 -0500 |
| Message-ID | <a9OdncSG8p9UcVnBnZ2dnUU7-UvNnZ2d@giganews.com> |
| In reply to | #32787 |
On 4/27/2019 6:41 PM, peteolcott wrote:
> 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.
****************************************************************
QUIT BEING A JACKASS AND TAKE FIVE MINUTES TO STUDY IT !!!
****************************************************************
Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Stipulating** this specification of True and 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))
Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
The following logic sentence is refuted on the basis of Axiom(3)
∃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.
Making the following paragraph false:
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried out,
there are statements of the language of F which can neither be proved
nor disproved in F. (Raatikainen 2018)
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 | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2019-04-27 17:10 -0700 |
| Message-ID | <875zqzoupy.fsf@nightsong.com> |
| In reply to | #32786 |
Jeff Barnett <jbb@notatt.com> writes: > believes that PROLOG represents real and deep logic systems. I don't know Prolog but have been wondering what kind of logic it uses. I.e. I thought that it basically solves constraint satisfaction problems in what amounts to propositional logic. That is in fact a decidable system, but it's a very weak one, being unable to express propositions about arithmetic. Can one write the twin prime conjecture in Prolog? OTOH, the OP says propositions are true (provable), false (the negation is provable), or unsound. If "unsound" just means "unprovable in the given theory", then fine, that's what I'm used to. Maybe he adds a philosophical claim that the statement then doesn't have a truth value, so there is no such thing as an intended model. I can live with that, but the terminology is so weird and vague as to not have much meaning. OP, please read a logic book and use standard terminology if you want anyone to understand you. I liked Enderton's "A Mathematical Introduction to Logic" though it might be considered old-fashioned by onw.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 19:44 -0500 |
| Message-ID | <ypCdnWxXxrTDalnBnZ2dnUU7-WvNnZ2d@giganews.com> |
| In reply to | #32789 |
On 4/27/2019 7:10 PM, Paul Rubin wrote:
> Jeff Barnett <jbb@notatt.com> writes:
>> believes that PROLOG represents real and deep logic systems.
>
> I don't know Prolog but have been wondering what kind of logic it uses.
> I.e. I thought that it basically solves constraint satisfaction problems
> in what amounts to propositional logic. That is in fact a decidable
> system, but it's a very weak one, being unable to express propositions
> about arithmetic. Can one write the twin prime conjecture in Prolog?
>
> OTOH, the OP says propositions are true (provable), false (the negation
> is provable), or unsound. If "unsound" just means "unprovable in the
> given theory", then fine, that's what I'm used to.
Within the sound deductive inference model unsound simply means not
provable and the negation is also not provable.
In other words if its not True or False then its Unsound.
> Maybe he adds a
> philosophical claim that the statement then doesn't have a truth value,
> so there is no such thing as an intended model. I can live with that,
> but the terminology is so weird and vague as to not have much meaning.
>
It is exactly the same thing as unsound in the deductive logical inference
model show below.
It excludes all of the expressions of language that would otherwise
show undecidability or inconsistency as simply deductively unsound.
The 1931 Incompleteness Theorem and the Tarski Undefinability Theorem
simply become 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.
> OP, please read a logic book and use standard terminology if you want
> anyone to understand you. I liked Enderton's "A Mathematical
> Introduction to Logic" though it might be considered old-fashioned by
> onw.
>
I only mean this very simple idea, no textbook needed:
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.
--
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 19:26 -0600 |
| Message-ID | <qa2vgj$foa$1@dont-email.me> |
| In reply to | #32789 |
Paul Rubin wrote on 4/27/2019 6:10 PM: > Jeff Barnett <jbb@notatt.com> writes: >> believes that PROLOG represents real and deep logic systems. > > I don't know Prolog but have been wondering what kind of logic it uses. > I.e. I thought that it basically solves constraint satisfaction problems > in what amounts to propositional logic. That is in fact a decidable > system, but it's a very weak one, being unable to express propositions > about arithmetic. Can one write the twin prime conjecture in Prolog? Probably not. I haven't looked at PROLOG for a while but for at least the first decade of its existence it only allowed Horn clauses - pretty week stuff. It basically was like some of the old AI by-rule systems with a vanilla execution engine. With Horn clauses you could not imply a negative nor could anything be implied by a negative. Total toy. > OTOH, the OP says propositions are true (provable), false (the negation > is provable), or unsound. If "unsound" just means "unprovable in the > given theory", then fine, that's what I'm used to. Maybe he adds a > philosophical claim that the statement then doesn't have a truth value, > so there is no such thing as an intended model. I can live with that, > but the terminology is so weird and vague as to not have much meaning. Don't assume the OP aka PO knows anything of which he speaks. His math, logic, and programming skills are pathetic. His abilities to concentrate and check what he is saying are non existent. That is why he can publish a half dozen versions of the same gibberish, trying to correct minor issues, in a single day. In anther area, he would be accused of premature ejaculation and sent to a urologist for a consultation. I think the current issues need a psychiatrist prescribing meds. > OP, please read a logic book and use standard terminology if you want > anyone to understand you. I liked Enderton's "A Mathematical > Introduction to Logic" though it might be considered old-fashioned by > onw. 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. -- Jeff Barnett
[toc] | [prev] | [next] | [standalone]
| From | Paul Rubin <no.email@nospam.invalid> |
|---|---|
| Date | 2019-04-27 18:52 -0700 |
| Message-ID | <87ef5mkia5.fsf@nightsong.com> |
| In reply to | #32793 |
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.
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-27 21:38 -0500 |
| Message-ID | <j46dnWVt_8qrj1jBnZ2dnUU7-LPNnZ2d@giganews.com> |
| In reply to | #32794 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-29 21:53 -0500 |
| Message-ID | <TOydnSJT068oJVrBnZ2dnUU7-dPNnZ2d@giganews.com> |
| In reply to | #32796 |
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]
| From | "Pascal J. Bourguignon" <pjb@informatimago.com> |
|---|---|
| Date | 2019-04-30 07:08 +0200 |
| Message-ID | <m2k1fcxepj.fsf@despina.home> |
| In reply to | #32808 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-30 00:41 -0500 |
| Message-ID | <wLydnVr9gKKRfVrBnZ2dnUU7-fvNnZ2d@giganews.com> |
| In reply to | #32811 |
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]
| From | taruss@google.com |
|---|---|
| Date | 2019-04-30 09:23 -0700 |
| Message-ID | <40f4acd5-de82-4b2f-94b6-b419ae5b23b6@googlegroups.com> |
| In reply to | #32812 |
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. 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/
[toc] | [prev] | [next] | [standalone]
| From | "Pascal J. Bourguignon" <pjb@informatimago.com> |
|---|---|
| Date | 2019-04-30 18:47 +0200 |
| Message-ID | <m2ftpzxwxn.fsf@despina.home> |
| In reply to | #32815 |
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). > 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/ -- __Pascal J. Bourguignon__ http://www.informatimago.com
[toc] | [prev] | [next] | [standalone]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-04-30 12:02 -0500 |
| Message-ID | <lOKdnRIm49IF4lXBnZ2dnUU7-QnNnZ2d@giganews.com> |
| In reply to | #32816 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-01 07:50 -0500 |
| Message-ID | <uqOdne-V7rqVC1TBnZ2dnUU7-evNnZ2d@giganews.com> |
| In reply to | #32818 |
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]
| From | "Pascal J. Bourguignon" <pjb@informatimago.com> |
|---|---|
| Date | 2019-05-01 14:53 +0200 |
| Message-ID | <m27eba72vb.fsf@despina.home> |
| In reply to | #32822 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-01 09:29 -0500 |
| Message-ID | <9r2dnaPWIqTcMFTBnZ2dnUU7-LWdnZ2d@giganews.com> |
| In reply to | #32823 |
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]
| From | "Pascal J. Bourguignon" <pjb@informatimago.com> |
|---|---|
| Date | 2019-05-01 18:37 +0200 |
| Message-ID | <m21s1i6sh1.fsf@despina.home> |
| In reply to | #32824 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-01 13:53 -0500 |
| Message-ID | <xJ6dnXe38YOidlTBnZ2dnUU7-TXNnZ2d@giganews.com> |
| In reply to | #32826 |
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]
| From | peteolcott <Here@Home> |
|---|---|
| Date | 2019-05-01 13:56 -0500 |
| Message-ID | <xJ6dnXa38YNEdlTBnZ2dnUU7-TVQAAAA@giganews.com> |
| In reply to | #32823 |
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]
| From | Keith Thompson <kst-u@mib.org> |
|---|---|
| Date | 2019-05-01 10:48 -0700 |
| Message-ID | <lnsgtyvzfh.fsf@kst-u.example.com> |
| In reply to | #32822 |
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]
| From | Bonita Montero <Bonita.Montero@gmail.com> |
|---|---|
| Date | 2019-05-01 20:25 +0200 |
| Message-ID | <qacoac$mlh$1@news.albasani.net> |
| In reply to | #32827 |
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]
Page 2 of 4 — ← Prev page 1 [2] 3 4 Next page →
Back to top | Article view | comp.lang.lisp
csiph-web