Deductively Sound Formal Proofs (Eliminates undecidability)

[peteolcott]

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]

---The following is applied to the formal proofs of mathematical logic---

When we augment this definition of Axiom (1) becomes (2)
(1) A proposition regarded as self-evidently true without proof [1]
(2) An expression of language (or WFF) having the semantic value of Boolean true. [2]

Then every formal proof to theorem consequences: (⊢x) transmits the truth value
of the Axioms to these consequences thus making the consequence necessarily true.

This provides: [Deductively Sound Formal Proofs] (DSFP) -- True(x) ↔ (⊢x)
True Premises(P) Necessarily derive a True Consequence(C): ◻(True(P) ⊢ True(C))

Now we have a formal specification of the notion of True that cannot possibly fail.
From this specification we derive formal specification of the notion of False: (⊢¬x).

With True and False formalized we specify a semantic criterion of Well-formedness:
Deductively_Sound_Consequence(x) ↔ (True(x) ∨ False(x))

The above derives three meta-mathematical axiom schemata:
(1) True(x) ↔ (⊢x)
(2) False(x) ↔ (⊢¬x)
(3) Deductively_Sound_Consequence(x) ↔ (True(x) ∨ False(x))
Defining [Deductively Sound Consequences of Formal Proofs].

Deductively_Sound_Consequence(x) excludes consequences that do not belong to
deductively sound inference. This eliminates undecidability in formal systems.

[1] http://mathworld.wolfram.com/Axiom.html

[2] Embedding the semantics of Boolean values directly in the syntax of formal
proofs is a precedent already established by Haskell Curry Foundations of
Mathematical Logic, 1977 and Rudolf Carnap Meaning Postulates, 1952.

https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs

--
Copyright 2019 Pete Olcott All rights reserved

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