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

[peteolcott]

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

[Siri Cruise]

In article <2_ydnT3SYPULgV7B...@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

[peteolcott]

On 4/26/2019 10:20 AM, Siri Cruise wrote:
> In article <2_ydnT3SYPULgV7B...@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.

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

[Kaz Kylheku]

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

[peteolcott]

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

[Kaz Kylheku]

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

[Keith Thompson]

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) ks...@mib.org <http://www.ghoti.net/~kst>
Will write code for food.
void Void(void) { Void(); } /* The recursive call of the void */

[peteolcott]

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

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

[peteolcott]

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

[peteolcott]

On 4/27/2019 4:56 PM, Ike Naar wrote:

> On 2019-04-27, Kaz Kylheku <847-11...@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

[peteolcott]

On 4/27/2019 1:26 PM, Kaz Kylheku wrote:

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

[peteolcott]

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

[peteolcott]

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

[peteolcott]

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

[peteolcott]

On 4/27/2019 7:10 PM, Paul Rubin wrote:

> Jeff Barnett <j...@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.

[peteolcott]

On 4/27/2019 7:16 PM, Spiros Bousbouras wrote:

> On Sat, 27 Apr 2019 17:12:45 -0600
> Jeff Barnett <j...@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

[peteolcott]

On 4/27/2019 8:52 PM, Paul Rubin wrote:
> Jeff Barnett <j...@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.

[peteolcott]

On 4/29/2019 4:53 PM, paul wallich wrote:

> On 4/27/19 7:12 PM, Jeff Barnett wrote:
>> Paul Rubin wrote on 4/27/2019 3:52 PM:
>>> peteolcott <Here@Home> writes:
>>>> I have spent 22 years and 12,000 hours on this.
>>>
>>> http://web.mst.edu/%7Elmhall/WhatToDoWhenTrisectorComes.pdf
>>
>> Thanks for the pointer. It seems I missed that article - it came in a crack between regularly reading the Intelligencer in the USC/ISI library where I was employed and starting my own subscription which I kept for two decades. The Intelligencer went from
>> wildly entertaining to hard to read during the latter period. The article by Dudley has a wider appeal today than when he wrote it in 1983; we have lots of computer systems to shield cranks and save then postage.
>>

>> PO fits the article's profile to a tee: he claims to be in his 60's, to have spent thousands of hours, keeps cleaning and pushing the same mistakes over and over again, and is basically a very poor mathematician who believes that PROLOG represents real
>> and deep logic systems. I have been leaning towards troll rather than ignoramus but the article gives me a third choice: trisector! I'll keep it in mind.
>>
>> The thing I find interesting is that most people, including me, find it so hard to not respond to his gibberish. The first reaction is to help a lost soul back onto the path of truth (caps?) while the second reaction is mostly a reaction to a hard
>> challenge like trying to stare down a lizard.
>
> I think that the problem isn't trisection exactly but rather a sort of weird semantic capture. The term "unsound" is used to tag the category "neither provable nor refutable" but that's -- within the system -- just a tag. The logical system, such as it is,
> would work just as well if the tag were "NPNR" or "frabjous" or "charmed" or "boogabooga". But use the tag "unsound", and magically all of the senses of "unsound" from colloguial language and other logical systems suddenly get dragged in and pasted over
> the top of what might as well be "frabjous".
>
> Do some brains need better macro systems?

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

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

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

[peteolcott]

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.

[peteolcott]

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.

[peteolcott]

On 4/30/2019 11:23 AM, tar...@google.com wrote:
> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>
>> Based on these three axioms Gödel's Incompleteness is refuted:

>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))

>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
>

> Not sure why these are axioms. It would seem that these are properties of
> your formal system, which if satisfied would admit it into your system. I don't
> see how asserting that all formal systems obey these axioms work. For arbitrary
> formal systems, it is clear that these axioms do not hold.

>
>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>> There is no sentence G of Formal System F that is neither True nor False in F.
>

> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
> statement.
>
> Instead, the claim that you have is that if you create a suitably constrained
> formal system, then in *that* system you can have complete inference. This is
> well-recognized result. The interesting question is whether the constraints
> needed to achieve this complete inference will leave you with enough expressive
> power to be able to perform interesting inference in your system.
>
> Certainly one of Gödel's results is that if you have a formal system that is
> expressive enough to include arithmetic, you run into incompleteness.

Only because the mathematical system that he used to form this proof was too
weak to discern semantic ill formedness:

In the same way that not all finite strings are well-formed formula
(when semantic criteria is applied) not all closed WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the
semantic property of Boolean true then the theorem consequences
of formal proofs form:
[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.


>A
> consequence of that is that your system, therefore, cannot use arithmetic. As
> long as you don't need arithmetic for the inferences of interest, then you may
> find your formal system adequate.
>
> For an interesting discussion of some issue having to do with decidability and
> efficiency of reasoning, you may want to look at the Description Logic
> research. There are a number of variants of description logic with different
> expressive power and consequently different decisions regarding what can be
> computed, ranging from tractable complete inference to undecidability.
>
> Overview: https://en.wikipedia.org/wiki/Description_logic
> Complexity: http://www.cs.man.ac.uk/~ezolin/dl/

[peteolcott]

On 4/30/2019 11:47 AM, Pascal J. Bourguignon wrote:

> tar...@google.com writes:
>
>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>
>>> Based on these three axioms Gödel's Incompleteness is refuted:

>>> Axiom(1) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F, x) ↔ (F ⊢ x))
>>> Axiom(2) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (False(F, x) ↔ (F ⊢ ¬x))

>>> Axiom(3) ∀F ∈ Formal_System ∀x ∈ Closed_WFF(F) (True(F,x) ∨ False(F,x))
>>

>> Not sure why these are axioms. It would seem that these are properties of
>> your formal system, which if satisfied would admit it into your system. I don't
>> see how asserting that all formal systems obey these axioms work. For arbitrary
>> formal systems, it is clear that these axioms do not hold.
>>

>>> ∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))
>>> There is no sentence G of Formal System F that is neither True nor False in F.
>>

>> I would suggest that claiming Gödel's Incompleteness is refuted is too strong a
>> statement.
>>
>> Instead, the claim that you have is that if you create a suitably constrained
>> formal system, then in *that* system you can have complete inference. This is
>> well-recognized result. The interesting question is whether the constraints
>> needed to achieve this complete inference will leave you with enough expressive
>> power to be able to perform interesting inference in your system.
>>
>> Certainly one of Gödel's results is that if you have a formal system that is

>> expressive enough to include arithmetic, you run into incompleteness. A

>> consequence of that is that your system, therefore, cannot use arithmetic. As
>> long as you don't need arithmetic for the inferences of interest, then you may
>> find your formal system adequate.
>

> And note that arithmetic is a consequence of Turing Completeness. So if
> your formals sytem is any useful to a programmer (ie. is Turing
> Equivalent), then it will have arithmetic, and therefore it will be
> inconsistent or incomplete, choose of of two.
>
> (Ie. correct programs will produce wrong results, or there will be
> programs that you won't be able to prove if it is correct or incorrect).
>

My system can express anything including arithmetic, it simply does not
do so erroneously:

In the same way that not all finite strings are well-formed
formula (when semantic criteria is applied) not all closed
WFF are logic sentences.

Any expression of language that is neither true nor false is
not a logic sentence of any formal system that has been
adapted to conform to the sound deductive inference model.

Logic sentences are always derived from sound deduction. In
the sound deductive inference model this means that there is:
[a connected sequence of valid deductions from true premises to a true conclusion].

When axioms are construed as expressions of language having the semantic

property of Boolean true (thus anchoring formal proofs in the semantics of
Boolean values) then the theorem consequences of formal proofs form:

[a connected sequence of inference from axioms to a true consequence].

In neither case is undecidability, incompleteness or inconsistency possible.

[peteolcott]

On 5/1/2019 5:21 AM, bert wrote:
> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott wrote:
>> On 4/30/2019 1:06 PM, bert wrote:

>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott wrote:
>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:

>>> etcetera
>>>
>>> One of the hallmarks of a crank is being the
>>> author of nearly all of the posts in a thread.
>>
>> What if I am a crank and I am correct?
>
> Then other distribution and publicity routes
> would be more appropriate for your theories.
>

I have to first get someone to consider the possibility that I am correct
so that they can test my actual reasoning and thus prove that I am correct.
Because my result is unbelievable I am simply dismissed out-of-hand.

In sound deductive inference there is:

[a connected sequence of valid deductions from true premises to a true conclusion].

If we simply construe Axioms as expressions of language having
the semantic property of Boolean true this would anchor the syntax
of formal proofs to the semantics of Boolean values.

Now we have: [Deductively Sound Formal Proofs] True(x) ↔ (⊢x)

[a connected sequence of inference from axioms to a true consequence].

AKA the same universal truth predicate that Tarski "proved" was impossible.

he 1936 Tarski Undefinability Proof
http://liarparadox.org/Tarski_Proof_275_276.pdf

[peteolcott]

On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:

> peteolcott <Here@Home> writes:
>
>> On 5/1/2019 5:21 AM, bert wrote:
>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott wrote:
>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott wrote:
>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>> etcetera
>>>>>
>>>>> One of the hallmarks of a crank is being the
>>>>> author of nearly all of the posts in a thread.
>>>>
>>>> What if I am a crank and I am correct?
>>>
>>> Then other distribution and publicity routes
>>> would be more appropriate for your theories.
>>>
>>
>> I have to first get someone to consider the possibility that I am correct
>> so that they can test my actual reasoning and thus prove that I am correct.
>> Because my result is unbelievable I am simply dismissed out-of-hand.
>

> Or you could show us a non-trivial formal system that is both consistent
> and complete.
>

I just did and you trimmed it from your reply.
Go back to my message and analyze the part that you trimmed point-by-point.

[Bonita Montero]

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

[Keith Thompson]

peteolcott <Here@Home> writes:
[...]

One last try.

Pete, as far as I can tell you have written nothing relevant to
C, C++, or Lisp. Please stop posting in comp.lang.{c,c++,lisp}.
(I would have emailed you if you had provided a valid email address.)

I do not intend to post again in this thread.

[Bonita Montero]

Am 01.05.2019 um 19:48 schrieb Keith Thompson:
> peteolcott <Here@Home> writes:
> [...]
>
> One last try.
>
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp. Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
> I do not intend to post again in this thread.

Look at this thread - he seems to be manic.
Arguing is a waste of time here.

[peteolcott]

On 5/1/2019 11:37 AM, Pascal J. Bourguignon wrote:
> peteolcott <Here@Home> writes:
>
>> On 5/1/2019 7:53 AM, Pascal J. Bourguignon wrote:
>>> peteolcott <Here@Home> writes:
>>>
>>>> On 5/1/2019 5:21 AM, bert wrote:
>>>>> On Wednesday, 1 May 2019 06:51:26 UTC+1, peteolcott wrote:
>>>>>> On 4/30/2019 1:06 PM, bert wrote:
>>>>>>> On Tuesday, 30 April 2019 18:02:32 UTC+1, peteolcott wrote:
>>>>>>>>>> On Monday, April 29, 2019 at 10:41:40 PM UTC-7, peteolcott wrote:
>>>>>>> etcetera
>>>>>>>
>>>>>>> One of the hallmarks of a crank is being the
>>>>>>> author of nearly all of the posts in a thread.
>>>>>>
>>>>>> What if I am a crank and I am correct?
>>>>>
>>>>> Then other distribution and publicity routes
>>>>> would be more appropriate for your theories.
>>>>>
>>>>
>>>> I have to first get someone to consider the possibility that I am correct
>>>> so that they can test my actual reasoning and thus prove that I am correct.
>>>> Because my result is unbelievable I am simply dismissed out-of-hand.
>>>
>>> Or you could show us a non-trivial formal system that is both consistent
>>> and complete.
>>>
>>
>> I just did and you trimmed it from your reply.
>> Go back to my message and analyze the part that you trimmed point-by-point.
>

> Well, if I trimmed it, it was trivial…
> Could I have missed arithmetic?
>

That is exactly what I mean by dismissed out-of-hand

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)
is the universal truth predicate that Tarski "proved" was impossible.

[peteolcott]

On 5/1/2019 12:48 PM, Keith Thompson wrote:
> peteolcott <Here@Home> writes:
> [...]
>
> One last try.
>
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp. Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
>
> I do not intend to post again in this thread.
>

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

If Axioms are defined as expressions of language having the
semantic property of Boolean true then this: True(x) ↔ (⊢x)

is the universal truth predicate that Tarski "proved" was impossible.

[peteolcott]

I check each group individually. If respondent were to trim
the other group form their response I would have beet feedback
regrading which groups are relevant.

Although I am not manic I am very excited that I completed
my 22 year 12,000 hour research project with a formalization
of the the notion of True, thus refuting Tarski:

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.

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

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

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

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

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

The only reason that this is possible is a key undiscovered detail that
no one noticed for 81 years.

[peteolcott]

On 4/27/2019 1:26 PM, Kaz Kylheku wrote:

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

[peteolcott]

On 5/1/2019 12:48 PM, Keith Thompson wrote:

> peteolcott <Here@Home> writes:
> [...]
>
> One last try.
>
> Pete, as far as I can tell you have written nothing relevant to
> C, C++, or Lisp. Please stop posting in comp.lang.{c,c++,lisp}.
> (I would have emailed you if you had provided a valid email address.)
>
> I do not intend to post again in this thread.
>

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

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

Every detail of the encoding of virtual machines implementing the Peter

Linz H deciding halting for the Peter Linz input pair: (Ĥ, Ĥ) is complete.

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

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

The only reason that this is possible is a key undiscovered detail that

no one noticed for 81 more than eight decades.

[David Brown]

On 01/05/2019 21:01, peteolcott wrote:
> On 5/1/2019 12:48 PM, Keith Thompson wrote:
>> peteolcott <Here@Home> writes:
>> [...]
>>
>> One last try.
>>
>> Pete, as far as I can tell you have written nothing relevant to
>> C, C++, or Lisp.  Please stop posting in comp.lang.{c,c++,lisp}.
>> (I would have emailed you if you had provided a valid email address.)
>>
>> I do not intend to post again in this thread.
>>
>
> You have been proven to be incorrect in that people continue to
> respond. It is most relevant to Prolog, it is next most relevant
> to Lisp because Lisp is an AI language. I might drop C++, and C
> off the list of cross-posts.
>

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

[peteolcott]

I used to talk about this on comp.theory and then comp.theory died:

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

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

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

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

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

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

[Öö Tiib]

On Wednesday, 1 May 2019 18:56:40 UTC+3, Bonita Montero wrote:
> Is this a second "Amine Moulay Ramdane"?
> According to his manic posting-frequency he might be.

No, each kook deviates from average people in unique manner.
Their background and reasons of going crazy in that background
are rather different. :)

[David Brown]

Why am I not surprised? Posters like you kill groups.

If you ever get as far as working on a C++ implementation and want to
discuss coding details, come back here. Until then, please stay out of
irrelevant groups.

[leigh.v....@googlemail.com]

Says the guy who doesn't mind religious spam being posted to this group.

/Leigh

[guinne...@gmail.com]

On Wednesday, 1 May 2019 22:44:22 UTC+1, peteolcott wrote:
>
> I used to talk about this on comp.theory and then comp.theory died:

There's a serious hole in your logic system if it failed to infer the latter from the former.

[David Brown]

I am sorry, but I think you have got people mixed up. I have never
approved of spam - religious or otherwise. Nor do I like continuous
junk posts (which are not spam - there is a difference) - that includes
certain pointlessly repetitive religious posts, and it includes your own
pointlessly repetitive posts.

There is a difference between an /occasional/ off-topic discussion,
which may be of interest to some people who happen to be in the group,
and the kind of pantomime nonsense perpetrated by you and Rick. Yes,
you are equally guilty.

[peteolcott]

I only come here because the more relevant groups died.

[Öö Tiib]

Perhaps you haven't put it clearly forward that you dislike Leigh's ways
of "fighting" with religious spam even more than religious spam that
you also dislike?

[Öö Tiib]

The groups die because of people who act like you. They post
lot of posts and are impossible to discuss with. Then everybody
will decide that they don't want to be in such sad places where
such mentally ill behavior prevails.

Go look at comp.programming and comp.programming.threads.
These have became personal, insane blogs of "Amine Moulay
Ramdane". He also dislikes that the groups are dead so he
occasionally posts his crap to alive groups in comp.lang or
alt.comp.lang or comp.arch. If he gets any responses from
there then only insults. People are allergic to disrespectful
behavior of madmen.

[Mr Flibble]

You need to have a serious word with yourself, m8.

/Flibble

--
“You won’t burn in hell. But be nice anyway.” – Ricky Gervais

“I see Atheists are fighting and killing each other again, over who
doesn’t believe in any God the most. Oh, no..wait.. that never happens.” –
Ricky Gervais

"Suppose it's all true, and you walk up to the pearly gates, and are
confronted by God," Bryne asked on his show The Meaning of Life. "What
will Stephen Fry say to him, her, or it?"
"I'd say, bone cancer in children? What's that about?" Fry replied.
"How dare you? How dare you create a world to which there is such misery
that is not our fault. It's not right, it's utterly, utterly evil."
"Why should I respect a capricious, mean-minded, stupid God who creates a
world that is so full of injustice and pain. That's what I would say."

[peteolcott]

My system of reasoning has finally been vetted.

Now we have: [Deductively Sound Formal Proofs] -- True(x) ↔ (⊢x)
True Premises Necessarily derive a True Consequence: ◻(True(P) ⊢ True(C))
This refutes Tarski and Gödel.

[peteolcott]

Now we have: [Deductively Sound Formal Proofs] -- True(x) ↔ (⊢x)
True Premises Necessarily derive a True Consequence: ◻(True(P) ⊢ True(C))

Within [Deductively Sound Formal Proofs] expressions of
language that are not decided to be True are decided to be ¬True,
thus undecidable sentences cannot be expressed.

[peteolcott]

Now we have: [Deductively Sound Formal Proofs] -- True(x) ↔ (⊢x)
True Premises Necessarily derive a True Consequence: ◻(True(P) ⊢ True(C))

Within [Deductively Sound Formal Proofs] expressions of language
that are not decided to be True are decided to be ¬True, thus
undecidable sentences cannot be expressed.

[peteolcott]

I am correct and here is the proof:

Now we have: [Deductively Sound Formal Proofs] -- True(x) ↔ (⊢x)
True Premises Necessarily derive a True Consequence: ◻(True(P) ⊢ True(C))

Within [Deductively Sound Formal Proofs] expressions of language
that are not decided to be True are decided to be ¬True, thus
undecidable sentences cannot be expressed.

> They post
> lot of posts and are impossible to discuss with. Then everybody
> will decide that they don't want to be in such sad places where
> such mentally ill behavior prevails.
>
> Go look at comp.programming and comp.programming.threads.
> These have became personal, insane blogs of "Amine Moulay
> Ramdane". He also dislikes that the groups are dead so he
> occasionally posts his crap to alive groups in comp.lang or
> alt.comp.lang or comp.arch. If he gets any responses from
> there then only insults. People are allergic to disrespectful
> behavior of madmen.
>

[peteolcott]

Now we have: [Deductively Sound Formal Proofs] -- True(x) ↔ (⊢x)
True Premises Necessarily derive a True Consequence: ◻(True(P) ⊢ True(C))

Within [Deductively Sound Formal Proofs] expressions of language
that are not decided to be True are decided to be ¬True, thus
undecidable sentences cannot be expressed.

[Manfred]

I see a reason for that (even if I tend to keep out of this stuff at
least it is a reason for me): however annoyingly off-topic Rick's posts
may be, I have seen enough of Flibble's replies be straight rude and
insulting to dislike them even more.

Both of them represent one kind of attitude that justifies restricting
internet freedom.
And freedom (of speech) is a precious value, it shouldn't be wasted this
way.

[Mr Flibble]

That's nice, dear. Now run along to your padded cell and play with your legos.

[Richard Damon]

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.

[peteolcott]

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