Google Groups no longer supports new Usenet posts or subscriptions. Historical content remains viewable.
Dismiss

Deductively Sound Formal Proofs --- (v2)

0 views
Skip to first unread message

peteolcott

unread,
May 10, 2019, 2:06:04 PM5/10/19
to
Using the sound deductive inference model as the basis of the a
notion of a formal system defines [Deductively Sound Formal Proofs].
Within (DSFP) closed Well-formed formula that were undecidable in
other formal systems are excluded on the basis that they do not
belong to deductively sound inference.

The sound deductive inference model specifies:
[a connected sequence of valid deductions from true premises to a true conclusion]

http://liarparadox.org/Provable_Mendelson.pdf (Mendelson 2015:28)
Making the conventional formal proofs of mathematical logic conform to the
sound deductive inference model only requires one tiny little change this
Γ ⊢ C becomes this True(Γ) ⊢ C. This specifies the sound deductive inference
model subset of all conventional formal proofs (the subset of conventional
formal proofs having every element of their set of premises true).

How hard is it to understand the basic model of Sound_Deduction?
True premises combined with valid inference necessitates true consequences.

When-so-ever ¬((Γ ⊢ C) ∨ (Γ ⊢ ¬C)) we can know (a) or (b) and (c):
(a) Not all of the the premises specified by Γ are true.
(b) There is no sequence B1, …, Bk of wfs from Γ to C.
(c) ∴ ¬Deductively_Sound(Γ, C)

When a man that has never been married is asked:
Have you stopped beating your wife yet?

The lack of a correct answer does not indicate that all of human
reasoning is fundamentally incomplete. When-so-ever a yes or no
question lacks a correct yes or no answer the question itself is
incorrect.

This same reasoning applies euqally to logic sentences: When-so-ever
a logic sentence lacks a correct true or false Boolean value the
logic sentence itself is incorrect.

When the above is applied to every conventional undecidable sentence
of mathematical logic it simply decides that these sentences are
deductively unsound thus semantically erroneous.

Mendelson, Elliott 2015. Introduction to Mathematical Logic (sixth edition).
Boca Raton: Taylor & Francis Group LLC.

Deductively Sound Formal Proofs
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs


--
Copyright 2019 Pete Olcott
All rights reserved

peteolcott

unread,
May 10, 2019, 3:21:06 PM5/10/19
to
Within the conventional notion of formal proof: Γ ⊢ C
http://liarparadox.org/Provable_Mendelson.pdf
¬((Γ ⊢ C) ∨ (Γ ⊢ ¬C)) defines ¬Deductively_Sound(Γ, C)

This excludes every undecidable logic sentence of conventional
formal proofs as deductively unsound thus semantically incorrect.

peteolcott

unread,
May 10, 2019, 3:41:27 PM5/10/19
to
Within the conventional notion of formal proof: Γ ⊢ C
http://liarparadox.org/Provable_Mendelson.pdf
¬((Γ ⊢ C) ∨ (Γ ⊢ ¬C)) defines ¬Deductively_Sound(Γ, C)

This excludes every undecidable logic sentence of the conventional formal
proofs of mathematical logic as deductively unsound thus semantically incorrect.

On 5/10/2019 1:05 PM, peteolcott wrote:
0 new messages