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  4253  exmidsssnc  4258  exmidundif  4261  exmidundifim  4262  exmid1stab  4263  ontriexmidim  4583  ontri2orexmidim  4633  dcextest  4642  nndceq0  4679  nndceq  6603  nndcel  6604  fidceq  6987  tridc  7017  finexdc  7020  unsnfidcex  7038  unsnfidcel  7039  undifdcss  7041  dcfi  7104  ctssdccl  7234  nninfisollem0  7253  nninfisollemne  7254  nninfisollemeq  7255  nninfisol  7256  fodjuomnilemdc  7267  omniwomnimkv  7290  exmidonfinlem  7327  exmidfodomrlemr  7336  exmidfodomrlemrALT  7337  exmidaclem  7346  elni2  7457  indpi  7485  distrlem4prl  7727  distrlem4pru  7728  sup3exmid  9060  zdcle  9479  zdclt  9480  uzin  9711  elnn1uz2  9758  eluzdc  9761  xnn0dcle  9954  xrpnfdc  9994  xrmnfdc  9995  fztri3or  10191  fzdcel  10192  fzneuz  10253  exfzdc  10401  infssuzex  10408  qdclt  10420  fzfig  10607  fzowrddc  11133  sumdc  11754  zsumdc  11780  isum  11781  sum0  11784  fisumss  11788  isumss2  11789  fsumsplit  11803  sumsplitdc  11828  isumlessdc  11892  zproddc  11975  iprodap  11976  iprodap0  11978  prod0  11981  fprodssdc  11986  fprodsplitdc  11992  fprodsplit  11993  fprodunsn  12000  ef0lem  12056  nnwosdc  12445  prmdc  12537  pclemdc  12696  1arith  12775  ennnfonelemdc  12855  ctiunctlemudc  12893  bj-trdc  15858  bj-fadc  15860  bj-dcstab  15862  bj-nndcALT  15864  decidi  15901  decidr  15902  bj-charfunr  15915  bddc  15933  subctctexmid  16109  triap  16140  dceqnconst  16171  dcapnconst  16172  nconstwlpolem0  16174  nconstwlpo  16177  dftest  16186