Is it possible to show $(\lnot p \implies p) \implies p \vdash (\lnot \lnot p \implies p)$ in constructive logic?

Question

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!

Answer 1

Yes. We can reduce as $$(\lnot p\to p)\to p,\lnot\lnot p\vdash p,$$ and then it suffices to show $$ (\lnot p\to p)\to p, \lnot\lnot p\vdash \lnot p \to p,$$ and again we can reduce that to $$ (\lnot p\to p)\to p,\lnot\lnot p, \lnot p\vdash p,$$ and we see we have a statement and its negation to the left of the turnstyle and we're done.

Observe that the left-hand side of the turnstyle in your title has the schematic form of proof by contradiction (note, nothing would change with the above proof if we replaced with $(\lnot p \to \bot)\to p$, and indeed this does not change the semantics of the statement, since we can prove $\bot$ from $\lnot p$ if and only if we can prove $p$ from $\lnot p$). Thus, we might expect this to be an equivalence. And it is... try to prove the other direction.

Answer 2

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

Answer 3

The question had been answered a while ago, but it's one that contains a bunch of red herrings and so I'll post the far broader principle at work:

• If $Q\to P$, then always $(N\to Q)\to(N\to P)$ as well as $(P\to p)\to(Q\to p)$.
• If $Q\to P$, then combining these we further get $\big((N\to P)\to p\big)\to\big((N\to Q)\to p\big)$.

Whenever $Q$ implies $p$, the formula also holds when setting $P=p$. Assuming explosion, $Q=\bot$ implies everything, and $p$ in particular. OP's result is obtained by further specializing with $N=\neg p$.