# How to prove double negation elimination without using $\bot$?

$$\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}$$ I am trying to derive some rules without the use of the $$\bot$$ symbol.

First I want to describe how I am defining certain inference rules:

Negation Introduction: $$\{(a\to b), (a \to \lnot b) \} \vdash \lnot a$$:

$$\fitch{} {\fitch{a} {\vdots \\b} \\a\to b\\ {\fitch{a} {\vdots \\\lnot b}} \\ a \to \lnot b \\ \lnot a}$$

Now presume that we take the law of excluded middle $$a \lor \lnot a$$ as an axiom and use it (with negation introduction and disjunction elimination) to prove the double-negation rule:

$$\fitch{\lnot \lnot a}{ a \lor \lnot a \\ \fitch{a}{ a } \\ a \to a \\ \fitch{\lnot a}{ \vdots \\ a } \\ \lnot a \to a \\ a \text{ (by or-elim using LEM and the two implications)} }$$

I can't quite figure out how to fill in the dotted section. Normally we'd just restate $$\lnot \lnot a$$ and note the contradiction with $$\lnot a$$, state the contradiction $$\bot$$, and then use ex falso $$\bot \to a$$ to invoke $$a$$ and finish the proof.

But without the $$\bot$$ symbol, is this impossible to do? I don't know how to prove ex falso in the first place without using $$\bot$$ or double negation elimination which is the very thing I am trying to prove.

• So are you using "proof by cases"? [That is, from p or q and p ->r and q -> r get r.] I mean is using this rule OK in your restricted system without $\bot$ – coffeemath Oct 9 '18 at 1:51
• @coffeemath yes that is allowed – user525966 Oct 9 '18 at 2:07
• Is disjunctive syllogism allowed? You may use that instead. $$\begin{split}\neg a \vdash \neg a\vee a\quad&\quad \neg a\vee a, \neg a \vdash a\\ \hline &\vdash \neg a \to a\end{split}$$ – Graham Kemp Oct 9 '18 at 3:30
• With $a \to b, a \to \lnot b \vdash \lnot a$ as $\lnot$-I rule, you may use $a, \lnot a \vdash b$ as $\lnot$-E rule. – Mauro ALLEGRANZA Oct 9 '18 at 14:10
• If so, using $\lnot a \lor a$ and $\lor$-E, you may derive $\lnot \lnot a \vdash a$. – Mauro ALLEGRANZA Oct 9 '18 at 14:11

Without a falsum constant, your rule of ex falso quodlibet should look something like $$\phi, \neg \phi \vdash \psi$$.   So from the contradictory assumptions, $$\neg\neg a$$ and $$\neg a$$, you may immediately derive $$a$$.

$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline #2\end{array}}\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{a \qquad \text{ex falso quodlibet }\neg a, \neg\neg a \vdash a }\\\vdots}$$

PS: If ex falso quodlibet looks like $$\phi\wedge\neg\phi\vdash\psi$$, simply introduce a conjunction then use it.

PPS

If ex falso quodlibet is not accepted as fundamental, but disjunctive syllogism is, then introduce a disjunction and use that. $$\fitch{\neg\neg a}{\vdots\\\fitch{\neg a}{\neg a\vee a\qquad:\text{disjunctive introduction }\neg a\vdash \neg a\vee a\\a \qquad\qquad:\text{disjunctive syllogism }\neg a\vee a, \neg\neg a \vdash a }\\\vdots}$$

P$$^3$$S

Disjunctive Syllogism and Ex Falso Quodlibet are interprovable - each may be justified only by accepting the other - so which is considered fundamental by a proof system is a matter of preference.   (EFQ has a smaller format.) $$\tiny\fitch{((p\lor q)\land\lnot p)\to q:\text{Premise of Disj.Sylogism}}{\fitch{p\land\lnot p}{\lnot p:\text{Conj. Elim.}\\p:\text{Conj.Elim.}\\p\lor q:\text{Disj.Intro}\\(p\lor q)\land\lnot p:\text{Conj.Into.}\\q:\text{Cond.Elim.}}\\(p\land\lnot p)\to q:\text{Cond.Into}}\fitch{(p\land\lnot p)\to q:\text{Premise of Ex Falso Quodlibet}}{\fitch{(p\vee q)\land\lnot p}{\lnot p:\text{Conj.Elim.}\\p\lor q:\text{Conj.Elim.}\\\fitch{p}{p\land\lnot p:\text{Conj.Intro.}\\q:\text{Cond.Elim.}}\\p\to q:\text{Cond.Into.}\\\fitch{q}{}\\q\to q:\text{Cond.Intro.}\\q:\text{Disj.Elim.}}\\((p\vee q)\land\lnot p)\to q:\text{Cond.Into.}}$$

P$$^4$$S Oh!   As Mauro comments, if $$\phi\to\psi,\phi\to\neg \psi\vdash \neg \phi$$ is considered as the negation introduction rule, then $$\phi,\neg\phi\vdash\psi$$ (EFQ) could be considered the corresponding negation elimination rule.   Thereby cutting out the need for a falsum symbol.

• But does it require it's own rule or is it derivable? – user525966 Oct 9 '18 at 2:08
• Ex falso quolibet is a fundamental rule of natural deduction, though it is sometimes justified by accepting disjunctive syllogism. – Graham Kemp Oct 9 '18 at 3:14
• I am trying to get a sense for which rules are derived and which aren't to see where the intuition for certain things come from. The idea of ex falso quodlibet is just a fundamental assumption? We can't prove it from other rules? Proving disjunctive syllogism appears to require double-negation elim. which is what I am trying to prove, for example. – user525966 Oct 9 '18 at 13:23
• Ex falso quodlibet and Disjunctive Syllogism are interprovable - each may be justified by accepting the other. Which of them a N.D. proof system regards as more fundamental is just a matter of preference. @user525966 – Graham Kemp Oct 9 '18 at 22:58
• I think I've also seen formulations in which the rule you would use is $\lnot \phi \rightarrow \psi, \lnot \phi \rightarrow \lnot \psi \vdash \phi$. (Sort of a combination of double negation elimination and negation introduction.) – Daniel Schepler Oct 9 '18 at 23:46