Definition df-dc 830

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 x = y corresponds to " x = y is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 848, exmiddc 831, peircedc 909, or notnotrdc 838, any of which would correspond to the assertion that all propositions are decidable.

(Contributed by Jim Kingdon, 11-Mar-2018.)

Assertion

Ref	Expression
df-dc	|- (DECID ph <-> ( ph \/ -. ph ) )

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2	1	wdc 829	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 703	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 104	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  831  pm2.1dc  832  dcbid  833  dcim  836  dcn  837  notnotrdc  838  stdcndc  840  stdcndcOLD  841  stdcn  842  dcnnOLD  844  nndc  846  condcOLD  849  pm2.61ddc  856  pm5.18dc  878  pm2.13dc  880  pm2.25dc  888  pm2.85dc  900  pm5.12dc  905  pm5.14dc  906  pm5.55dc  908  peircedc  909  pm5.54dc  913  dcan  928  dcor  930  pm5.62dc  940  pm5.63dc  941  pm4.83dc  946  xordc1  1388  biassdc  1390  19.30dc  1620  nfdc  1652  exmodc  2069  moexexdc  2103  dcne  2351  eueq2dc  2903  eueq3dc  2904  abvor0dc  3437  dcun  3524  ifcldcd  3560  ifnotdc  3561  ifandc  3562  ifmdc  3563  exmid01  4182  exmidsssnc  4187  exmidundif  4190  exmidundifim  4191  ontriexmidim  4504  ontri2orexmidim  4554  dcextest  4563  nndceq0  4600  nndceq  6476  nndcel  6477  fidceq  6844  tridc  6874  finexdc  6877  unsnfidcex  6894  unsnfidcel  6895  undifdcss  6897  dcfi  6955  ctssdccl  7085  nninfisollem0  7103  nninfisollemne  7104  nninfisollemeq  7105  nninfisol  7106  fodjuomnilemdc  7117  omniwomnimkv  7140  exmidonfinlem  7159  exmidfodomrlemr  7168  exmidfodomrlemrALT  7169  exmidaclem  7174  elni2  7265  indpi  7293  distrlem4prl  7535  distrlem4pru  7536  sup3exmid  8862  zdcle  9277  zdclt  9278  uzin  9508  elnn1uz2  9555  eluzdc  9558  xnn0dcle  9748  xrpnfdc  9788  xrmnfdc  9789  fztri3or  9984  fzdcel  9985  fzneuz  10046  exfzdc  10185  fzfig  10375  sumdc  11310  zsumdc  11336  isum  11337  sum0  11340  fisumss  11344  isumss2  11345  fsumsplit  11359  sumsplitdc  11384  isumlessdc  11448  zproddc  11531  iprodap  11532  iprodap0  11534  prod0  11537  fprodssdc  11542  fprodsplitdc  11548  fprodsplit  11549  fprodunsn  11556  ef0lem  11612  infssuzex  11893  nnwosdc  11983  prmdc  12073  pclemdc  12231  1arith  12308  ennnfonelemdc  12343  ctiunctlemudc  12381  bj-trdc  13748  bj-fadc  13750  bj-dcstab  13752  bj-nndcALT  13754  decidi  13791  decidr  13792  bj-charfunr  13807  bddc  13825  exmid1stab  13995  subctctexmid  13996  triap  14023  dceqnconst  14053  dcapnconst  14054  nconstwlpolem0  14056  nconstwlpo  14059  dftest  14066