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

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

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

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

Contents

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

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

#9211

On 5/1/2019 12:48 PM, Keith Thompson wrote:
> 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.
> 

You have been proven to be incorrect in that people continue to
respond. It is most relevant to Prolog, it is next most relevant
to Lisp because Lisp is an AI language. I might drop C++, and C
off the list of cross-posts.

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]

#9218

On 01/05/2019 21:01, peteolcott wrote:
> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>> 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.
>>
> 
> You have been proven to be incorrect in that people continue to
> respond. It is most relevant to Prolog, it is next most relevant
> to Lisp because Lisp is an AI language. I might drop C++, and C
> off the list of cross-posts.
> 

Please do drop C and C++ groups.  I can't answer for prolog or lisp 
groups, as I do not follow these.  But I note that everyone else in your 
threads - baring those like me who are complaining - has dropped the C 
and C++ groups.  Thus all we see are endless posts from you, apparently 
replying to yourself, and with no content of any interest to our groups. 
  It may be that you have discovered some important result in formal 
systems, but we in the C and C++ groups are not interested.  (If anyone 
from these groups disagrees with me, please say so.)

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

#9217

On 5/1/2019 12:48 PM, Keith Thompson wrote:
> 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.
> 

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

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

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

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

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

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 more than eight decades.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#9189

On 4/29/2019 4:53 PM, paul wallich wrote:
> On 4/27/19 7: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 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.
> 
> I think that the problem isn't trisection exactly but rather a sort of weird semantic capture. The term "unsound" is used to tag the category "neither provable nor refutable" but that's -- within the system -- just a tag. The logical system, such as it is, 
> would work just as well if the tag were "NPNR" or "frabjous" or "charmed" or "boogabooga". But use the tag "unsound", and magically all of the senses of "unsound" from colloguial language and other logical systems suddenly get dragged in and pasted over 
> the top of what might as well be "frabjous".
> 
> Do some brains need better macro systems?

Sound deductive inference
(a) All dogs are mammals
(b) All mammals breath
(c) Therefore all dogs breath

Unsound deductive inference (false premise)
(a) All dogs are office buildings
(b) All office buildings have windows
(c) Therefore all dogs have windows

Unsound deductive inference (invalid inference)
(a) All dogs are mammals
(b) All fish swim
(c) Therefore all dogs breath


-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#9191

On 4/29/2019 7:22 PM, luserdroog 0wrote:
> On Monday, April 29, 2019 at 6:43:11 PM UTC-5, peteolcott wrote:
> 
>> Sound deductive inference
>> (a) All dogs are mammals
>> (b) All mammals breath
>> (c) Therefore all dogs breath
>>
>> Unsound deductive inference (false premise)
>> (a) All dogs are office buildings
>> (b) All office buildings have windows
>> (c) Therefore all dogs have windows
>>
>> Unsound deductive inference (invalid inference)
>> (a) All dogs are mammals
>> (b) All fish swim
>> (c) Therefore all dogs breath
>>
>>
> 
> Nit: the verb is "breathe", breath is the noun as in
> "dog's have bad breath."
> 
> This looks almost like Aristotle's syllogisms. These
> were treated in a very interesting book by Lukasiewicz.
> 

The only reason that incompleteness is provable is that the formal
proofs of symbolic logic diverge from that simple pattern.

Summing it up:
True(X) is Provable(X) from True Premises.
False(X) is Provable(¬X) from True Premises.
Otherwise Unsound(X).

Technically {Unsound} only applies to arguments and not to single
expressions of language I had to extend the meaning of the term
{Unsound} when I applied the concept of soundness to formal proofs.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#9213

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]

#9215

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.  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.
> 

[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]

#9216

On 4/27/2019 8:26 PM, Jeff Barnett wrote:
> 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.
> 

[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]

#9222

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]

#9223

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]

#9169

So you have renamed that X is undecided to unsound.
Thats quite original and crazy at the same time.

Comgratulations, you obtained a degree in crankomatic. 

Am Samstag, 27. April 2019 00:22:49 UTC+2 schrieb peteolcott:
> 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]

#9168

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]

#9205

Is this a second "Amine Moulay Ramdane"?
According to his manic posting-frequency he might be.

[toc] | [prev] | [standalone]

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

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

csiph-web