Definition df-dc 825

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 843, exmiddc 826, peircedc 904, or notnotrdc 833, 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 824	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 698	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 104	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  826  pm2.1dc  827  dcbid  828  dcim  831  dcn  832  notnotrdc  833  stdcndc  835  stdcndcOLD  836  stdcn  837  dcnnOLD  839  nndc  841  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.13dc  875  pm2.25dc  883  pm2.85dc  895  pm5.12dc  900  pm5.14dc  901  pm5.55dc  903  peircedc  904  pm5.54dc  908  dcan  923  dcor  925  pm5.62dc  935  pm5.63dc  936  pm4.83dc  941  xordc1  1383  biassdc  1385  19.30dc  1615  nfdc  1647  exmodc  2064  moexexdc  2098  dcne  2346  eueq2dc  2898  eueq3dc  2899  abvor0dc  3431  dcun  3518  ifcldcd  3554  ifnotdc  3555  ifandc  3556  ifmdc  3557  exmid01  4176  exmidsssnc  4181  exmidundif  4184  exmidundifim  4185  ontriexmidim  4498  ontri2orexmidim  4548  dcextest  4557  nndceq0  4594  nndceq  6463  nndcel  6464  fidceq  6831  tridc  6861  finexdc  6864  unsnfidcex  6881  unsnfidcel  6882  undifdcss  6884  dcfi  6942  ctssdccl  7072  nninfisollem0  7090  nninfisollemne  7091  nninfisollemeq  7092  nninfisol  7093  fodjuomnilemdc  7104  omniwomnimkv  7127  exmidonfinlem  7145  exmidfodomrlemr  7154  exmidfodomrlemrALT  7155  exmidaclem  7160  elni2  7251  indpi  7279  distrlem4prl  7521  distrlem4pru  7522  sup3exmid  8848  zdcle  9263  zdclt  9264  uzin  9494  elnn1uz2  9541  eluzdc  9544  xnn0dcle  9734  xrpnfdc  9774  xrmnfdc  9775  fztri3or  9970  fzdcel  9971  fzneuz  10032  exfzdc  10171  fzfig  10361  sumdc  11295  zsumdc  11321  isum  11322  sum0  11325  fisumss  11329  isumss2  11330  fsumsplit  11344  sumsplitdc  11369  isumlessdc  11433  zproddc  11516  iprodap  11517  iprodap0  11519  prod0  11522  fprodssdc  11527  fprodsplitdc  11533  fprodsplit  11534  fprodunsn  11541  ef0lem  11597  infssuzex  11878  nnwosdc  11968  prmdc  12058  pclemdc  12216  1arith  12293  ennnfonelemdc  12328  ctiunctlemudc  12366  bj-trdc  13593  bj-fadc  13595  bj-dcstab  13597  bj-nndcALT  13599  decidi  13636  decidr  13637  bj-charfunr  13652  bddc  13670  exmid1stab  13840  subctctexmid  13841  triap  13868  dceqnconst  13898  dcapnconst  13899  nconstwlpolem0  13901  nconstwlpo  13904  dftest  13911