![]() |
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 777 | . 2 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) | |
2 | 1 | biimpi 118 | 1 ⊢ (DECID 𝜑 → (𝜑 ∨ ¬ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 662 DECID wdc 776 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 |
This theorem depends on definitions: df-bi 115 df-dc 777 |
This theorem is referenced by: stabtestimpdc 858 modc 1986 rabxmdc 3297 ifsbdc 3385 ifcldadc 3400 ifeq1dadc 3401 ifbothdadc 3402 ifbothdc 3403 eqifdc 3404 exmidundif 3999 dcextest 4359 dcdifsnid 6195 fidceq 6515 fidifsnen 6516 finexdc 6545 unfiexmid 6555 unsnfidcex 6557 unsnfidcel 6558 undifdcss 6560 ssfirab 6568 exmidomniim 6702 exmidfodomrlemim 6730 nnnninf 8645 exfzdc 9540 flqeqceilz 9614 modifeq2int 9682 modfzo0difsn 9691 modsumfzodifsn 9692 bcval 9992 bccmpl 9997 ibcval5 10006 bcpasc 10009 bccl 10010 hashfzp1 10067 sumdc 10569 isumrblem 10573 fisumcvg 10574 dvdsabseq 10628 zsupcllemstep 10721 infssuzex 10725 gcdval 10731 gcddvds 10735 gcdcl 10738 gcd0id 10750 gcdneg 10753 gcdaddm 10755 dfgcd3 10779 dfgcd2 10783 gcdmultiplez 10790 dvdssq 10800 dvdslcm 10831 lcmcl 10834 lcmneg 10836 lcmgcd 10840 lcmdvds 10841 lcmid 10842 mulgcddvds 10856 cncongr2 10866 prmind2 10882 rpexp 10912 pw2dvdslemn 10923 unennn 10990 sumdc2 11042 nnsf 11237 nninfsellemsuc 11246 |
Copyright terms: Public domain | W3C validator |