![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-dc | Unicode 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 We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 748, exmiddc 743, peircedc 819, or notnot2dc 750, any of which would correspond to the assertion that all propositions are decidable. (Contributed by Jim Kingdon, 11-Mar-2018.) |
Ref | Expression |
---|---|
df-dc |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph |
. . 3
![]() ![]() | |
2 | 1 | wdc 741 |
. 2
![]() ![]() |
3 | 1 | wn 3 |
. . 3
![]() ![]() ![]() |
4 | 1, 3 | wo 628 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | wb 98 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
This definition is referenced by: exmiddc 743 pm2.1dc 744 dcn 745 dcbii 746 dcbid 747 condc 748 notnot2dc 750 pm2.61ddc 757 pm5.18dc 776 pm2.13dc 778 dcim 783 pm2.25dc 791 pm2.85dc 810 pm5.12dc 815 pm5.14dc 816 pm5.55dc 818 peircedc 819 dftest 821 testbitestn 822 stabtestimpdc 823 pm5.54dc 826 dcan 841 dcor 842 pm5.62dc 851 pm5.63dc 852 pm4.83dc 857 xordc1 1281 biassdc 1283 19.30dc 1515 nfdc 1546 exmodc 1947 moexexdc 1981 dcne 2211 eueq2dc 2708 eueq3dc 2709 abvor0dc 3236 nndceq0 4282 nndceq 6015 nndcel 6016 elni2 6298 indpi 6326 distrlem4prl 6560 distrlem4pru 6561 zdcle 8093 zdclt 8094 uzin 8281 elnn1uz2 8320 eluzdc 8323 fztri3or 8673 fzdcel 8674 fzneuz 8733 fzfig 8887 expival 8911 nndc 9235 dcdc 9236 bddc 9283 bj-dcbi 9383 |
Copyright terms: Public domain | W3C validator |