Definition df-dc 847

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 x = y corresponds to " x = y is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 865, exmiddc 848, peircedc 926, or notnotrdc 855, 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 ph <-> ( ph \/ -. ph ) )

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2	1	wdc 846	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 720	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  848  pm2.1dc  849  dcbid  850  dcim  853  dcn  854  notnotrdc  855  stdcndc  857  stdcndcOLD  858  stdcn  859  dcnnOLD  861  nndc  863  condcOLD  866  pm2.61ddc  873  pm5.18dc  895  pm2.13dc  897  pm2.25dc  905  pm2.85dc  917  pm5.12dc  922  pm5.14dc  923  pm5.55dc  925  peircedc  926  pm5.54dc  930  dcand  945  dcor  948  pm5.62dc  958  pm5.63dc  959  pm4.83dc  964  ifpdc  992  xordc1  1442  biassdc  1444  dcfromnotnotr  1497  dcfromcon  1498  dcfrompeirce  1499  19.30dc  1680  nfdc  1711  exmodc  2137  moexexdc  2171  dcne  2431  eueq2dc  2999  eueq3dc  3000  abvor0dc  3545  dcun  3637  ifcldcd  3678  ifnotdc  3679  ifandc  3681  ifmdc  3683  ifeqeqxdc  3687  exmid01  4333  exmidsssnc  4338  exmidundif  4341  exmidundifim  4342  exmid1stab  4343  ontriexmidim  4667  ontri2orexmidim  4717  dcextest  4726  nndceq0  4763  nndceq  6765  nndcel  6766  fidceq  7164  fidcen  7196  tridc  7197  finexdc  7200  elssdc  7202  eqsndc  7203  unsnfidcex  7220  unsnfidcel  7221  undifdcss  7223  exmidssfi  7239  fissfi  7256  dcfi  7308  fdcf1  7309  ctssdccl  7444  nninfisollem0  7463  nninfisollemne  7464  nninfisollemeq  7465  nninfisol  7466  fodjuomnilemdc  7477  omniwomnimkv  7500  exmidonfinlem  7538  exmidfodomrlemr  7547  exmidfodomrlemrALT  7548  exmidaclem  7557  elni2  7674  indpi  7702  distrlem4prl  7944  distrlem4pru  7945  sup3exmid  9280  zdcle  9703  zdclt  9704  uzin  9937  elnn1uz2  9989  eluzdc  9992  xnn0dcle  10186  xrpnfdc  10226  xrmnfdc  10227  fztri3or  10425  fzdcel  10426  fzneuz  10489  exfzdc  10640  infssuzex  10647  qdclt  10661  fzfig  10848  fzowrddc  11400  sumdc  12105  zsumdc  12132  isum  12133  sum0  12136  fisumss  12140  isumss2  12141  fsumsplit  12155  sumsplitdc  12180  isumlessdc  12244  zproddc  12327  iprodap  12328  iprodap0  12330  prod0  12333  fprodssdc  12338  fprodsplitdc  12344  fprodsplit  12345  fprodunsn  12352  ef0lem  12408  nnwosdc  12797  prmdc  12889  pclemdc  13048  1arith  13127  ballotfilemcdc  13204  ennnfonelemdc  13271  ctiunctlemudc  13309  1loopgruspgr  16461  eupth2lem3lem4fi  16631  bj-trdc  16697  bj-fadc  16699  bj-dcstab  16701  bj-nndcALT  16703  decidi  16740  decidr  16741  bj-charfunr  16753  bddc  16771  subctctexmid  16947  triap  16986  dceqnconst  17018  dcapnconst  17019  nconstwlpolem0  17021  nconstwlpo  17024  dftest  17033