A question concerning discharging assumptions

606 Views Asked by At

In page 19 of Mathematical Logic by Chiswell and Hodges, they provided a derivation of the sequent $\vdash (\phi\to(\phi\to\phi))$:

enter image description here

where $(\to I)$ is:

enter image description here

I understand that if we discharge $\phi$ in 1 this will work since, as $\phi$ has already been discharged, we discharge it again in 2. I don't understand the case where ? is 2, i.e, we discharge $\phi$ at that step. Since we're leaving $\phi$ undischarged until 2, how can we use $(\to I)$ in 1 without discharging $\phi$?

Thank you in advance!

1

There are 1 best solutions below

1
On BEST ANSWER

By Sequent Rule (Axiom Rule), for $\Gamma = \{\}$, we have the sequent $\Gamma \cup \{\phi\} \vdash \phi$, so by Sequent Rule ($\rightarrow \textrm{I}$), we have $\{\} \vdash (\phi \rightarrow \phi)$. That is, we get the tautology $\phi \rightarrow \phi$ "for free" ($\phi$ having been introduced by assumption on the previous line).

Recall the text (p. 17, immediately following the definition of Sequent Rule ($\rightarrow \textrm{I}$)) "the assumption $\phi$ in the first sequent of the sequent rule ($\rightarrow \textrm{I}$) is allowed to drop out of the assumptions of the second sequent". Note "allowed" $\neq$ "required". This is discussed further in Remark 2.4.2.

Recall also the text (p. 17, prior to the definition of Natural Deduction Rule ($\rightarrow \textrm{I}$) "in forming the derivation we are allowed to discharge any occurrence of the assumptions $\phi$ written in $D$. The rule is still correctly applied if we do not discharge all of them; in fact the rule is correctly applied ... [if] there is nothing to discharge." This indicates (1) an assumption may appear more than once in a derivation, (2) applying the rule allows you to discharge all, any, or none of them, and (3) the rule may be applied even when all assumptions are discharged.

This third case is somewhat similar to the first paragraph above. If $\psi$ is something we can deduce and $\phi$ is any statement whatever, we can deduce $\phi \rightarrow \psi$ (because $\psi$ is already known to be true).