Definition df-dc 847

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 865, exmiddc 848, peircedc 926, or notnotrdc 855, 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 846	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 720	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is used by:  exmiddc  848  pm2.1dc  849  dcbid  850  dcim  853  dcn  854  notnotrdc  855  stdcndc  857  stdcndcOLD  858  stdcn  859  dcnnOLD  861  nndc  863  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.13dc  897  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifpdc  992  xordc1  1442  biassdc  1444  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  19.30dc  1680  nfdc  1711  exmodc  2137  moexexdc  2171  dcne  2431  eueq2dc  2999  eueq3dc  3000  abvor0dc  3545  dcun  3637  ifcldcd  3678  ifnotdc  3679  ifandc  3681  ifmdc  3683  ifeqeqxdc  3687  exmid01  4335  exmidsssnc  4340  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  ontriexmidim  4669  ontri2orexmidim  4719  dcextest  4728  nndceq0  4765  nndceq  6772  nndcel  6773  fidceq  7171  fidcen  7203  tridc  7204  finexdc  7207  elssdc  7209  eqsndc  7210  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  exmidssfi  7246  fissfi  7263  dcfi  7315  fdcf1  7316  ctssdccl  7451  nninfisollem0  7470  nninfisollemne  7471  nninfisollemeq  7472  nninfisol  7473  fodjuomnilemdc  7484  omniwomnimkv  7507  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  elni2  7681  indpi  7709  distrlem4prl  7951  distrlem4pru  7952  sup3exmid  9289  zdcle  9725  zdclt  9726  uzin  9964  elnn1uz2  10016  eluzdc  10019  xnn0dcle  10214  xrpnfdc  10254  xrmnfdc  10255  fztri3or  10453  fzdcel  10454  fzneuz  10518  exfzdc  10669  infssuzex  10676  qdclt  10690  fzfig  10880  fzowrddc  11433  sumdc  12140  zsumdc  12167  isum  12168  sum0  12171  fisumss  12175  isumss2  12176  fsumsplit  12190  sumsplitdc  12215  isumlessdc  12279  zproddc  12362  iprodap  12363  iprodap0  12365  prod0  12368  fprodssdc  12373  fprodsplitdc  12379  fprodsplit  12380  fprodunsn  12387  ef0lem  12443  nnwosdc  12832  prmdc  12924  prmdcz  12925  nn0sqdcq  13004  pclemdc  13087  1arith  13166  ballotfilemcdc  13272  ennnfonelemdc  13339  ctiunctlemudc  13377  ppiprm  16170  ppidif  16175  ppiqub  16194  1loopgruspgr  16642  eupth2lem3lem4fi  16812  bj-trdc  16878  bj-fadc  16880  bj-dcstab  16882  bj-nndcALT  16884  decidi  16921  decidr  16922  bj-charfunr  16934  bddc  16952  subctctexmid  17128  wexmiddc  17140  wexmiddiffi  17142  wexmiddifxylem  17143  triap  17176  dceqnconst  17208  dcapnconst  17209  nconstwlpolem0  17211  nconstwlpo  17214  dftest  17223