Deductively sound formal proofs of mathematical logic


When true is defined as deductively sound conclusions:
(1) True is ALWAYS defined (thus not undefinable).


(2) Everything ELSE is defined as untrue

(eliminating undecidability and incompleteness).

Here is how that is formalized:
When we specify that True(x) is the consequences of the subset of the of conventional formal proofs of mathematical logic having true premises then True(x) is always defined and never undefinable.

The above specifies formal systems that are complete, consistent and True(x) is always defined. We consider axioms to be specified by a finite list of finite strings combined with a finite list of axiom schemata. Rules-of-inference are specified by another finite list.

The above specs make my whole point!

Understanding this post requires total familiarity with formal proofs of mathematical logic as explained in the following two pages of Mendelson:

http://liarparadox.org/Provable_Mendelson.pdf 
Introduction to Mathematical logic Sixth edition Elliott Mendelson (2015) 

Could the ideas of formal proofs of mathematical logic and sound deductive inference be combined to derive deductively sound formal proofs of mathematical logic specifying formal systems that are both consistent and complete?

If the notion of True(x) is defined as provable from axioms and axioms are stipulated to be finite strings having the semantic property of Boolean true then every expression of language that not a theorem or an axiom is not true.

Because valid deduction from true premises necessarily derives a true consequence we know that the following predicate pair consistently decides every deductively sound argument. So we only need to exclude deductively unsound arguments to define a complete and consistent formal system.

// LHS := RHS the LHS is defined as an alias for the RHS
∀x True(x) := ⊢x
∀x False(x) := ⊢¬x

This additional axiom schema requires that all logic sentences be either true or false: ∀x Deductively_Sound_Consequence(x) := True(x) ∨ False(x)

Every closed WFF not the consequence of a deductively sound argument is construed to be semantically incorrect and excluded from membership in the set of logic sentences. Formalized paradoxes and many undecidable decision problems fall into this category.

Now we apply deductively sound formal proofs of mathematical logic to the 1931 Incompleteness Theorem

https://plato.stanford.edu/entries/goedel-incompleteness
The first incompleteness theorem states that in any consistent formal
system F within which a certain amount of arithmetic can be carried
out, there are statements of the language of F which can neither be
proved nor disproved in F. (Raatikainen 2018)

When we formalize the essence of above we get this logic sentence:
∃F ∈ Formal_System ∃G ∈ Closed_WFF(F) (G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)))

We are assuming consistency without specifying it and we don’t limit the scope to arithmetic. If the above sentence is false then Gödel is wrong.

Within the sound deductive inference model the G of this expression:
((F ⊬ G) ∧ (F ⊬ ¬G)) is a closed WFF that is neither true or false, thus excluding it from membership in the set of logic sentences.

Within the sound deductive inference model the RHS portion of this
expression: G ↔ ((F ⊬ G) ∧ (F ⊬ ¬G)) cannot be evaluated for
material equivalence with G because it is not a logic sentence.

∴ There is no G that is materially equivalent to its own unprovability and its own irrefutability because this would require it to be materially equivalent to neither True or False.