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

  • $\begingroup$ 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$ $\endgroup$ – coffeemath Oct 9 '18 at 1:51
  • $\begingroup$ @coffeemath yes that is allowed $\endgroup$ – user525966 Oct 9 '18 at 2:07
  • $\begingroup$ 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}$$ $\endgroup$ – Graham Kemp Oct 9 '18 at 3:30
  • 1
    $\begingroup$ 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. $\endgroup$ – Mauro ALLEGRANZA Oct 9 '18 at 14:10
  • $\begingroup$ If so, using $\lnot a \lor a$ and $\lor$-E, you may derive $\lnot \lnot a \vdash a$. $\endgroup$ – 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.


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


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.

  • $\begingroup$ But does it require it's own rule or is it derivable? $\endgroup$ – user525966 Oct 9 '18 at 2:08
  • $\begingroup$ Ex falso quolibet is a fundamental rule of natural deduction, though it is sometimes justified by accepting disjunctive syllogism. $\endgroup$ – Graham Kemp Oct 9 '18 at 3:14
  • $\begingroup$ 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. $\endgroup$ – user525966 Oct 9 '18 at 13:23
  • $\begingroup$ 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 $\endgroup$ – Graham Kemp Oct 9 '18 at 22:58
  • $\begingroup$ 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.) $\endgroup$ – Daniel Schepler Oct 9 '18 at 23:46

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.