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


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.