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  3475  dcun  3561  ifcldcd  3598  ifnotdc  3599  ifandc  3600  ifmdc  3602  exmid01  4232  exmidsssnc  4237  exmidundif  4240  exmidundifim  4241  exmid1stab  4242  ontriexmidim  4559  ontri2orexmidim  4609  dcextest  4618  nndceq0  4655  nndceq  6566  nndcel  6567  fidceq  6939  tridc  6969  finexdc  6972  unsnfidcex  6990  unsnfidcel  6991  undifdcss  6993  dcfi  7056  ctssdccl  7186  nninfisollem0  7205  nninfisollemne  7206  nninfisollemeq  7207  nninfisol  7208  fodjuomnilemdc  7219  omniwomnimkv  7242  exmidonfinlem  7274  exmidfodomrlemr  7283  exmidfodomrlemrALT  7284  exmidaclem  7293  elni2  7400  indpi  7428  distrlem4prl  7670  distrlem4pru  7671  sup3exmid  9003  zdcle  9421  zdclt  9422  uzin  9653  elnn1uz2  9700  eluzdc  9703  xnn0dcle  9896  xrpnfdc  9936  xrmnfdc  9937  fztri3or  10133  fzdcel  10134  fzneuz  10195  exfzdc  10335  infssuzex  10342  qdclt  10354  fzfig  10541  sumdc  11542  zsumdc  11568  isum  11569  sum0  11572  fisumss  11576  isumss2  11577  fsumsplit  11591  sumsplitdc  11616  isumlessdc  11680  zproddc  11763  iprodap  11764  iprodap0  11766  prod0  11769  fprodssdc  11774  fprodsplitdc  11780  fprodsplit  11781  fprodunsn  11788  ef0lem  11844  nnwosdc  12233  prmdc  12325  pclemdc  12484  1arith  12563  ennnfonelemdc  12643  ctiunctlemudc  12681  bj-trdc  15506  bj-fadc  15508  bj-dcstab  15510  bj-nndcALT  15512  decidi  15549  decidr  15550  bj-charfunr  15564  bddc  15582  subctctexmid  15755  triap  15786  dceqnconst  15817  dcapnconst  15818  nconstwlpolem0  15820  nconstwlpo  15823  dftest  15832