![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-dc | GIF version |
Description: Propositions which are
known to be true or false are called decidable.
The (classical) Law of the Excluded Middle corresponds to the principle
that all propositions are decidable, but even given intuitionistic logic,
particular kinds of propositions may be decidable (for example, the
proposition that two natural numbers are equal will be decidable under
most sets of axioms).
Our notation for decidability is a connective DECID which we place before the formula in question. For example, DECID 𝑥 = 𝑦 corresponds to "x = y is decidable". We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 749, exmiddc 744, peircedc 820, or notnotrdc 751, any of which would correspond to the assertion that all propositions are decidable. (Contributed by Jim Kingdon, 11-Mar-2018.) |
Ref | Expression |
---|---|
df-dc | ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . . 3 wff 𝜑 | |
2 | 1 | wdc 742 | . 2 wff DECID 𝜑 |
3 | 1 | wn 3 | . . 3 wff ¬ 𝜑 |
4 | 1, 3 | wo 629 | . 2 wff (𝜑 ∨ ¬ 𝜑) |
5 | 2, 4 | wb 98 | 1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑)) |
Colors of variables: wff set class |
This definition is referenced by: exmiddc 744 pm2.1dc 745 dcn 746 dcbii 747 dcbid 748 condc 749 notnotrdc 751 pm2.61ddc 758 pm5.18dc 777 pm2.13dc 779 dcim 784 pm2.25dc 792 pm2.85dc 811 pm5.12dc 816 pm5.14dc 817 pm5.55dc 819 peircedc 820 dftest 822 testbitestn 823 stabtestimpdc 824 pm5.54dc 827 dcan 842 dcor 843 pm5.62dc 852 pm5.63dc 853 pm4.83dc 858 xordc1 1284 biassdc 1286 19.30dc 1518 nfdc 1549 exmodc 1950 moexexdc 1984 dcne 2216 eueq2dc 2714 eueq3dc 2715 abvor0dc 3242 ifcldcd 3358 nndceq0 4339 nndceq 6077 nndcel 6078 nndifsnid 6080 fidceq 6330 fidifsnid 6332 elni2 6412 indpi 6440 distrlem4prl 6682 distrlem4pru 6683 zdcle 8317 zdclt 8318 uzin 8505 elnn1uz2 8544 eluzdc 8547 fztri3or 8903 fzdcel 8904 fzneuz 8963 fzfig 9206 expival 9257 nndc 9900 dcdc 9901 bddc 9948 bj-dcbi 10048 |
Copyright terms: Public domain | W3C validator |