Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > exmiddc  Structured version GIF version 
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 inbetween 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, 12May2018.) 
Ref  Expression 

exmiddc  ⊢ (DECID φ → (φ ∨ ¬ φ)) 
Step  Hyp  Ref  Expression 

1  dfdc 742  . 2 ⊢ (DECID φ ↔ (φ ∨ ¬ φ))  
2  1  biimpi 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: ax1 5 ax2 6 axmp 7 axia1 99 
This theorem depends on definitions: dfbi 110 dfdc 742 
This theorem is referenced by: stabtestimpdc 823 modc 1940 rabxmdc 3243 
Copyright terms: Public domain  W3C validator 