Deductively sound formal proofs (v7)

[peteolcott]

Mendelson, Elliott 2015. Introduction to Mathematical Logic (sixth edition) page 27-28
http://liarparadox.org/Provable_Mendelson.pdf

To explain the notion of [sound deduction] using the terms of the art and
symbols of [formal proofs] requires totally understanding this one aspect
of [formal proofs]: Γ ⊢ C means that "C is a consequence of premises Γ"

"Γ" ----- Specifies the premises of a formal proof.
"C" ----- Specifies the consequence of a formal proofs.
"⊢" ----- Specifies valid deduction from premises to consequence of formal proofs.
"Γ ⊢ C" Specifies that C is provable from Γ, in other words "Γ ⊢ C" a valid deductive argument.

Validity and Soundness
https://www.iep.utm.edu/val-snd/

To convert a valid deductive argument into a sound deductive
argument only requires that all the premises are true:
True(Γ) Specifies the premises of the formal proof are true.

Thus defining:
[deductively sound formal proofs of mathematical logic]: True(Γ) ∧ (Γ ⊢ C)

--
Copyright 2019 Pete Olcott
All rights reserved