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?

  • 2
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Jul 18 '16 at 13:33
  • $\begingroup$ @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. $\endgroup$ – 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)$


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.