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  2092  moexexdc  2126  dcne  2375  eueq2dc  2934  eueq3dc  2935  abvor0dc  3471  dcun  3557  ifcldcd  3594  ifnotdc  3595  ifandc  3596  ifmdc  3598  exmid01  4228  exmidsssnc  4233  exmidundif  4236  exmidundifim  4237  exmid1stab  4238  ontriexmidim  4555  ontri2orexmidim  4605  dcextest  4614  nndceq0  4651  nndceq  6554  nndcel  6555  fidceq  6927  tridc  6957  finexdc  6960  unsnfidcex  6978  unsnfidcel  6979  undifdcss  6981  dcfi  7042  ctssdccl  7172  nninfisollem0  7191  nninfisollemne  7192  nninfisollemeq  7193  nninfisol  7194  fodjuomnilemdc  7205  omniwomnimkv  7228  exmidonfinlem  7255  exmidfodomrlemr  7264  exmidfodomrlemrALT  7265  exmidaclem  7270  elni2  7376  indpi  7404  distrlem4prl  7646  distrlem4pru  7647  sup3exmid  8978  zdcle  9396  zdclt  9397  uzin  9628  elnn1uz2  9675  eluzdc  9678  xnn0dcle  9871  xrpnfdc  9911  xrmnfdc  9912  fztri3or  10108  fzdcel  10109  fzneuz  10170  exfzdc  10310  qdclt  10318  fzfig  10504  sumdc  11504  zsumdc  11530  isum  11531  sum0  11534  fisumss  11538  isumss2  11539  fsumsplit  11553  sumsplitdc  11578  isumlessdc  11642  zproddc  11725  iprodap  11726  iprodap0  11728  prod0  11731  fprodssdc  11736  fprodsplitdc  11742  fprodsplit  11743  fprodunsn  11750  ef0lem  11806  infssuzex  12089  nnwosdc  12179  prmdc  12271  pclemdc  12429  1arith  12508  ennnfonelemdc  12559  ctiunctlemudc  12597  bj-trdc  15314  bj-fadc  15316  bj-dcstab  15318  bj-nndcALT  15320  decidi  15357  decidr  15358  bj-charfunr  15372  bddc  15390  subctctexmid  15561  triap  15589  dceqnconst  15620  dcapnconst  15621  nconstwlpolem0  15623  nconstwlpo  15626  dftest  15635