Sequents: if-introduction and discharging assumptions

Question

I am reading through "Mathematical Logic by Ian Chiswell & Wilfred Hodges"(amazon, and publisher)

for context I am reading through this for self-study, so I don't have the normal support of a classroom environment - and the lack of exercise solutions makes it hard to check my understanding.

On page 21 there is Exercise 2.4.4.f which asks "write out a derivation to prove the following sequent"

$\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$

So far we have covered $\rightarrow$-Introduction and discharging in the following form

$$\begin{array}{lr} \phi & \psi\\ \hline & (\phi \rightarrow \psi) \\ \end{array} $$

which will discharge $\phi$ using $\rightarrow$-Introduction

My solution to 2.4.4.f so far is

(f) derivation of sequent $ \{ (\phi \rightarrow (\psi \rightarrow \chi)) \} \vdash ((\phi \wedge \psi) \rightarrow \chi) $

$$ \begin{array}{rrr} \phi & & (\phi \rightarrow (\psi \rightarrow \chi)) \\ \hline \psi & & (\psi \rightarrow \chi) \\ \hline & & \chi \end{array} $$

which now leaves us with the undischarged assumptions $ \{\phi, \psi, (\phi \rightarrow (\psi \rightarrow \chi)) \} $

from this I have $\chi$ so I can then (using $\rightarrow$-introduction)

$$ \begin{array}{r} \chi \\ \hline ((\phi \wedge \psi) \rightarrow \chi) \\ \end{array} $$

I don't have to discharge $(\phi \rightarrow (\psi \rightarrow \chi))$ as it is captured in the LHS of the sequent - but I do have to discharge both $\phi$ and $\psi$

In my $\rightarrow$-introduction above this means I can then discharge $(\phi \wedge \psi)$, but by the rules given so far it doesn't mean I can discharge $\phi$ and $\psi$ even though I know they are logically equivalent - that is if we can assume $(\phi \wedge \psi)$ then it is easy to show this entails both $\phi$ and $\psi$

Is it allowable to use $\rightarrow$-introduction of $(\phi \wedge \psi)$ to then discharge the assumptions of both $\phi$ and $\psi$ ?

If so, what is the generalisation of this ?

If not, how can I correctly form a derivation to prove this sequent?

Answer 1

@MauroALLEGRANZA said: 'You have to start from $(\phi \wedge \psi)$ and then "unpack" it with $\wedge$-elim to get $\phi$ and $\psi$ separately. Then you can go on with the first part of your derivation.'

This answer tries to capture that technique

2.4.4.f is to prove $\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$

$\wedge$-elim to get $\phi$ : $$ \begin{array}{c} (\phi \wedge \psi) \\ \hline \phi \end{array} $$

$\wedge$-elim to get $\psi$ : $$ \begin{array}{c} (\phi \wedge \psi) \\ \hline \psi \end{array} $$

and now the derivation the above 2 derivations allow us to discharge $\phi$ and $\psi$

$$ \begin{array}{rrr} \phi & & (\phi \rightarrow (\psi \rightarrow \chi)) \\ \hline \psi & & (\psi \rightarrow \chi) \\ \hline & & \chi \\ \hline & & ((\phi \wedge \psi) \rightarrow \chi) \\ \end{array} $$

which shows we can derive the sequent $((\phi \wedge \psi) \rightarrow \chi)$ with the undisharged assumptions of $\{ (\phi \rightarrow (\psi \rightarrow \chi))\}$

Thus proving the sequent $\{(\phi \rightarrow (\psi \rightarrow \chi))\} \vdash ((\phi \wedge \psi) \rightarrow \chi)$

Answer 2

It is helpful to indicate what assumptions are being discharged and where; usually by indices and either canceling or boxing off the assumption.   So conditional introduction should be presented similar to: $$\require{cancel}\dfrac{\cancel{~\phi~}^n\quad\psi}{\phi\to\psi}{\small{\to}\mathsf I^n}\qquad\dfrac{[\phi]^n\quad\psi}{\phi\to\psi}{\small{\to}\mathsf I^n}\\~\\\tiny\text{NB: I prefer boxing, as it is cleaner.}$$

Why is this helpful? Well, the assumption may not appear immediately above the line in which it is discharged; and may appear multiple times.  

In this case, you seek to discharge $\phi\land\psi$ so to introduce the conditional; further, the only assumption that should remain undischarged at the end of the proof is the premise $\phi\to(\psi\to\chi)$. So you cannot leave the $\phi$ and $\psi$ naked; they must be covered by the discharged assumption; ie: you must derive them using conjunction elimination.

$$\dfrac{\dfrac{\dfrac{\lower{1.5ex}{\phi\to(\psi\to\chi)}\quad\dfrac{[\phi\land\psi]^1}{\phi}{\small\land\mathsf E}}{\psi\to\chi}{\small{\to}\mathsf E}\quad\dfrac{[\phi\land\psi]^1}{\psi}{\small\land\mathsf E}~}{\chi}{\small{\to}\mathsf E}}{(\phi\land\psi)\to\chi}{\small{\to}\mathsf I^1}$$

---

In Fitch style, this proof would look like$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~~\phi\to(\psi\to\chi)}{\fitch{~~2.~~\phi\land\psi}{~~3.~~\psi\hspace{12ex}{\land}\mathsf E~2\\~~4.~~\phi\hspace{12ex}{\land}\mathsf E~2\\~~5.~~\psi\to\chi\hspace{7ex}{\to}\mathsf E~4,1\\~~6.~~\chi\hspace{12ex}{\to}\mathsf E~3,5}\\~~7.~~(\phi\land\psi)\to\chi\hspace{4ex}{\to}\mathsf I~2{-}6}$$

So the assumption is raised in line 2, used twice (in lines 3 and 4), and discharged for line 7