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  7452  nninfisollem0  7471  nninfisollemne  7472  nninfisollemeq  7473  nninfisol  7474  fodjuomnilemdc  7485  omniwomnimkv  7508  exmidonfinlem  7546  exmidfodomrlemr  7555  exmidfodomrlemrALT  7556  exmidaclem  7565  elni2  7682  indpi  7710  distrlem4prl  7952  distrlem4pru  7953  sup3exmid  9290  zdcle  9726  zdclt  9727  uzin  9965  elnn1uz2  10017  eluzdc  10020  xnn0dcle  10215  xrpnfdc  10255  xrmnfdc  10256  fztri3or  10454  fzdcel  10455  fzneuz  10519  exfzdc  10670  infssuzex  10677  qdclt  10691  fzfig  10882  fzowrddc  11435  sumdc  12143  zsumdc  12170  isum  12171  sum0  12174  fisumss  12178  isumss2  12179  fsumsplit  12193  sumsplitdc  12218  isumlessdc  12282  zproddc  12365  iprodap  12366  iprodap0  12368  prod0  12371  fprodssdc  12376  fprodsplitdc  12382  fprodsplit  12383  fprodunsn  12390  ef0lem  12446  nnwosdc  12835  prmdc  12927  prmdcz  12928  nn0sqdcq  13007  pclemdc  13090  1arith  13169  ballotfilemcdc  13275  ennnfonelemdc  13342  ctiunctlemudc  13380  ppiprm  16220  chtprm  16222  efchtqdvds  16226  ppidif  16230  prmorcht  16243  ppiqub  16254  1loopgruspgr  16710  eupth2lem3lem4fi  16880  bj-trdc  16946  bj-fadc  16948  bj-dcstab  16950  bj-nndcALT  16952  decidi  16989  decidr  16990  bj-charfunr  17002  bddc  17020  subctctexmid  17196  wexmiddc  17208  wexmiddiffi  17210  wexmiddifxylem  17211  triap  17244  dceqnconst  17277  dcapnconst  17278  nconstwlpolem0  17280  nconstwlpo  17283  dftest  17292