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

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

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.

• To (A) : Yes. – Mauro ALLEGRANZA Jul 29 '16 at 11:28
• To (B) : ??? The application of ($\lnot$I) discharge the assumption "labelled" (1), i.e. $\lnot \phi$. – Mauro ALLEGRANZA Jul 29 '16 at 11:30
• @MauroALLEGRANZA every other rule so far has taken the thing on the top and performed an operation on it, so I was reading $(\lnot I)$ as 'taking' the $\bot$ as input to make $(\lnot\phi)$. – cjh Jul 29 '16 at 11:35
• @MauroALLEGRANZA however if instead $(\lnot I)$ must always operate on $\bot$ and it adds a $\lnot$ to any assumption it crosses - then that makes more sense. Is this correct? – cjh Jul 29 '16 at 11:36
• @MauroALLEGRANZA ohh of course, the top for $(\lnot I)$ is the value $\bot$ rather than a variable like $\phi$, so of course it is special. – cjh Jul 29 '16 at 11:40

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