# Formal proofs and Deduction Theorem

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.

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\rightarrowq)\rightarrow(p\rightarrow(r\rightarrowq))), 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$).

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.

• Thanks for answering the second part of the question, it was made clear. But would you know the first part too ? – nerdy May 15 '14 at 11:31
• 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 always possible to represent the formal proof of γ from A as : $\\ A \\ \models \beta1 \\ \models \beta2 \\ ... \\ \models \gamma$ – nerdy May 15 '14 at 11:31
• @nerdy Can you represent the last proof I've put in my answer by that format? Well, it has two axioms used, which consequently need stated for the sequence to qualify as a formal proof. The axioms are independent of each other in that neither axiom can derive the other (under uniform substitution and detachment). So, given a basis with more than one element (axiom) the answer is no. However, for many logical systems there exists a basis consisting of a single element. In other words, the single axiom {A} for the system can derive the axioms in {B, ... Bn}} of another given basis, and 1/2 – Doug Spoonwood May 15 '14 at 13:53
• @nerdy {B, ..., Bn} can derive A (under the same set of inference rules... usually uniform substitution and detachment). For example, the two axiom basis I used above {(p→(q→p)), ((p→(q→r))→((p→q)→(p→r)))} could get replaced by any of the 12, 17-letter single axioms here web.ics.purdue.edu/~dulrich/C-pure-intuitionism-page.htm If we do that, then we could write a proof of "((p→q)→(p→(r→q))))" or equivalently "CCpqCpCrq" in Polish notation, in the format you've suggested... except that we wouldn't use the semantic turnstile indicator |=, we'd use |- or omit it. – Doug Spoonwood May 15 '14 at 13:59
• @nerdy Sure you can start with such a conjunction, and then get to the end point, so long as you have the rules K$\alpha$$\beta \vdash \alpha and K\alpha$$\beta$ $\vdash$ $\beta$ where "K" is in Polish notation, indicating conjunction, and K precedes its arguments "$\alpha$" and "$\beta$". – Doug Spoonwood May 18 '14 at 22:22