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 1 of 3  [1] 2 3  Next page →

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

Prolog already implements the sound deductive inference model.
The Prolog Database is equivalent to a formal system.
Prolog Facts are equivalent to the Axioms of a formal system.
Prolog Rules are equivalent to the rules-of-inference of a formal system.
Prolog Queries are equivalent to the logic sentences of a formal system.
https://en.wikipedia.org/wiki/Prolog#Execution

If a the query of a Prolog goal returns Yes then the query is True: (F ⊢ X)
If a the query of the negation of a Prolog goal returns Yes then the query is False: (F ⊢ ¬X)

Otherwise the goal is neither provable nor refutable on the basis of the
Facts and Rules in the Prolog Database: ¬(True(F, X) ∨ False(F, X))

Here is the simplest way to explain how the formal proofs of symbolic
logic have been made to conform to the sound deductive inference model:

(1) If there is a (connected sequence of valid deductions from
true premises to a true conclusion) then X is TRUE:  (F ⊢ X).

(2) If there is a (connected sequence of valid deductions from
true premises to the negation of the conclusion) then X is FALSE:  (F ⊢ ¬X).

(3) otherwise X UNSOUND

We use the Axioms of formal systems in place of true premises and
the conclusion of a formal proof is called a consequence.

This simple little system shows that Gödel's Incompleteness Theorem
and the Tarski Undefinability Theorem are false.

https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems

-- 
Copyright 2019 Pete Olcott All rights reserved

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

[toc] | [next] | [standalone]

#143463

In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>,
 peteolcott <Here@Home> wrote:

> If a the query of the negation of a Prolog goal returns Yes then the query is 
> False: (F ? ﾂX)

No. A successful negated goal is that it is unproveable with the resources 
provided. The problem is Prolog cannot always implement the excluded middle.

-- 
:-<> Siri Seal of Disavowal #000-001. Disavowed. Denied. Deleted.    @
'I desire mercy, not sacrifice.'                                    /|¥
The first law of discordiamism: The more energy   This post         / ¥
to make order is nore energy made into entropy.   insults Islam.  Mohammed

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

#143465

On 4/26/2019 10:20 AM, Siri Cruise wrote:
> In article <2_ydnT3SYPULgV7BnZ2dnUU7-cnNnZ2d@giganews.com>,
>   peteolcott <Here@Home> wrote:
> 
>> If a the query of the negation of a Prolog goal returns Yes then the query is
>> False: Provable(F, ~X)
> 
> No. A successful negated goal is that it is unproveable with the resources
> provided. The problem is Prolog cannot always implement the excluded middle.
> 

That is not a problem at all. That is simply sound deductive inference
working correctly. In this case the resources provided (Facts and Rules)
are the formal system of symbolic logic. Not provable or refutable in
the formal system is UNSOUND in this formal system.

The formal proofs of symbolic logic are not discerning enough to see that
every closed WFF that is neither True nor False is semantically unsound.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#143466

On 4/26/2019 10:24 AM, Siebe de Vos wrote:
> (It's Friday evening, so I allow myself this little reply:) You might be a good example of your own bottom quote.
> 
> On 26/04/2019 16.58, peteolcott wrote:
>> [Prolog, etc.]
>>
>> This simple little system shows that Gödel's Incompleteness Theorem
>> and the Tarski Undefinability Theorem are false.
>>
>> https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems
>>
>> -- 
>> Copyright 2019 Pete Olcott All rights reserved
>>
>> "Great spirits have always encountered violent
>> opposition from mediocre minds." Albert Einstein
> 

The only way to know for sure is to find at least one valid
counter-example to my assertion.

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#143469

["Followup-To:" header set to comp.lang.lisp.]
On 2019-04-26, peteolcott <Here@Home> wrote:
> The only way to know for sure is to find at least one valid
> counter-example to my assertion.

Warning: numerous past debates with Peter Olcott have convinced me that
he doesn't know what a counter-example is, and such.

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

#143481

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]

#143482

["Followup-To:" header set to comp.lang.lisp.]
On 2019-04-26, peteolcott <Here@Home> wrote:
> On 4/26/2019 12:48 PM, Kaz Kylheku wrote:
>> ["Followup-To:" header set to comp.lang.lisp.]
>> On 2019-04-26, peteolcott <Here@Home> wrote:
>>> The only way to know for sure is to find at least one valid
>>> counter-example to my assertion.
>> 
>> Warning: numerous past debates with Peter Olcott have convinced me that
>> he doesn't know what a counter-example is, and such.
>> 
>
> I have come a very long way since the last time that we talked four
> years ago.

If you aren't doing this in some kind of Lisp, though, it's off topic in
comp.lang.lisp.

> Converting formal proofs of symbolic logic to conform to the sound
> deductive inference model:
>
> Then True(X) means Provable(X) and False(X) mean Provable(¬X) Leaving
> everything else as Unsound(X).

If all truths are provable, and anything not provable is false, then the
system has been weakened; it is incomplete.

Gödel's work is not restricted to examining the properties of
a system which conforms to these constraints; it speaks about a more
general system in which a truth can be unprovable.

(You can wish that that system didn't exist, but that doesn't make
it go away.)

Similarly, in computing, we could restrict ourselves to a programming
language that has only bounded loops and no recursion. Then claim,
look, everything halts!

Everything surely halts in that language which conforms to those
restrictions, but not in a model of computation that doesn't have those
restrictions.

That's all I'm going to say on the subject, except for this:

If True(X) means Provable(X), and only *only* True(X) means that, then
that means your system has no axioms; how can it exist and do anything
useful?

Formal systems require axioms: the basic propositions that are painted
as true rather than proven, from which other things follow. "Provable"
is synonymous with "derivable from axioms". How could you have
forgotten these?

Gödel's work informs us, essentially, that the syntax of formal systems is
capable of expressing new axioms.  These are well-formed statements
which do not conflict with any of the existing axioms, yet which we are
not able to derive from those axioms either: they relate to the existing
axioms in the same way that those axioms to each other.  (Just like
Euclid's Fifth Postulate can't be proven from the other four. It either
has to be accepted, rejected (resulting in a weaker form of geometry) or
replaced with different versions (leading to alternative geometries).

Contrary to your past claims, you have not found a devastating mistake
in Gödel's work; nobody has. It stands.

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

#143493

On 4/26/2019 8:13 PM, Kaz Kylheku wrote:
> ["Followup-To:" header set to comp.lang.lisp.]
> On 2019-04-26, peteolcott <Here@Home> wrote:
>> On 4/26/2019 12:48 PM, Kaz Kylheku wrote:
>>> ["Followup-To:" header set to comp.lang.lisp.]
>>> On 2019-04-26, peteolcott <Here@Home> wrote:
>>>> The only way to know for sure is to find at least one valid
>>>> counter-example to my assertion.
>>>
>>> Warning: numerous past debates with Peter Olcott have convinced me that
>>> he doesn't know what a counter-example is, and such.
>>>
>>
>> I have come a very long way since the last time that we talked four
>> years ago.
> 
> If you aren't doing this in some kind of Lisp, though, it's off topic in
> comp.lang.lisp.
> 
>> Converting formal proofs of symbolic logic to conform to the sound
>> deductive inference model:
>>
>> Then True(X) means Provable(X) and False(X) mean Provable(¬X) Leaving
>> everything else as Unsound(X).
> 
> If all truths are provable, and anything not provable is false, then the
> system has been weakened; it is incomplete.
> 
That is nothing like what I just said.

> Gödel's work is not restricted to examining the properties of
> a system which conforms to these constraints; it speaks about a more
> general system in which a truth can be unprovable.
> 

Truth cannot possibly be unprovable in the sound deductive inference model.

Within the sound deductive inference model there is a (connected sequence of
valid deductions from true premises to a true conclusion)  thus unlike the
formal proofs of symbolic logic provability cannot diverge from truth.


> (You can wish that that system didn't exist, but that doesn't make
> it go away.)
> 
> Similarly, in computing, we could restrict ourselves to a programming
> language that has only bounded loops and no recursion. Then claim,
> look, everything halts!
> 
> Everything surely halts in that language which conforms to those
> restrictions, but not in a model of computation that doesn't have those
> restrictions.
> 
> That's all I'm going to say on the subject, except for this:
> 
> If True(X) means Provable(X), and only *only* True(X) means that, then
> that means your system has no axioms; how can it exist and do anything
> useful?
> 
> Formal systems require axioms: the basic propositions that are painted
> as true rather than proven, from which other things follow. "Provable"
> is synonymous with "derivable from axioms". How could you have
> forgotten these?

Formalizing the Sound Deductive Inference Model in Symbolic Logic
Axiom(0) Stipulates** this definition of Axiom:
Expressions of language defined to have the semantic value of Boolean True.
Provides the symbolic logic equivalent of true premises.

Stipulating** this specification of True and False:  (TRUE ↔ ⊤ ∧ FALSE ↔ ⊥)
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
Thus stipulating** that consequences are provable from axioms.

Stipulating** that formal systems are Boolean:
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
Screens out semantically unsound sentences as not belonging to the formal system.

> 
> Gödel's work informs us, essentially, that the syntax of formal systems is
> capable of expressing new axioms.  These are well-formed statements
> which do not conflict with any of the existing axioms, yet which we are
> not able to derive from those axioms either: they relate to the existing
> axioms in the same way that those axioms to each other.  (Just like
> Euclid's Fifth Postulate can't be proven from the other four. It either
> has to be accepted, rejected (resulting in a weaker form of geometry) or
> replaced with different versions (leading to alternative geometries).
> 
> Contrary to your past claims, you have not found a devastating mistake
> in Gödel's work; nobody has. It stands.
> 



-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#143497

On 2019-04-27, peteolcott <Here@Home> wrote:
> Truth cannot possibly be unprovable in the sound deductive inference model.

Again, only if it that model contains no axioms. Axioms are not
provable; they are declared true as part of the basis of the system.

You're really still not brushed up on even a second year university
level understanding of this stuff.

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

#143500

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.

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

#143503

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]

#143501

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]

#143504

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]

#143505

On 4/27/2019 4:52 PM, Paul Rubin wrote:
> peteolcott <Here@Home> writes:
>> I have spent 22 years and 12,000 hours on this.
> 
> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
> 

IT ELIMINATES INCOMPLETENESS AND INCONSISTENCY OF FORMAL SYSTEMS
NO VALID COUNTER-EXAMPLE EXISTS SHOWING OTHERWISE
I DARE YOU TO FIND ONE

All that I do is translate the formal proofs to theorem consequences of
symbolic logic to conform to the sound deductive inference model.

Axioms are merely expressions of language that have been defined
to have the semantic value of Boolean true.

I made this much simpler for people that do not know symbolic logic:
True(X) is Provable(X) from Axioms.
False(X) is Provable(¬X) from Axioms.
Otherwise Unsound(X).

Here it is in symbolic logic:
Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))
Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))

Eliminating Undecidability and Incompleteness in Formal Systems
https://www.researchgate.net/publication/332427635_Eliminating_Undecidability_and_Incompleteness_in_Formal_Systems

-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#143506

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]

#143507

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]

#143508

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]

#143509

On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:
> On Sat, 27 Apr 2019 17:12:45 -0600
> Jeff Barnett <jbb@notatt.com> 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.
> 
> Dudley has written a whole book on the subject , "A budget of trisections".
> 

The huge difference in this case is that deriving a complete and consistent
formulation of the notion of True finally anchors Truth Conditional Semantics.
https://en.wikipedia.org/wiki/Truth-conditional_semantics



-- 
Copyright 2019 Pete Olcott All rights reserved

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

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

#143510

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]

#143535

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]

Page 1 of 3  [1] 2 3  Next page →

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

csiph-web