Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > exmiddc | 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 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.) |
Ref | Expression |
---|---|
exmiddc | ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-dc 743 | . 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) | |
2 | 1 | biimpi 113 | 1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 629 DECID wdc 742 |
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 743 |
This theorem is referenced by: stabtestimpdc 824 modc 1943 rabxmdc 3249 ifbothdc 3357 fidceq 6330 fidifsnen 6331 flqeqceilz 9160 |
Copyright terms: Public domain | W3C validator |