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  1412  biassdc  1414  dcfromnotnotr  1466  dcfromcon  1467  dcfrompeirce  1468  19.30dc  1649  nfdc  1681  exmodc  2103  moexexdc  2137  dcne  2386  eueq2dc  2945  eueq3dc  2946  abvor0dc  3483  dcun  3569  ifcldcd  3607  ifnotdc  3608  ifandc  3609  ifmdc  3611  exmid01  4241  exmidsssnc  4246  exmidundif  4249  exmidundifim  4250  exmid1stab  4251  ontriexmidim  4568  ontri2orexmidim  4618  dcextest  4627  nndceq0  4664  nndceq  6575  nndcel  6576  fidceq  6948  tridc  6978  finexdc  6981  unsnfidcex  6999  unsnfidcel  7000  undifdcss  7002  dcfi  7065  ctssdccl  7195  nninfisollem0  7214  nninfisollemne  7215  nninfisollemeq  7216  nninfisol  7217  fodjuomnilemdc  7228  omniwomnimkv  7251  exmidonfinlem  7283  exmidfodomrlemr  7292  exmidfodomrlemrALT  7293  exmidaclem  7302  elni2  7409  indpi  7437  distrlem4prl  7679  distrlem4pru  7680  sup3exmid  9012  zdcle  9431  zdclt  9432  uzin  9663  elnn1uz2  9710  eluzdc  9713  xnn0dcle  9906  xrpnfdc  9946  xrmnfdc  9947  fztri3or  10143  fzdcel  10144  fzneuz  10205  exfzdc  10350  infssuzex  10357  qdclt  10369  fzfig  10556  sumdc  11588  zsumdc  11614  isum  11615  sum0  11618  fisumss  11622  isumss2  11623  fsumsplit  11637  sumsplitdc  11662  isumlessdc  11726  zproddc  11809  iprodap  11810  iprodap0  11812  prod0  11815  fprodssdc  11820  fprodsplitdc  11826  fprodsplit  11827  fprodunsn  11834  ef0lem  11890  nnwosdc  12279  prmdc  12371  pclemdc  12530  1arith  12609  ennnfonelemdc  12689  ctiunctlemudc  12727  bj-trdc  15552  bj-fadc  15554  bj-dcstab  15556  bj-nndcALT  15558  decidi  15595  decidr  15596  bj-charfunr  15610  bddc  15628  subctctexmid  15801  triap  15832  dceqnconst  15863  dcapnconst  15864  nconstwlpolem0  15866  nconstwlpo  15869  dftest  15878