In this question i will explain one idea i had about basic formal proofs and the use of Deduction Theorem.
I'm considering a formula γ to be a logical consequence of a set A of formulas if and only if it is true in all models of the set A of formulas ( structures that satisfy the set of A formulas ). Also, I'm considering a formal proof of a formula γ from a set A of formulas, as a finite list of formulas that are either formulas of A, logically valid formulas ( instances of axioms schemmas ) or formulas obtained by applying rules of infernece ( axiom schemmas ) to two or more preeceding formulas on the list.
At the same time, by soundness, to say that we have a formal proof of γ from the set A, would be saying that :
$ A⊨γ $
Now i have a series of questions...
First of, is it it true that for all propositions(theorems,etc) that simply affirm that a formula is a logical consequence of a set of formulas, no matter how hard(long) its ( of proposition ) formal proof is, will it always possibly be represented by a long chain of "logical consequences" ? I heard from a lecturer say that this would be the most "formal" kind of formal proof, a formal proof consisting only of a chain of logical consequences. For example, for any A,γ , is it possible to represent the formal proof of γ from A as :
$ A \\ ⊨β1\\⊨β2\\...\\⊨γ $
If the answer is yes, then i imediately thought that we could use deduction theorem to transform it into the following logically valid formula :
So, i thought that it would mean that actually any formal proof in this more formal state ( only chains of logical consequences) could be seen as possibly translated to a logically valid formula of our formal logic ( first-order, second-order ... ) that has the form of an implication, and that has all information required and used to prove γ from A. Is it true ? Let me give one example :
Extrapolation, ignore if completely wrong
As an analogy i thought of the tuple (4,3,2) in R^n that carries all information needed about the polynomial 4x² + 3x + 2 .
So , analogally, could we view a kind of "informal isomorphism" between the set of all formal proofs in that "supposedly rigorous" state of only chain of logical consequences and logically valid formulas of our formal language in that shape ( chain of implications ) ?
Then it would be possible to translate back and forth between formal proofs on that state, and logically valid implications of our formal language.
Thanks a bunch.