constructive-mathematicslogicnatural-deductionproof-writingpropositional-calculus
I was given the task of showing that $(\lnot p \implies p) \vdash p$ cannot be proven in constructive logic (that is, a system with no excluded middle, double negation, or $\lnot$-elimination).
I'm trying to assume that a proof for it exists and use that to show the law of excluded middle, or double negation to arrive at a contradiction. However, I'm a bit stuck and I'm not sure if this is the right approach.
Any input appreciated!
1) $\lnot (A \lor \lnot A)$ --- assumed [a]
2) $A$ --- assumed [b]
3) $A \lor \lnot A$ --- from 1) by $\lor$-intro
4) $\lnot A$ --- from the contradiction : 2) and 3) by $\lnot$-intro, discharging [b]
5) $A \lor \lnot A$ --- $\lor$-intro
6) $\lnot \lnot (A \lor \lnot A)$ --- from the contradiction : 1) and 5) by $\lnot$-intro, discharging [a]
7) $A \lor \lnot A$ --- from 6) by $\lnot \lnot$-elim.
For the different "flavours" of the negation rules in Natural Deduction you can see :
Dag Prawitz, Natural Deduction : A Proof-Theoretical Study (1965), page 35 (for the two $\lnot$-rules replacing the $\bot$-rules in classical logic); or :
Neil Tennant, Natural logic (1978), page 57.
Your idea regarding the proof : $P \to Q \vdash \lnot P \lor Q$ is correct: you can use the "derived" rule :
$$\dfrac { } {\lnot P \lor P}$$
Alternatively :
0) $A \to B$ --- premise
1) $\lnot A$ --- assumed [a]
2) $\lnot A \lor B$ --- by $\lor$-intro
3) $\lnot (\lnot A \lor B)$ --- assumed [b]
4) $\lnot \lnot A$ --- from 1) with contradiction : 2) and 3) by $\lnot$-intro, discharging [a]
5) $A$ --- from 4) by $\lnot \lnot$-elim
6) $B$ --- from 0) and 5) by $\to$-elim
7) $\lnot A \lor B$ --- $\lor$-intro
8) $\lnot \lnot (\lnot A \lor B)$ --- from 3) with contradiction : 7) and 3) by $\lnot$-intro, discharging [b]
9) $\lnot A \lor B$ --- from 8) by $\lnot \lnot$-elim
Thus, from 0) and 9) :
$A \to B \vdash \lnot A \lor B$.
Couple of thoughts:
First, any question like 'is there a proof ...' should always be couched relative to some proof system. i.e you should really ask 'Is there a proof system in which there exists a proof ...'
Second, when you ask for a proof that LEM implies DNE ... that's a little weird, since in classical logics DNE holds without making any further assumptions. That is, for all complete systems $S$ for classic propositional logic we have $\vdash_S \neg \neg \phi \rightarrow \phi$
EDIT: From the comments I understand you are looking for a proof that does not use LEM (nor $\bot \rightarrow \phi$ ... I'll refer to that rule as $\bot$ Elim) as one of its steps. OK, below is a proof done in Fitch, where $\neg$ Elim is defined as going from $\neg \neg \phi$ to $\phi$, so that doesn't use LEM or $\bot$ Elim:
Finaly, if you're looking for a system where you do have to derive $\neg \neg \phi \rightarrow \phi$, but that still does not use LEM or $\bot$ Elim, I point you the Hilbert system, which does not have LEM or $\bot$ Elim as its rules, but you can prove $\neg \neg \phi \rightarrow \phi$ in that system nevertheless.
Best Answer
$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{(\neg p\to p)\to p}{\fitch{\neg\neg p}{\fitch{\neg p}{\bot\\p}\\\neg p\to p\\p}\\\neg\neg p\to p}$
Take $(\neg p\to p)\to p$ as a premise. Assume $\neg\neg p$ and $\neg p$. Derive $p$ by explosion of the contradiction (EFQ). Deduce $\neg p\to p$ by discharging the second assumption (ie $\to$-introduction). Derive $p$ by modus ponens with the premise (or $\to$-elimination). Deduce $\neg\neg p\to p$ by discharging the first premise ($\to$-introduction).
This demonstrates that $(\neg p\to p)\to p\vdash \neg\neg p\to p$ may be derived using only rules of inference acceptable in constructive logic .
Therefore $(\neg\ p\to p)\to p$ can not be a theorem in constructive logic since it constructively entails $\neg\neg p\to p$, which is definitely not a theorem in constructive logic,