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 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 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 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wdc 846	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 720	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

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  6777  nndcel  6778  fidceq  7177  fidcen  7209  tridc  7210  finexdc  7213  elssdc  7215  eqsndc  7216  unsnfidcex  7233  unsnfidcel  7234  undifdcss  7236  exmidssfi  7252  fissfi  7269  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  9730  zdclt  9731  uzin  9970  elnn1uz2  10022  eluzdc  10025  xnn0dcle  10220  xrpnfdc  10260  xrmnfdc  10261  fztri3or  10459  fzdcel  10460  fzneuz  10524  exfzdc  10675  infssuzex  10682  qdclt  10696  fzfig  10887  fzowrddc  11440  sumdc  12148  zsumdc  12175  isum  12176  sum0  12179  fisumss  12183  isumss2  12184  fsumsplit  12198  sumsplitdc  12223  isumlessdc  12287  zproddc  12370  iprodap  12371  iprodap0  12373  prod0  12376  fprodssdc  12381  fprodsplitdc  12387  fprodsplit  12388  fprodunsn  12395  ef0lem  12451  nnwosdc  12840  prmdc  12932  prmdcz  12933  nn0sqdcq  13012  pclemdc  13095  1arith  13174  ballotfilemcdc  13280  ennnfonelemdc  13347  ctiunctlemudc  13385  gsummptfidmsplit  14253  ppiprm  16276  chtprm  16278  efchtqdvds  16282  ppidif  16286  prmorcht  16299  ppiqub  16310  1loopgruspgr  16766  eupth2lem3lem4fi  16936  bj-trdc  17002  bj-fadc  17004  bj-dcstab  17006  bj-nndcALT  17008  decidi  17045  decidr  17046  bj-charfunr  17058  bddc  17076  subctctexmid  17252  wexmiddc  17264  wexmiddiffi  17266  wexmiddifxylem  17267  triap  17301  dceqnconst  17334  dcapnconst  17335  nconstwlpolem0  17337  nconstwlpo  17340  dftest  17349