Prove $\{\phi\} \vdash \psi$ if and only if $\vdash (\phi \rightarrow \psi)$

I'm self-teaching myself some logic, and I was hoping that someone can check my proof of the statement in the title, and give comment on whether this is formatted acceptably.

(This problem comes from the textbook I'm learning from, Mathematical Logic by Chiswell and Hodges, Ex. 2.4.5).

The rules I use, as declared in the textbook, are:

($\rightarrow I$): $\Gamma \cup \{\phi\} \vdash \psi \Rightarrow \Gamma \vdash (\phi \rightarrow \psi)$

($\rightarrow$ E): $(\Gamma \vdash \phi) \wedge (\Delta \vdash (\phi \rightarrow \psi)) \Rightarrow (\Gamma \cup \Delta \vdash \phi)$

(Axiom Rule): $\phi \vdash \phi$

And the proof is:

1. Prove $\{\phi\} \vdash \psi \Leftrightarrow~ \vdash (\phi \rightarrow \psi)$
2. $\{\phi\} \vdash \psi \Rightarrow~ \vdash (\phi \rightarrow \psi)$ (from $\rightarrow$ I).
3. $\vdash (\phi \rightarrow \psi) \Rightarrow \{\phi\} \vdash \psi$ --(From Axiom Rule and $\rightarrow$ E)
4. It is proven because 2. and 3. and definition of $a \Leftrightarrow b \equiv a \Rightarrow b \wedge b \Rightarrow a$

I'm not sure if I should be elaborating further on each step, or if this is how proofs are usually formatted. Any feedback would be welcomed.

• Looks fine to me. Maybe elaborate more on the way you used the rules in steps 2 and 3, but otherwise i find it a valid proof. – Mano Plizzi Sep 15 '16 at 0:59
• @ManoPlizzi thanks! – esotechnica Sep 15 '16 at 3:49
• I don't entirely agree with this proof. The notation is misleading. The $\vdash$ of the theorem and the $\vdash$ of the inferences represent two different things. The former is a statement "there exists a proof of..." and the latter is an inductive step. The actual statement you are trying to prove does require induction on the length of proofs, or something like that. – DanielV Sep 15 '16 at 4:44
• @DanielV I'm not following what you mean. There has been no mention of "induction" anywhere in the text so far. The biggest gripe I have with this text is that none of the answers to these "proof" exercises are provided in the answers section at the back of the book, nor are any examples given. So I'm not sure how to learn how these proofs are written! Are you able to give an example proof? – esotechnica Sep 15 '16 at 10:23
• @DanielV - I do not agree... C&H (page 7) Def 2.1.2 A sequent is an expression $Γ \vdash \psi$ that means "There is a proof whose conclusion is $\psi$ and whose undischarged assumptions are all in the set $Γ$." Thus, $\{ ϕ \} \vdash \psi$ means "there is a derivation $D$...". Then, write down $D$ and add at the end an instance of the rule ($\to$-I) and we get a new derivation $D'$ for $(\phi \to \psi$) with no assumptions left. – Mauro ALLEGRANZA Sep 15 '16 at 10:27