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 used 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  4337  exmidsssnc  4342  exmidundif  4345  exmidundifim  4346  exmid1stab  4347  ontriexmidim  4671  ontri2orexmidim  4721  dcextest  4730  nndceq0  4767  nndceq  6776  nndcel  6777  fidceq  7175  fidcen  7207  tridc  7208  finexdc  7211  elssdc  7213  eqsndc  7214  unsnfidcex  7231  unsnfidcel  7232  undifdcss  7234  exmidssfi  7250  fissfi  7267  dcfi  7320  fdcf1  7321  ctssdccl  7457  nninfisollem0  7476  nninfisollemne  7477  nninfisollemeq  7478  nninfisol  7479  fodjuomnilemdc  7490  omniwomnimkv  7513  exmidonfinlem  7551  exmidfodomrlemr  7560  exmidfodomrlemrALT  7561  exmidaclem  7570  elni2  7687  indpi  7715  distrlem4prl  7957  distrlem4pru  7958  sup3exmid  9295  zdcle  9732  zdclt  9733  uzin  9971  elnn1uz2  10023  eluzdc  10026  xnn0dcle  10221  xrpnfdc  10261  xrmnfdc  10262  fztri3or  10460  fzdcel  10461  fzneuz  10525  exfzdc  10676  infssuzex  10683  qdclt  10697  fzfig  10888  fzowrddc  11441  sumdc  12149  zsumdc  12176  isum  12177  sum0  12180  fisumss  12184  isumss2  12185  fsumsplit  12199  sumsplitdc  12224  isumlessdc  12288  zproddc  12371  iprodap  12372  iprodap0  12374  prod0  12377  fprodssdc  12382  fprodsplitdc  12388  fprodsplit  12389  fprodunsn  12396  ef0lem  12452  nnwosdc  12841  prmdc  12933  prmdcz  12934  nn0sqdcq  13013  pclemdc  13096  1arith  13175  ballotfilemcdc  13281  ennnfonelemdc  13348  ctiunctlemudc  13386  gsummptfidmsplit  14254  ppiprm  16259  chtprm  16261  efchtqdvds  16265  ppidif  16269  prmorcht  16282  ppiqub  16293  1loopgruspgr  16749  eupth2lem3lem4fi  16919  bj-trdc  16985  bj-fadc  16987  bj-dcstab  16989  bj-nndcALT  16991  decidi  17028  decidr  17029  bj-charfunr  17041  bddc  17059  subctctexmid  17235  wexmiddc  17247  wexmiddiffi  17249  wexmiddifxylem  17250  triap  17284  dceqnconst  17317  dcapnconst  17318  nconstwlpolem0  17320  nconstwlpo  17323  dftest  17332