Preamble:
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.
I also realised that in my previous two questions I referred to this as 'sequents' and 'sequent calculus', but from my understanding now this is specifically 'natural deduction' - which appears to be a simplified sequent calculus.
Natural deduction rules:
I am on pages 24-26 of Mathematical logic, covering section 2.6 "Arguments using 'not'"
We are giving the intro and elim rules as follows
Natural deduction rule ($\lnot$E)
If
$$\begin{array}{lr} D & D' \\ \phi & (\lnot\phi) \\ \end{array} $$
are derivations of $\phi$ and $(\lnot\phi$) respectively, then
\begin{align} D \quad D' \quad \quad \quad \\ \cfrac{\phi \quad (\lnot\phi)}{\bot} (\lnot E) \end{align}
Is a derivation of $\bot$. Its undischarged assumptions are those of D together with those of D'.
Natural deduction rule ($\lnot$I)
suppose
$$\begin{array}{l} D \\ \bot \\ \end{array} $$
is a derivation of $\bot$, and $\phi$ is a statement. Then the following is a derivation of $(\lnot\phi)$.
\begin{align} \require{cancel} \cancel{\phi} \qquad \quad \\ D \qquad \quad \\ \cfrac{\bot}{ (\lnot\phi) } (\lnot I) \end{align}
Its undischarged assumptions are those of D, except possibly $\phi$.
Problem:
Example 2.7.1 (page 25) shows
\begin{align} \require{cancel} \cfrac{ \cancel{\phi} (2) \qquad \cancel{(\lnot\phi)}(1) }{ (1)\cfrac{ \bot }{ (2)\cfrac{ (\lnot(\lnot\phi)) } { (\phi \rightarrow (\lnot (\lnot \phi))) } (\rightarrow I) } (\lnot I) } (\lnot E) \end{align}
Questions
A) From our deduction rule for $(\lnot I)$ I can see that $(\lnot \phi)$ cancels the assumption $\phi$, so here I think our $(\lnot I)$(1) resulting in $(\lnot(\lnot\phi))$ is therefore cancelling $(\lnot\phi)$, is this correct?
B) the application of $(\lnot I)$ (1) also looks like it is taking two steps, and I cannot see how this matches our natural deduction rule for $(\lnot I)$
It looks like it is being applied twice to get from $\bot$ to $(\lnot(\lnot\phi))$ whereas the natural deduction rule when specified goes from $\bot$ to $(\lnot\phi)$.
Is $(\lnot I)$ being implicitly applied twice here?
It $(\lnot I)$ always applied twice?
If this is the case, then my issue is that if we instead apply it once, we can generate what I consider to be a garbage sequent: $(\lnot\phi) \vdash (\phi \rightarrow (\lnot\phi))$
\begin{align} \require{cancel} \cfrac{ \cancel{\phi} (2) \qquad (\lnot\phi) }{ (1)\cfrac{ \bot }{ (2)\cfrac{ (\lnot\phi) } { (\phi \rightarrow (\lnot \phi)) } (\rightarrow I) } (\lnot I) } (\lnot E) \end{align}
I naively suspect we could use $(\lnot I)$ to create even more garbage rules, but I am unsure.
The coverage of this topic in the book isn't very helpful.
You have to consider that $\phi$ is not a propositional letter $p_i$, but a metavariable that denotes a "generic" formula [see page 33].
In a nutshell, the rule "adds" a $¬$ occurrence to the assumption $\phi$, deriving $¬ \phi$, and discharge the assumption.
If the assumption is e.g. $¬¬¬ \psi$, then the conlcusion will be : $¬¬¬¬ \psi$, with one more occurrence of $¬$.
In the example, the application of (¬I) discharge the assumption "labelled" (1), i.e. $¬ \phi$, deriving $¬¬ \phi$.