# Negation of a Formula is Provable without Including the Formula as an Assumption

The following lemma states that if we can prove negation of a Well Formed Formula (WFF) $$\alpha$$ by assuming the formula itself, then we can do it without such an assumption.

Lemma. Let $$\Sigma$$ be a set of WFFs and $$\alpha$$ a WFF. If $$\Sigma \cup \{\alpha\} \vdash (\neg \alpha)$$, then $$\Sigma \vdash (\neg \alpha)$$.

Proof. Suppose that we have shown that $$\vdash ((\alpha \to (\neg \alpha)) \to (\neg \alpha))$$. By the deduction theorem, $$\Sigma \cup \{\alpha\} \vdash (\neg \alpha)$$ implies that $$\Sigma \vdash (\alpha \to (\neg \alpha))$$. By monotonicity, we also have $$\Sigma \vdash ((\alpha \to (\neg \alpha)) \to (\neg \alpha))$$. Now, applying Modus Ponens (MP), we can conclude that $$\Sigma \vdash (\neg \alpha)$$.

As you can see, the proof relies on showing that $$\vdash ((\alpha \to (\neg \alpha)) \to (\neg \alpha))$$. Here is a list of tools that I can use for proving this.

Hilbert Axioms. Any WFF of the the following forms is considered as an axiom.

• $$(\alpha \to (\beta \to \alpha))$$.
• $$\big((\alpha \to (\beta \to \gamma)) \to ((\alpha \to \beta) \to (\alpha \to \gamma))\big)$$.
• $$\big(((\neg \beta) \to (\neg \alpha)) \to (\alpha \to \beta)\big)$$.

Also, by using Hilbert axioms, I have proved the followings.

• $$\vdash (\alpha \to \alpha)$$.
• $$\vdash \big((\neg(\neg \alpha)) \to \alpha\big)$$.
• $$\vdash \big(\alpha \to (\neg(\neg \alpha))\big)$$.

One last thing that I can use is transitivity, which I proved by using the deduction theorem.

• $$\{\alpha \to \beta, \, \beta \to \gamma\} \vdash (\alpha \to \gamma)$$.

Question. How can I show that $$\vdash ((\alpha \to (\neg \alpha)) \to (\neg \alpha))$$? It would be nice to let me know your line of thought for tackling this problem.

• Hint: if we define $\neg \alpha$ as $\alpha \to \bot$, then the proof is just contraction: $\alpha, \alpha \vdash \bot$ implies $\alpha \vdash \bot$. (In $\lambda$-calculus: $\lambda f a. f a a$) Commented Jul 12 at 11:24
• @NaïmFavier: What is $\bot$? Commented Jul 12 at 11:26
• Falsehood. The negation of $\top$. Commented Jul 12 at 11:30
• @NaïmFavier: I am not familiar with these symbols and I do not have them in my formal language. Can you give a hint without these? Commented Jul 12 at 11:35
• @NaïmFavier: As far as we are in the syntax realm, no meaning is attached to these symbols. The notion of a formal proof is purely syntactic. So $\neg$ is just a symbol and we are just playing a game with symbols. Commented Jul 12 at 11:39

IMO the "trick" in similar cases of long derivations in Hilbert-style, is to use some intermediate result as Lemma.

Having Ax.3 and the Doble Negation laws, you can prove all Contraposition laws (various combinations).

In addition, it is useful to have an intermediate result: call it

Lemma 1: $$(A \to \lnot A) \to (B \to \lnot A)$$.

Poof:

1. $$(A \to (\lnot A \to \lnot B))$$ --- easily proved using Ax.1, Contraposition and Transitivity

2. $$(A \to (\lnot A \to \lnot B)) \to ((A \to \lnot A) \to (A \to \lnot B))$$ --- Ax.2

3. $$((A \to \lnot A) \to (A \to \lnot B))$$ --- from 1) and 2) by MP

4. $$(A \to \lnot B) \to (B \to \lnot A)$$ --- Contraposition

5. $$(A \to \lnot A) \to (B \to \lnot A)$$ --- from 3) and 4) by Transitivity.

Now for the main result:

1. $$(A \to \lnot A) \to ((A \to \lnot A) \to \lnot A)$$ --- Lemma 1

2. $$[(A \to \lnot A) \to ((A \to \lnot A) \to \lnot A)] \to [((A \to \lnot A) \to (A \to \lnot A)) \to ((A \to \lnot A) \to \lnot A)]$$ --- Ax.2

3. $$[((A \to \lnot A) \to (A \to \lnot A)) \to ((A \to \lnot A) \to \lnot A) ]$$ --- from 1) and 2) by MP

4. $$((A \to \lnot A) \to (A \to \lnot A))$$ --- from $$(\alpha \to \alpha)$$

1. $$(A \to \lnot A) \to \lnot A$$ --- from 3) and 4) by MP.
• (+1) Thanks a ton. This is exactly what I wanted. But I am wondering how did you come up with such a proof? Can you elaborate on your way of thinking to tackle such problems? Commented Jul 12 at 12:52
• @HoseinRahnama - textbooks and previous experience. I think that a very similar problem has been already discussed in MSE :-) Commented Jul 12 at 12:58
• Do you mean this post? Commented Jul 12 at 12:59
• @HoseinRahnama - good catch! Commented Jul 12 at 13:04

Expanding on my hint in the comments: define $$\top = q \to r \to q$$ (where $$q, r$$ are fresh variables), so that $$\top$$ is provable by axiom 1. Define $$\bot = \neg \top$$. Prove $$\neg\bot$$ using $$\top$$ and $$a \to\neg\neg a$$. Prove $$\bot \to x$$ using axioms 3, 1, MP and $$\neg\bot$$. Prove $$\neg a \to a \to \bot$$ using axioms 3 and 1. Prove $$(a \to b) \to \neg b \to \neg a$$ using axiom 3 and $$a \leftrightarrow \neg\neg a$$. Prove $$(a \to \bot) \to \neg a$$ using the previous theorem and $$\neg\bot$$. Prove $$(a \to a \to \bot) \to a \to \bot$$ using axioms 1 and 2. Prove the claim using the previous results.

There is most likely a more direct way but I can't be bothered to find it. If you want an elegant proof, stop using Hilbert-style systems.

As you requested...

Screenshot:

Note: Consistent with other infix binary operators in the system used here, '=>' is left-associative.

Text version:

1   A => ~A
Premise

2   A
Premise

3   ~A
Detach, 1, 2

4   A & ~A
Join, 2, 3

5   ~A
Conclusion, 2

6   A => ~A => ~A
Conclusion, 1

• That should be (A => ~A) => ~A. Implication is right-associative by convention. Commented Jul 13 at 15:50
• I forgot to mention that '=>' is left associative in the system I use, as with other binary logical connectives. It seemed more... natural. Commented Jul 13 at 15:56
• One appealing reason for having $\to$ right-associative is currying: $A \times B \to C \simeq A \to B \to C$. So you can write down curried multiple-argument functions (or multiple-premise theorems) without drowning in parentheses. On the other hand it is rare to encounter deeply left-nested arrows, except when messing with continuation-passing stuff. Commented Jul 13 at 16:02
• @NaïmFavier It seemed an unnecessary exception to the rule used for other binary logical connectives. Commented Jul 13 at 16:22
• What other connectives? $\land$ and $\lor$ are associative, so it doesn't matter which way you associate them... Commented Jul 13 at 17:06