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  4569  ontri2orexmidim  4619  dcextest  4628  nndceq0  4665  nndceq  6584  nndcel  6585  fidceq  6965  tridc  6995  finexdc  6998  unsnfidcex  7016  unsnfidcel  7017  undifdcss  7019  dcfi  7082  ctssdccl  7212  nninfisollem0  7231  nninfisollemne  7232  nninfisollemeq  7233  nninfisol  7234  fodjuomnilemdc  7245  omniwomnimkv  7268  exmidonfinlem  7300  exmidfodomrlemr  7309  exmidfodomrlemrALT  7310  exmidaclem  7319  elni2  7426  indpi  7454  distrlem4prl  7696  distrlem4pru  7697  sup3exmid  9029  zdcle  9448  zdclt  9449  uzin  9680  elnn1uz2  9727  eluzdc  9730  xnn0dcle  9923  xrpnfdc  9963  xrmnfdc  9964  fztri3or  10160  fzdcel  10161  fzneuz  10222  exfzdc  10367  infssuzex  10374  qdclt  10386  fzfig  10573  sumdc  11611  zsumdc  11637  isum  11638  sum0  11641  fisumss  11645  isumss2  11646  fsumsplit  11660  sumsplitdc  11685  isumlessdc  11749  zproddc  11832  iprodap  11833  iprodap0  11835  prod0  11838  fprodssdc  11843  fprodsplitdc  11849  fprodsplit  11850  fprodunsn  11857  ef0lem  11913  nnwosdc  12302  prmdc  12394  pclemdc  12553  1arith  12632  ennnfonelemdc  12712  ctiunctlemudc  12750  bj-trdc  15621  bj-fadc  15623  bj-dcstab  15625  bj-nndcALT  15627  decidi  15664  decidr  15665  bj-charfunr  15679  bddc  15697  subctctexmid  15870  triap  15901  dceqnconst  15932  dcapnconst  15933  nconstwlpolem0  15935  nconstwlpo  15938  dftest  15947