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  dcfromnotnotr  1458  dcfromcon  1459  dcfrompeirce  1460  19.30dc  1641  nfdc  1673  exmodc  2095  moexexdc  2129  dcne  2378  eueq2dc  2937  eueq3dc  2938  abvor0dc  3474  dcun  3560  ifcldcd  3597  ifnotdc  3598  ifandc  3599  ifmdc  3601  exmid01  4231  exmidsssnc  4236  exmidundif  4239  exmidundifim  4240  exmid1stab  4241  ontriexmidim  4558  ontri2orexmidim  4608  dcextest  4617  nndceq0  4654  nndceq  6557  nndcel  6558  fidceq  6930  tridc  6960  finexdc  6963  unsnfidcex  6981  unsnfidcel  6982  undifdcss  6984  dcfi  7047  ctssdccl  7177  nninfisollem0  7196  nninfisollemne  7197  nninfisollemeq  7198  nninfisol  7199  fodjuomnilemdc  7210  omniwomnimkv  7233  exmidonfinlem  7260  exmidfodomrlemr  7269  exmidfodomrlemrALT  7270  exmidaclem  7275  elni2  7381  indpi  7409  distrlem4prl  7651  distrlem4pru  7652  sup3exmid  8984  zdcle  9402  zdclt  9403  uzin  9634  elnn1uz2  9681  eluzdc  9684  xnn0dcle  9877  xrpnfdc  9917  xrmnfdc  9918  fztri3or  10114  fzdcel  10115  fzneuz  10176  exfzdc  10316  infssuzex  10323  qdclt  10335  fzfig  10522  sumdc  11523  zsumdc  11549  isum  11550  sum0  11553  fisumss  11557  isumss2  11558  fsumsplit  11572  sumsplitdc  11597  isumlessdc  11661  zproddc  11744  iprodap  11745  iprodap0  11747  prod0  11750  fprodssdc  11755  fprodsplitdc  11761  fprodsplit  11762  fprodunsn  11769  ef0lem  11825  nnwosdc  12206  prmdc  12298  pclemdc  12457  1arith  12536  ennnfonelemdc  12616  ctiunctlemudc  12654  bj-trdc  15398  bj-fadc  15400  bj-dcstab  15402  bj-nndcALT  15404  decidi  15441  decidr  15442  bj-charfunr  15456  bddc  15474  subctctexmid  15645  triap  15673  dceqnconst  15704  dcapnconst  15705  nconstwlpolem0  15707  nconstwlpo  15710  dftest  15719