Is it possible to derive Peirce's Law:

⊢∗ [(α → β) → α] → α

in a calculus that has modus ponens, the Deduction Theorem, Cut rule, Inconsistency effect and Principle of Indirect Proof?

Thanks a lot in advance!

  • 1
    $\begingroup$ What do you mean by Inconsistency effect and Principle of indirect Proof? Neither are standard labels. $\endgroup$ – Peter Smith Feb 4 '18 at 7:31
  • $\begingroup$ Sorry about that. Inconsistency Effect: If Φ ⊢ , then Φ ⊢ β for every formula β (if Φ is inconsistent, then any formula can be deduced) . Principle of Indirect Proof: If Φ, ¬ α ⊢ , then Φ ⊢ α (If Φ, ¬ α is inconsistent, then α can be deduced from Φ) . $\endgroup$ – DiscipleOfKant Feb 4 '18 at 7:44
  • $\begingroup$ What you're calling the "Inconsistency Effect" is (much) more commonly called the Principle of Explosion or "ex falso quodlibet" (often shortened to just "ex falso") or, in some contexts, falsity/bottom elimination though that's often written as $\bot E$. $\endgroup$ – Derek Elkins Feb 5 '18 at 1:28
  • $\begingroup$ The Wikipedia article on Peirce's law has good background information. $\endgroup$ – hardmath Feb 5 '18 at 17:27

We refer to: Moshe Machover, Set Theory, Logic and Their Limitations Cambridge UP (1996), page 116-on for the definitions and some results about propositional calculus.


1) $(ϕ → ψ) → ϕ$ --- premise

2) $\lnot \phi$ --- premise

3) $\vdash^* \lnot \phi \to (\phi \to \psi)$ --- Problem 8.8 [page 125]

4) $\phi \to \psi$ --- from 2) and 3) by mp

5) $\phi$ --- from 1) and 4) by mp.

Up to now we have: $(ϕ → ψ) → ϕ, \lnot \phi \vdash^* \phi$.

Obviously: $(ϕ → ψ) → ϕ, \lnot \phi \vdash^* \lnot \phi$.

Thus, we can use Indirect proof to get:

6) $(ϕ → ψ) → ϕ, \vdash^* \phi$.

7) $\vdash^* ((ϕ → ψ ) → ϕ) → ϕ$ --- from 6) by Deduction Theorem.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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