ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  exmiddc Structured version   GIF version

Theorem exmiddc 743
Description: Law of excluded middle, for a decidable proposition. The law of the excluded middle is also called the principle of tertium non datur. Theorem *2.11 of [WhiteheadRussell] p. 101. It says that something is either true or not true; there are no in-between values of truth. The key way in which intuitionistic logic differs from classical logic is that intuitionistic logic says that excluded middle only holds for some propositions, and classical logic says that it holds for all propositions. (Contributed by Jim Kingdon, 12-May-2018.)
Assertion
Ref Expression
exmiddc (DECID φ → (φ ¬ φ))

Proof of Theorem exmiddc
StepHypRef Expression
1 df-dc 742 . 2 (DECID φ ↔ (φ ¬ φ))
21biimpi 113 1 (DECID φ → (φ ¬ φ))
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4   wo 628  DECID wdc 741
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99
This theorem depends on definitions:  df-bi 110  df-dc 742
This theorem is referenced by:  stabtestimpdc  823  modc  1940  rabxmdc  3243
  Copyright terms: Public domain W3C validator