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)


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


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


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}


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.

  • 1
    $\begingroup$ To (A) : Yes. $\endgroup$ – Mauro ALLEGRANZA Jul 29 '16 at 11:28
  • 1
    $\begingroup$ To (B) : ??? The application of ($\lnot$I) discharge the assumption "labelled" (1), i.e. $\lnot \phi$. $\endgroup$ – Mauro ALLEGRANZA Jul 29 '16 at 11:30
  • $\begingroup$ @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)$. $\endgroup$ – cjh Jul 29 '16 at 11:35
  • $\begingroup$ @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? $\endgroup$ – cjh Jul 29 '16 at 11:36
  • $\begingroup$ @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. $\endgroup$ – 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$.

  • $\begingroup$ Thank you for putting this in answer form, once again you hit the nail on the head. In hindsight I can't see how I ever thought otherwise, this makes sense now :) $\endgroup$ – cjh Jul 29 '16 at 14:37

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.