# Sequents: if-introduction and discharging assumptions

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?

• You have to start from $(ϕ∧ψ)$ and then "unpack" it with $\land$-elim to get $ϕ$ and $ψ$ separately. Then you can go on with the first part of your derivation. – Mauro ALLEGRANZA Jul 18 '16 at 13:33
• @MauroALLEGRANZA ahh that makes sense, I had been using a similar technique elsewhere (using the LHS side of $\rightarrow$), thank you very much. For completeness I have added this as an answer below along with my full derivation. – cjh Jul 18 '16 at 23:36

@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)$