My purpose is to formalize this simple English:
A connected set of known truths necessarily always derives truth.
My basis for doing this is the sound deductive inference model with:
[a connected sequence of valid deductions from true premises to a true conclusion]
This equivalent end result is achieved in symbolic logic:
[a connected sequence of valid inference from axioms to a true consequence]
By construing Axioms as expressions of language having the semantic property of Boolean true.
This last part embeds the semantic notion of Boolean values directly in the syntax of formal expressions. Rudolf Carnap proposed this same idea in his (1952) Meaning Postulates.
Now we have: [Deductively Sound Formal Proofs] — True(x) ↔ (⊢x)
Defining a specification of the notion of formal systems having a universal truth predicate without undecidability, incompleteness or inconsistency.
When one begins with truth and applies valid inference then one necessarily derives truth: (True(P) ⊢ True(C)).
Both Tarski and Gödel “prove” provability can diverge from Truth.
When we boil their claim down to its simplest possible essence it is really claiming that valid inference from true premises might not always derive a true conclusion. This is obviously impossible.