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