Definition df-dc 842

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 860, exmiddc 843, peircedc 921, or notnotrdc 850, 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 841	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 715	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  843  pm2.1dc  844  dcbid  845  dcim  848  dcn  849  notnotrdc  850  stdcndc  852  stdcndcOLD  853  stdcn  854  dcnnOLD  856  nndc  858  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.13dc  892  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifpdc  987  xordc1  1437  biassdc  1439  dcfromnotnotr  1492  dcfromcon  1493  dcfrompeirce  1494  19.30dc  1675  nfdc  1707  exmodc  2130  moexexdc  2164  dcne  2413  eueq2dc  2979  eueq3dc  2980  abvor0dc  3518  dcun  3604  ifcldcd  3643  ifnotdc  3644  ifandc  3646  ifmdc  3648  exmid01  4288  exmidsssnc  4293  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  ontriexmidim  4620  ontri2orexmidim  4670  dcextest  4679  nndceq0  4716  nndceq  6666  nndcel  6667  fidceq  7055  fidcen  7087  tridc  7088  finexdc  7091  elssdc  7093  eqsndc  7094  unsnfidcex  7111  unsnfidcel  7112  undifdcss  7114  exmidssfi  7130  dcfi  7179  ctssdccl  7309  nninfisollem0  7328  nninfisollemne  7329  nninfisollemeq  7330  nninfisol  7331  fodjuomnilemdc  7342  omniwomnimkv  7365  exmidonfinlem  7403  exmidfodomrlemr  7412  exmidfodomrlemrALT  7413  exmidaclem  7422  elni2  7533  indpi  7561  distrlem4prl  7803  distrlem4pru  7804  sup3exmid  9136  zdcle  9555  zdclt  9556  uzin  9788  elnn1uz2  9840  eluzdc  9843  xnn0dcle  10036  xrpnfdc  10076  xrmnfdc  10077  fztri3or  10273  fzdcel  10274  fzneuz  10335  exfzdc  10485  infssuzex  10492  qdclt  10504  fzfig  10691  fzowrddc  11227  sumdc  11918  zsumdc  11944  isum  11945  sum0  11948  fisumss  11952  isumss2  11953  fsumsplit  11967  sumsplitdc  11992  isumlessdc  12056  zproddc  12139  iprodap  12140  iprodap0  12142  prod0  12145  fprodssdc  12150  fprodsplitdc  12156  fprodsplit  12157  fprodunsn  12164  ef0lem  12220  nnwosdc  12609  prmdc  12701  pclemdc  12860  1arith  12939  ennnfonelemdc  13019  ctiunctlemudc  13057  1loopgruspgr  16153  bj-trdc  16348  bj-fadc  16350  bj-dcstab  16352  bj-nndcALT  16354  decidi  16391  decidr  16392  bj-charfunr  16405  bddc  16423  subctctexmid  16601  triap  16633  dceqnconst  16664  dcapnconst  16665  nconstwlpolem0  16667  nconstwlpo  16670  dftest  16686