What sequent does this derivation prove?

Question

Trying to learn sequent calculus and so I am trying to work thru some examples to get a better grip/understanding but the following question is not answered at the back of the book. I wrote my guess in the blue writing in the attached picture, however I am unsure of my answer because phi appears in the consequent under the first line. So I am wondering if it should look like my second guess which is written in red. The book I took this from is Mathematical Logic, by Hodges. Hope somebody can explain what is correct and why, please!!!

Answer 1

Neither.

The sequent proved is :

$\vdash (\phi \to (\psi \to \phi))$.

It is the last formula and the only assumption of the derivation : $\phi$, has been discharged (it is crossed with the "dandah").

---

The derivation is correct; see the discussion in :

• Jan von Plato, Elements of Logical Reasoning (2013), page 22,

or see the relevant parts quoted into this post.

The approach followed by Chiswell & Hodeges into this example simply amounts to :

we can discharge any assumptions, also assumptions not "declared" as such in the derivation.

The intuition behind it is quite simple : let's start assuming $\phi$, and derive $\phi$.

Having preformed this obviuos derivation of $\phi$ from some assumptions, it is harmless to assert that we have derived it from "those" assumption plus some extra-one.

Conclusion : we can always add "unnecessary" assumptions in a derivation.

Answer 2

It is meant to prove the sequent $\vdash\phi\rightarrow (\psi\rightarrow\phi)$, but the derivation is not complete. The first $(\rightarrow I)$ needs the assumption $\psi$ (and repeating the assumption $\phi$):

From "Logic in computer science" (Huth & Ryan) page 20:

Also note that your derivation is in Natural Deduction and it's different from Sequent Calculus (since you said you are trying to learn Sequent Calculus)