Definition df-dc 837

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 855, exmiddc 838, peircedc 916, or notnotrdc 845, 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 836	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 710	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  838  pm2.1dc  839  dcbid  840  dcim  843  dcn  844  notnotrdc  845  stdcndc  847  stdcndcOLD  848  stdcn  849  dcnnOLD  851  nndc  853  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.13dc  887  pm2.25dc  895  pm2.85dc  907  pm5.12dc  912  pm5.14dc  913  pm5.55dc  915  peircedc  916  pm5.54dc  920  dcand  935  dcor  938  pm5.62dc  948  pm5.63dc  949  pm4.83dc  954  xordc1  1413  biassdc  1415  dcfromnotnotr  1468  dcfromcon  1469  dcfrompeirce  1470  19.30dc  1651  nfdc  1683  exmodc  2105  moexexdc  2139  dcne  2388  eueq2dc  2950  eueq3dc  2951  abvor0dc  3488  dcun  3574  ifcldcd  3613  ifnotdc  3614  ifandc  3615  ifmdc  3617  exmid01  4250  exmidsssnc  4255  exmidundif  4258  exmidundifim  4259  exmid1stab  4260  ontriexmidim  4578  ontri2orexmidim  4628  dcextest  4637  nndceq0  4674  nndceq  6598  nndcel  6599  fidceq  6981  tridc  7011  finexdc  7014  unsnfidcex  7032  unsnfidcel  7033  undifdcss  7035  dcfi  7098  ctssdccl  7228  nninfisollem0  7247  nninfisollemne  7248  nninfisollemeq  7249  nninfisol  7250  fodjuomnilemdc  7261  omniwomnimkv  7284  exmidonfinlem  7317  exmidfodomrlemr  7326  exmidfodomrlemrALT  7327  exmidaclem  7336  elni2  7447  indpi  7475  distrlem4prl  7717  distrlem4pru  7718  sup3exmid  9050  zdcle  9469  zdclt  9470  uzin  9701  elnn1uz2  9748  eluzdc  9751  xnn0dcle  9944  xrpnfdc  9984  xrmnfdc  9985  fztri3or  10181  fzdcel  10182  fzneuz  10243  exfzdc  10391  infssuzex  10398  qdclt  10410  fzfig  10597  fzowrddc  11123  sumdc  11744  zsumdc  11770  isum  11771  sum0  11774  fisumss  11778  isumss2  11779  fsumsplit  11793  sumsplitdc  11818  isumlessdc  11882  zproddc  11965  iprodap  11966  iprodap0  11968  prod0  11971  fprodssdc  11976  fprodsplitdc  11982  fprodsplit  11983  fprodunsn  11990  ef0lem  12046  nnwosdc  12435  prmdc  12527  pclemdc  12686  1arith  12765  ennnfonelemdc  12845  ctiunctlemudc  12883  bj-trdc  15827  bj-fadc  15829  bj-dcstab  15831  bj-nndcALT  15833  decidi  15870  decidr  15871  bj-charfunr  15884  bddc  15902  subctctexmid  16078  triap  16109  dceqnconst  16140  dcapnconst  16141  nconstwlpolem0  16143  nconstwlpo  16146  dftest  16155