I am finally being understood to be correct

[peteolcott]

The following portion of what I have been saying is now finally clear
enough to be understood to be correct.

[Deductively sound formal proofs of mathematical logic]

Could the intersection of [formal proofs of mathematical logic]
and [sound deductive inference] specify formal systems having
[deductively sound formal proofs of mathematical logic]?

All that we have to do to provide [deductively sound formal proofs
of mathematical logic] is select the subset of conventional
[formal proofs of mathematical logic] having true premises and
now we have [deductively sound formal proofs of mathematical logic].

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.

In other words in sound deduction there is a:
[connected sequence of valid deductions from true premises to a true conclusion]

College textbook explains exactly what is meant by [formal proofs of mathematical logic]
http://liarparadox.org/Provable_Mendelson.pdf

It is best that you totally understand the Mendelson definition of
formal proofs before proceeding. Once you totally understand the concept
of formal proofs of mathematical logic and the concept sound deductive
inference we can proceed.

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.

To convert a valid deductive argument into a sound deductive argument
only requires that all the premises are true. We only have to find
some way to select the subset of conventional formal proofs having
entirely true premises.

Deductively sound formal proofs of mathematical logic
https://www.researchgate.net/publication/332864362_Deductively_Sound_Formal_Proofs

--
Copyright 2019 Pete Olcott
All rights reserved