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  4335  exmidsssnc  4340  exmidundif  4343  exmidundifim  4344  exmid1stab  4345  ontriexmidim  4669  ontri2orexmidim  4719  dcextest  4728  nndceq0  4765  nndceq  6772  nndcel  6773  fidceq  7171  fidcen  7203  tridc  7204  finexdc  7207  elssdc  7209  eqsndc  7210  unsnfidcex  7227  unsnfidcel  7228  undifdcss  7230  exmidssfi  7246  fissfi  7263  dcfi  7315  fdcf1  7316  ctssdccl  7451  nninfisollem0  7470  nninfisollemne  7471  nninfisollemeq  7472  nninfisol  7473  fodjuomnilemdc  7484  omniwomnimkv  7507  exmidonfinlem  7545  exmidfodomrlemr  7554  exmidfodomrlemrALT  7555  exmidaclem  7564  elni2  7681  indpi  7709  distrlem4prl  7951  distrlem4pru  7952  sup3exmid  9287  zdcle  9721  zdclt  9722  uzin  9955  elnn1uz2  10007  eluzdc  10010  xnn0dcle  10204  xrpnfdc  10244  xrmnfdc  10245  fztri3or  10443  fzdcel  10444  fzneuz  10508  exfzdc  10659  infssuzex  10666  qdclt  10680  fzfig  10867  fzowrddc  11419  sumdc  12124  zsumdc  12151  isum  12152  sum0  12155  fisumss  12159  isumss2  12160  fsumsplit  12174  sumsplitdc  12199  isumlessdc  12263  zproddc  12346  iprodap  12347  iprodap0  12349  prod0  12352  fprodssdc  12357  fprodsplitdc  12363  fprodsplit  12364  fprodunsn  12371  ef0lem  12427  nnwosdc  12816  prmdc  12908  pclemdc  13067  1arith  13146  ballotfilemcdc  13223  ennnfonelemdc  13290  ctiunctlemudc  13328  1loopgruspgr  16544  eupth2lem3lem4fi  16714  bj-trdc  16780  bj-fadc  16782  bj-dcstab  16784  bj-nndcALT  16786  decidi  16823  decidr  16824  bj-charfunr  16836  bddc  16854  subctctexmid  17030  wexmiddc  17042  wexmiddiffi  17044  wexmiddifxylem  17045  triap  17078  dceqnconst  17110  dcapnconst  17111  nconstwlpolem0  17113  nconstwlpo  17116  dftest  17125