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

#9159 — 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]

#9160

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]

#9161

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]

#9164

On 4/26/19 11:48 AM, peteolcott wrote:
> 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.

What you've done is to define the cases that give you trouble out of 
existence. By doing so, you've gotten rid of incompleteness for your 
system, but that says more about your system than about Goedel. (I'd 
argue that you've provided a meta-proof of Goedel, but the margin of 
this point is too small to contain it.)

paul

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

#9214

On 4/26/2019 12:40 PM, paul wallich wrote:
> On 4/26/19 11:48 AM, peteolcott wrote:
>> 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.
> 
> What you've done is to define the cases that give you trouble out of existence. By doing so, you've gotten rid of incompleteness for your system, but that says more about your system than about Goedel. (I'd argue that you've provided a meta-proof of 
> Goedel, but the margin of this point is too small to contain it.)
> 
> paul
> 

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

#9162

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]

#9163

Try this in Prolog:

   p :- p.

The positive query gives:

   ?- p.
   %%% loops infinitely

The negative query gives:

   ?- \+ p.
   %%% loops infinitely

But this behaviour is sound!

Proof:
Logically p :- p says p <- p as Horn Clause,
with Clark Completion it says p <-> p. In either
case it says nothing, both are tautologies, 

always true. The the theories is {p <- p}, {p <-> p}
are {} are all logically equivalent. But we 
have the following for the empty theory:

   {} |/- p

   {} |/- ~p

Neither p nor ~p are derivable from the empty theory,
because the empty theory can have the models M1 = {p=1}
and M2 = {p=0}, so there is no model in favor of p

or in favor ~p, both have a counter model.

Q.E.D.

Am Freitag, 26. April 2019 17:51:01 UTC+2 schrieb peteolcott:
> 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]

#9165

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

#9166

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]

#9167

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

#9171

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]

#9172

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]

#9173

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 

already derived statements. Now take n=1.

Whats wrong with you guys?

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.

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

#9178

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]

#9174

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]

#9175

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]

#9176

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]

#9177

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]

#9179

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]

#9180

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]

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

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

csiph-web