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

Groups > comp.lang.c > #143462 > unrolled thread

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

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

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) 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: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) Ike Naar <ike@iceland.freeshell.org> - 2019-04-27 21:56 +0000
                  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 16:58 -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 17:49 -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) 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) 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) bert <bert.hutchings@btinternet.com> - 2019-04-30 11:06 -0700
                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-01 00:51 -0500
                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) bert <bert.hutchings@btinternet.com> - 2019-05-01 03:21 -0700
                            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) peteolcott <Here@Home> - 2019-05-01 09:29 -0500
                                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) 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 16:44 -0500
                                      Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) David Brown <david.brown@hesbynett.no> - 2019-05-02 09:19 +0200
                                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) mark.bluemel@gmail.com - 2019-05-02 00:45 -0700
                                          Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) Tim Rentsch <tr.17687@z991.linuxsc.com> - 2019-05-02 09:56 -0700
                                        Re: Eliminating Undecidability and Incompleteness in Formal Systems (Prolog already does this) peteolcott <Here@Home> - 2019-05-02 09:58 -0500
                                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) 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

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

#143536

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]

#143561

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]

#143597

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]

#143601

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]

#143483

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]

#143555

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

csiph-web