Definition df-dc 836

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 "𝑥 = 𝑦 is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 854, exmiddc 837, peircedc 915, or notnotrdc 844, 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 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wdc 835	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 709	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  837  pm2.1dc  838  dcbid  839  dcim  842  dcn  843  notnotrdc  844  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnnOLD  850  nndc  852  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.13dc  886  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  xordc1  1404  biassdc  1406  19.30dc  1638  nfdc  1670  exmodc  2088  moexexdc  2122  dcne  2371  eueq2dc  2925  eueq3dc  2926  abvor0dc  3461  dcun  3548  ifcldcd  3585  ifnotdc  3586  ifandc  3587  ifmdc  3589  exmid01  4216  exmidsssnc  4221  exmidundif  4224  exmidundifim  4225  exmid1stab  4226  ontriexmidim  4539  ontri2orexmidim  4589  dcextest  4598  nndceq0  4635  nndceq  6524  nndcel  6525  fidceq  6897  tridc  6927  finexdc  6930  unsnfidcex  6948  unsnfidcel  6949  undifdcss  6951  dcfi  7010  ctssdccl  7140  nninfisollem0  7158  nninfisollemne  7159  nninfisollemeq  7160  nninfisol  7161  fodjuomnilemdc  7172  omniwomnimkv  7195  exmidonfinlem  7222  exmidfodomrlemr  7231  exmidfodomrlemrALT  7232  exmidaclem  7237  elni2  7343  indpi  7371  distrlem4prl  7613  distrlem4pru  7614  sup3exmid  8944  zdcle  9359  zdclt  9360  uzin  9590  elnn1uz2  9637  eluzdc  9640  xnn0dcle  9832  xrpnfdc  9872  xrmnfdc  9873  fztri3or  10069  fzdcel  10070  fzneuz  10131  exfzdc  10270  fzfig  10461  sumdc  11398  zsumdc  11424  isum  11425  sum0  11428  fisumss  11432  isumss2  11433  fsumsplit  11447  sumsplitdc  11472  isumlessdc  11536  zproddc  11619  iprodap  11620  iprodap0  11622  prod0  11625  fprodssdc  11630  fprodsplitdc  11636  fprodsplit  11637  fprodunsn  11644  ef0lem  11700  infssuzex  11982  nnwosdc  12072  prmdc  12162  pclemdc  12320  1arith  12399  ennnfonelemdc  12450  ctiunctlemudc  12488  bj-trdc  14965  bj-fadc  14967  bj-dcstab  14969  bj-nndcALT  14971  decidi  15008  decidr  15009  bj-charfunr  15023  bddc  15041  subctctexmid  15212  triap  15239  dceqnconst  15270  dcapnconst  15271  nconstwlpolem0  15273  nconstwlpo  15276  dftest  15285