[Math] Formal proofs and Deduction Theorem

logicproof-theory

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 :

$A→(β1→(β2→(….→γ)))$

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 :

http://postimg.org/image/fcg318fsn/

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.

Best Answer

The deduction theorem says if {$\gamma$, $\alpha$} $\vdash$ $\beta$, then $\gamma$ $\vdash$ ($\alpha$$\rightarrow$$\beta$). Now you can represent a proof of $\gamma$ from $\alpha$ by a sequence

$\alpha$

$\vdash$ $\beta$1

$\vdash$ $\beta$2

.

.

.

$\vdash$ $\gamma$.

Consequently by the deduction theorem we can obtain ($\alpha$$\rightarrow$$\alpha$), ($\alpha$$\rightarrow$$\beta1$), ..., ($\alpha$$\rightarrow$$\gamma$). I repeat for emphasis that we have ($\alpha$$\rightarrow$$\gamma$) by having the deduction theorem. Now there exists a theorem which says:

((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$(r$\rightarrow$q))).

Thus to obtain ($\alpha$$\rightarrow$($\beta$$\rightarrow$$\gamma$)) we substitute p with $\alpha$, q with $\gamma$, and r with $\beta$ in ((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$(r$\rightarrow$q))), and from ($\alpha$$\rightarrow$$\gamma$) we detach ($\alpha$$\rightarrow$($\beta$$\rightarrow$$\gamma$)).

We iterate this process, substituting p with $\alpha$, q with ($\beta$$\rightarrow$$\gamma$), and r with $\delta$, and then we can detach ($\alpha$$\rightarrow$($\delta$$\rightarrow$($\beta$$\rightarrow$$\gamma$))).

The catch here comes as that we should obtain ($\alpha$$\rightarrow$($\beta$$_n$$\rightarrow$$\gamma$)) first, then ($\alpha$$\rightarrow$($\beta$$_m$$\rightarrow$($\beta$$_n$$\rightarrow$$\gamma$)) next [where "m"=(n-1)], until we finally obtain ($\alpha$→(β1→(β2→(....→γ)))).

Now let's suppose that we have ($\alpha$→(β1→(β2→(....→γ)))), and $\alpha$. By detachment we can obtain (β1→(β2→(....→γ))). Thus, if we have ($\alpha$$\rightarrow$$\beta$1) also, we can obtain $\beta$1 and thus (β2→(....→γ)). Eventually we can obtain ($\alpha$$\rightarrow$$\gamma$).

So, the answer to your question, I think, is "yes".

But, notice that the deduction theorem itself doesn't directly give us such a transformation as your original post suggests. We used

((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$(r$\rightarrow$q))) for this to work.

That said, if we have the deduction theorem, then ((p$\rightarrow$q)$\rightarrow$(p$\rightarrow$(r$\rightarrow$q))) will follow, as we can see from the following:

hypothesis          1 | (p→q)
hypothesis          2 || p
hypothesis          3 ||| r
detachment 1, 2     4 ||| q
conditional-in 3-4  5 || (r→q)
conditional-in 2-5  6 | (p→(r→q))
conditional-in 1-6  7 ((p→q)→(p→(r→q)))

If we have {(p→(q→p)), ((p→(q→r))→((p→q)→(p→r)))} as the basis used for proving the deduction theorem (other bases exist) we could also prove ((p→q)→(p→(r→q))) as follows:

axiom               1 (p→(q→p))
axiom               2 ((p→(q→r))→((p→q)→(p→r)))
1 p/q, q/r          3 (q→(r→q))
1 p/(q→(r→q)), q/p  4 ((q→(r→q))→(p→(q→(r→q))))
detachment 4, 3     5 (p→(q→(r→q)))
2 r/(r→q)           6 ((p→(q→(r→q)))→((p→q)→(p→(r→q))))
detachment 6, 5     7 ((p→q)→(p→(r→q))))

If we ignore the substitutions here, it looks like in this case that an axiomatic proof can work out as shorter than a natural deduction derivation.

Related Question