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  6667  nndcel  6668  fidceq  7056  fidcen  7088  tridc  7089  finexdc  7092  elssdc  7094  eqsndc  7095  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  exmidssfi  7131  dcfi  7180  ctssdccl  7310  nninfisollem0  7329  nninfisollemne  7330  nninfisollemeq  7331  nninfisol  7332  fodjuomnilemdc  7343  omniwomnimkv  7366  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  elni2  7534  indpi  7562  distrlem4prl  7804  distrlem4pru  7805  sup3exmid  9137  zdcle  9556  zdclt  9557  uzin  9789  elnn1uz2  9841  eluzdc  9844  xnn0dcle  10037  xrpnfdc  10077  xrmnfdc  10078  fztri3or  10274  fzdcel  10275  fzneuz  10336  exfzdc  10487  infssuzex  10494  qdclt  10506  fzfig  10693  fzowrddc  11232  sumdc  11936  zsumdc  11963  isum  11964  sum0  11967  fisumss  11971  isumss2  11972  fsumsplit  11986  sumsplitdc  12011  isumlessdc  12075  zproddc  12158  iprodap  12159  iprodap0  12161  prod0  12164  fprodssdc  12169  fprodsplitdc  12175  fprodsplit  12176  fprodunsn  12183  ef0lem  12239  nnwosdc  12628  prmdc  12720  pclemdc  12879  1arith  12958  ennnfonelemdc  13038  ctiunctlemudc  13076  1loopgruspgr  16173  eupth2lem3lem4fi  16343  bj-trdc  16399  bj-fadc  16401  bj-dcstab  16403  bj-nndcALT  16405  decidi  16442  decidr  16443  bj-charfunr  16456  bddc  16474  subctctexmid  16652  triap  16684  dceqnconst  16716  dcapnconst  16717  nconstwlpolem0  16719  nconstwlpo  16722  dftest  16741