How to prove $((P \Rightarrow Q) \Rightarrow P) \Rightarrow P$

Question

Task: prove the Pierce's law by the natural deduction or by the system LK:

$\vdash ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P ?$
$((P \Rightarrow Q) \Rightarrow P) \vdash P ?$
$¬P, ((P \Rightarrow Q) \Rightarrow P) \vdash ?$

I tried to find proof:

$\vdash P \Rightarrow P !$
$P \vdash P !$
$P, (P \Rightarrow Q) \Rightarrow P \vdash P !$
$P \vdash ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P !$

and

$(P \Rightarrow Q) \Rightarrow P \vdash (P \Rightarrow Q) \Rightarrow P$
$(P \Rightarrow Q), (P \Rightarrow Q) \Rightarrow P \vdash P !$
$(P \Rightarrow Q) \vdash ((P \Rightarrow Q) \Rightarrow P) \Rightarrow P !$

But there are formulas on the left.

Note: only implication and negation should be used.

Answer 1

The Natural Deduct proof in Gentzen's style:

$$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{}{(P\to Q)\to P\vdash (P\to Q)\to P}{\small\sf Ass}}{(P\to Q)\to P, (P\to Q)\vdash P}{\small{\to}\sf E}~~\dfrac{\dfrac{\dfrac{}{P,\neg Q\vdash P}{\small\sf Ass}~~\dfrac{}{\neg P,\neg Q\vdash\neg P}{\small\sf Ass}}{P,\neg P\vdash Q}{\small\sf RAA}}{\neg P\vdash P\to Q}{\small\sf{\to}I}}{(P\to Q)\to P, \neg P\vdash P}{\small\sf Cut}~~\dfrac{}{\neg P\vdash \neg P}{\small\sf Ass}}{(P\to Q)\to P\vdash P}{\small\sf RAA}}{\vdash ((P\to Q)\to P)\to P}{\small\sf{\to}I}$$

Answer 2

Without knowing the details of the proof system you're using, it's impossible to give a full answer ("the propositional calculus" can refer to many different proof systems - they all prove the same tautologies, but the details are different). But here's an outline of a proof, which it should be straightforward to translate into your favorite proof system.

Assume $(P\rightarrow Q)\rightarrow P$.

By the law of excluded middle, $P\lor \lnot P$. We'll prove $P$ by cases.

Case 1: $P$. We're done.

Case 2: $\lnot P$. Assume $P$. By explosion, $Q$. So $P\rightarrow Q$. By our assumption and modus ponens, $P$.

Having assumed $(P\rightarrow Q)\rightarrow P$ and proven $P$, we have $((P\rightarrow Q)\rightarrow P)\rightarrow P$.

---

As requested by the OP, I'll translate the above argument into the LK system as presented on this wikipedia page, using only the rules for $\rightarrow$ and $\lnot$ (together with the structural rules and cut).

1. $P\vdash P$ (I)
2. $\vdash \lnot P,P$ (1,$\lnot$R)
3. $\vdash P,\lnot P$ (2, PR)
4. $P\vdash Q,P$ (1, WR)
5. $P\vdash P,Q$ (4, PR)
6. $P,\lnot P\vdash Q$ (5, $\lnot$L)
7. $\lnot P,P\vdash Q$ (6, PL)
8. $\lnot P\vdash (P\rightarrow Q)$ (7, $\rightarrow$R).
9. $\vdash P,(P\rightarrow Q)$ (3,8,Cut)
10. $\vdash (P\rightarrow Q),P$ (9,PR)
11. $(P\rightarrow Q)\rightarrow P \vdash P,P$ (10,1,$\rightarrow$L)
12. $(P\rightarrow Q)\rightarrow P \vdash P$ (11,CR)
13. $\vdash ((P\rightarrow Q)\rightarrow P)\rightarrow P$ (12,$\rightarrow$R)

This is really the same proof strategy as the informal proof above, though the LK system does everything it can to obscure the idea of the proof... I'll try to spell it out.

We start in lines 1-2 by asserting the law of excluded middle. Lines 3-8 argue via explosion (line 6) that $(P\rightarrow Q)$ follows from $\lnot P$. We unify these in line 9, concluding that either $P$ is true or $(P\rightarrow Q)$ is true (this corresponds to the reasoning by cases). Now we apply the especially obscure $\rightarrow$L rule, which says that if we further assume $(P\rightarrow Q)\rightarrow P$ (putting it on the left hand side of the turnstile), then we can apply modus ponens to $(P\rightarrow Q)$ to get $P$ in the second case. Contraction in line 12 observes that in either case we get $P$. Thus, assuming $(P\rightarrow Q)\rightarrow P$ gives $P$, and we have proven the implication in line 13.

Answer 3

One can use truth tables to show the claim. $((P \implies Q) \implies P) \implies P$. $$ \begin{array}{|c|c|c|c|c|} \hline P & Q & (P \implies Q) & ((P \implies Q) \implies P) & ((P \implies Q) \implies P) \implies P \\ \hline T & T & T & T & T \\ \hline T & F & F & T & T \\ \hline F & T & T & F & T \\ \hline F & F & T & F & T \\ \hline \end{array} $$ Hence, the claim holds.

Answer 4

Hint: Equivalently, prove $(P \land \neg Q) \lor P \implies P$. Consider the 2 cases given by the antecedent:

1. $P \land \neg Q$

2. $P$

Answer 5

• Let's admit these principles infered from the truth table of the $\rightarrow$ operator.

(1) if the antecent of a conditional is false, the whole conditional is true

(2) if the antecedent is true while the consequent is false, then the whole conditional is false.

• Now, suppose that $P$ is false.

In that case $( P{\rightarrow}Q)$ is true, because its antecedent is false ( Principle (1) above ) .

So $ ( ( P {\rightarrow}Q) {\rightarrow} P)$ must be false, since its antecedent is true and its consequent false ( Principle (2) above).

• So the negation of $P$ ( i.e. our hypothesis) implies the negation of the proposition $ ( ( P {\rightarrow}Q) {\rightarrow} P)$.

• By contraposition, it means that the conditional you want to prove is true.