Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

I am studying for my logic finals and I came across this question:

Prove $((E\implies F)\implies E)\implies E$

I don't understand how there is a classical contradiction in this proof.

Using natural deduction, could some one explain why there is a classical contradiction in this proof?

Thank you in advance!

share|cite|improve this question
Couldn't you just look at truth tables? – Thomas Apr 23 '12 at 12:34
I have to format it using natural deduction. – Xabi Apr 23 '12 at 12:35
You will need to explain which inference rules you have available. "Natural deduction" is not one thing but a family of related proof systems. They agree more or less on how the intuitionistic fragment works, but what you want to prove is Peirce's law, which is not intuitionistically valid (but is itself one of several possible axioms that will extend intuitionistic logic to classical). So the proof you seek depends critically on which rule or axiom your variant of natural deduction uses to achieve classical logic. – Henning Makholm Apr 23 '12 at 12:40
@Fatz: Doesn't help. You have to tell us what the rules are. – Henning Makholm Apr 23 '12 at 12:46
Isn't this Peirce's law...? – Zhen Lin Apr 23 '12 at 13:56
up vote 1 down vote accepted

In your proof, in steps 4, 6, and 10 you have a contradiction, because you have both E and $ \lnot $E in play. Since you have that contradiction, in the next step you infer the negation of the last assumption you made if you have a proposition which is not a negation, if you have a negation as the last assumption you made you infer the proposition that such a negation negates i. e. if you have p, and you get a contradiction, you may immediately infer $\lnot$p. If you have $\lnot$p, and you have a contradiction, you may immediately infer p.

The sort of contradiction that appears in such proofs isn't exactly the same as a formula which always comes out as false under all valuations (every row of its truth table comes out false), and maybe that has tripped you up here. However, since almost surely your system has a conjunction-introduction rule which says something like "from p and q, we may immediately infer (p$\land$q)", anytime you have a proposition "p" and its negation "$\lnot$p" you can infer a formula which always comes out as false under all valuations.

share|cite|improve this answer

I can give it a try!

I'll assume you are using the natural deduction system that has the normal introduction and elimination rules for the logical symbols, the so-called "intuitionistic fragment" of propositional logic, together with double negation elimination "from $\lnot \lnot A$, conclude $A$'' (DNE). If you started out by adding the rule "if under assumption $\lnot p$ we have $\bot$, then $p$'', we can get (DNE) also.

Open the following assumptions in this order: 1) $(E \rightarrow F) \rightarrow E$, 2) $\lnot E$ and 3) $E \rightarrow F$. From 1) and 2), conclude $E$ contradicting 2), so that we can close assumption 3) and conclude $\lnot (E \rightarrow F)$ by the I-$\lnot$ rule. From this we get $\lnot \lnot E$ and then $E$. This contradicts 2) again, so we can close 2) and get $\lnot \lnot E$ by I-$\lnot$ rule again. By DNL, we have $E$. Hence we can close assumption 1) to get $((E\rightarrow F) \rightarrow E) \rightarrow E$ by I-$\rightarrow$ rule.

We used classical contradiction when we closed off 2) to conclude $E$ by showing that $\lnot E$ is absurd, and also to get from $\lnot \lnot E$ to $E$.

If the order of which assumptions to open seems ad-hoc, it's basically dictated by what you're trying to prove. Since Pierce's law has a $\rightarrow$ as an outer connective, it's prudent to try using the I-$\rightarrow$ first. Then we are left to show $E$ from assumption 1), which is handily proved by DNL.

Hope that helps!

share|cite|improve this answer
We don't have either of De Morgan's laws at play here. – Doug Spoonwood Apr 27 '12 at 13:09
True, not in this proof. From $\lnot(E \rightarrow F)$ we conclude $\lnot \lnot E$ and then $E$ by (DNE), thanks. I'll make the edit above. – lesnikow Apr 28 '12 at 6:23

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.