Definition df-dc 840

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 858, exmiddc 841, peircedc 919, or notnotrdc 848, 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 839	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 713	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  841  pm2.1dc  842  dcbid  843  dcim  846  dcn  847  notnotrdc  848  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnnOLD  854  nndc  856  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.13dc  890  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifpdc  985  xordc1  1435  biassdc  1437  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  19.30dc  1673  nfdc  1705  exmodc  2128  moexexdc  2162  dcne  2411  eueq2dc  2977  eueq3dc  2978  abvor0dc  3516  dcun  3602  ifcldcd  3641  ifnotdc  3642  ifandc  3644  ifmdc  3646  exmid01  4286  exmidsssnc  4291  exmidundif  4294  exmidundifim  4295  exmid1stab  4296  ontriexmidim  4618  ontri2orexmidim  4668  dcextest  4677  nndceq0  4714  nndceq  6662  nndcel  6663  fidceq  7051  fidcen  7081  tridc  7082  finexdc  7085  elssdc  7087  eqsndc  7088  unsnfidcex  7105  unsnfidcel  7106  undifdcss  7108  dcfi  7171  ctssdccl  7301  nninfisollem0  7320  nninfisollemne  7321  nninfisollemeq  7322  nninfisol  7323  fodjuomnilemdc  7334  omniwomnimkv  7357  exmidonfinlem  7394  exmidfodomrlemr  7403  exmidfodomrlemrALT  7404  exmidaclem  7413  elni2  7524  indpi  7552  distrlem4prl  7794  distrlem4pru  7795  sup3exmid  9127  zdcle  9546  zdclt  9547  uzin  9779  elnn1uz2  9831  eluzdc  9834  xnn0dcle  10027  xrpnfdc  10067  xrmnfdc  10068  fztri3or  10264  fzdcel  10265  fzneuz  10326  exfzdc  10476  infssuzex  10483  qdclt  10495  fzfig  10682  fzowrddc  11218  sumdc  11909  zsumdc  11935  isum  11936  sum0  11939  fisumss  11943  isumss2  11944  fsumsplit  11958  sumsplitdc  11983  isumlessdc  12047  zproddc  12130  iprodap  12131  iprodap0  12133  prod0  12136  fprodssdc  12141  fprodsplitdc  12147  fprodsplit  12148  fprodunsn  12155  ef0lem  12211  nnwosdc  12600  prmdc  12692  pclemdc  12851  1arith  12930  ennnfonelemdc  13010  ctiunctlemudc  13048  1loopgruspgr  16109  bj-trdc  16284  bj-fadc  16286  bj-dcstab  16288  bj-nndcALT  16290  decidi  16327  decidr  16328  bj-charfunr  16341  bddc  16359  subctctexmid  16537  triap  16569  dceqnconst  16600  dcapnconst  16601  nconstwlpolem0  16603  nconstwlpo  16606  dftest  16615