I'm currently working through the Chiswell and Hodges Mathematical Logic and found myself a little puzzled by a particular natural deduction issue for ($\to$I). The exercise I'm a little stuck on wants me to write out the sequent that is proved by the derivation:
So it certainly seems to me true that $\vdash (\phi \to (\psi \to \phi))$, but I'm having a hard time convincing myself that this is what the derivation above is proving. The natural deduction rule for conditional introduction presented in the book is:
This rule allows you to discharge an assumption $\phi$ after a derivation to $\psi$ and conclude $(\phi\to\psi)$, but I'm not seeing how the rule can allow you to reach a statement where the assumption is in the consequent. It feels like there ought to be a $\psi$ lurking around somewhere in order to make this work according to the rule.
So here's my question: is the key here that ($\to$I) allows you to discharge the assumption of the antecedent when you write down the conditional but doesn't require it? So if I treat the appearance of $\phi$ as like the $\psi$ in the rule pictured, the rule tells me: 'if you had a $\psi$ above you could discharge it in order to write down the conditional, but it's not necessary'?
Does this mean, for instance, that before the second step in the derivation pictured is taken, we would have something like this:
which would be a derivation that shows that $\phi \vdash (\psi\to\phi)$?
If any of the above rambling makes sense, then I think it follows that the derivation does indeed prove that $\vdash (\phi \to (\psi \to \phi))$. Apologies for any lack of clarity -- I'm accustomed to other natural deduction systems and am encountering this one for the first time.
You're right ... something is fishy here.
Now, first of all, the statement $\psi \to \phi$ is a logical consequence of $\phi$ ... and so it would be perfectly ok to define an inference rule of the form:
\begin{array}{cc} \phi\\ \hline \psi \to \phi & \to I\\ \end{array}
... which is of course your Test Derivation.
BUT ... this does not seem to be how this book defines the $\to \ I$ rule! Unless I am missing something, they define it as you indicate: you have to have the antecedent at the top, and then you discharge it with this rule.
Exactly! Like you, I don't see how the first Derivation is compatible with the rules as defined in their book.
I think a proper derivation would be:
\begin{array}{cc} \require{cancel} \cancel{\psi}_1 \quad \cancel{\phi}_2\\ \hline \psi \to \phi & \to I_1\\ \hline \phi \to (\psi \to \phi) & \to I_2 \end{array}
... although it doesn't seem you can have these side-by-side statements above a $\to I$ application ...
so maybe:
\begin{array}{cc} \require{cancel} \cancel{\phi}_2\\ \require{cancel} \cancel{\psi}_1\\ \hline \psi \to \phi & \to I_1\\ \hline \phi \to (\psi \to \phi) & \to I_2 \end{array}
.. but it seems the $\phi$ should be below the $\psi$ in order to do the first $\to I$?
OK, so maybe:
\begin{array}{cc} \require{cancel} \cancel{\psi}_1\\ \require{cancel} \cancel{\phi}_2\\ \hline \psi \to \phi & \to I_1\\ \hline \phi \to (\psi \to \phi) & \to I_2 \end{array}
I think that one is OK. In the Appendix, they do say that:
\begin{array}{c} \phi \end{array}
is a derivation, and so with their $\to I$ rule, that seems to work. If not, we'd have to somehow first derive $\phi$.
So, if it had a 'Reiteration' rule:
\begin{array}{cc} \require{cancel} \cancel{\psi}_1\\ \hline \require{cancel} \cancel{\phi}_2\\ \hline \phi \quad Reit\\ \hline \psi \to \phi & \to I_1\\ \hline \phi \to (\psi \to \phi) & \to I_2 \end{array}
But the system does not seem to have a Reiteration rule, in which case we'd be forced to do something like:
\begin{array}{cc} \require{cancel} \cancel{\psi}_1 \quad \cancel{\phi}_2\\ \hline \psi \land \phi \quad \land I\\ \hline \phi \quad \land E\\ \hline \psi \to \phi & \to I_1\\ \hline \phi \to (\psi \to \phi) & \to I_2 \end{array}