# Converting Formal Proofs to Sound Deduction

Formal proofs to theorem consequences of symbolic logic are converted to the sound deductive logic inference model

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

When we consider sound deductive inference to the negation of a conclusion we now also have a definitive specification of falsity.

Within the sound deductive inference model we can be certain that valid inference from true premises derives a true conclusion.

∴ Within the sound deductive inference model any logic sentence that does not evaluate to True or False is unsound, there is no undecidability or incompleteness in this model.

The key criterion measure that the sound deductive inference model would add to the formal proofs to theorem consequences of symbolic logic would be the semantic notion of soundness.

Formalizing Sound Deductive Inference in Symbolic Logic

Axiom(0) Stipulates this definition of Axiom
An Axiom is any 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))

Axiom(0) provides the symbolic logic equivalent of true premises.
Axiom(1) and Axiom(2) stipulate consequences are provable from axioms.
Axiom(3) screens out unsound (semantically malformed) sentences as not belonging to the formal system.