Definition df-dc 836

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 854, exmiddc 837, peircedc 915, or notnotrdc 844, 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 835	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 709	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  837  pm2.1dc  838  dcbid  839  dcim  842  dcn  843  notnotrdc  844  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnnOLD  850  nndc  852  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.13dc  886  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcand  934  dcor  937  pm5.62dc  947  pm5.63dc  948  pm4.83dc  953  xordc1  1404  biassdc  1406  19.30dc  1638  nfdc  1670  exmodc  2092  moexexdc  2126  dcne  2375  eueq2dc  2933  eueq3dc  2934  abvor0dc  3470  dcun  3556  ifcldcd  3593  ifnotdc  3594  ifandc  3595  ifmdc  3597  exmid01  4227  exmidsssnc  4232  exmidundif  4235  exmidundifim  4236  exmid1stab  4237  ontriexmidim  4554  ontri2orexmidim  4604  dcextest  4613  nndceq0  4650  nndceq  6552  nndcel  6553  fidceq  6925  tridc  6955  finexdc  6958  unsnfidcex  6976  unsnfidcel  6977  undifdcss  6979  dcfi  7040  ctssdccl  7170  nninfisollem0  7189  nninfisollemne  7190  nninfisollemeq  7191  nninfisol  7192  fodjuomnilemdc  7203  omniwomnimkv  7226  exmidonfinlem  7253  exmidfodomrlemr  7262  exmidfodomrlemrALT  7263  exmidaclem  7268  elni2  7374  indpi  7402  distrlem4prl  7644  distrlem4pru  7645  sup3exmid  8976  zdcle  9393  zdclt  9394  uzin  9625  elnn1uz2  9672  eluzdc  9675  xnn0dcle  9868  xrpnfdc  9908  xrmnfdc  9909  fztri3or  10105  fzdcel  10106  fzneuz  10167  exfzdc  10307  qdclt  10315  fzfig  10501  sumdc  11501  zsumdc  11527  isum  11528  sum0  11531  fisumss  11535  isumss2  11536  fsumsplit  11550  sumsplitdc  11575  isumlessdc  11639  zproddc  11722  iprodap  11723  iprodap0  11725  prod0  11728  fprodssdc  11733  fprodsplitdc  11739  fprodsplit  11740  fprodunsn  11747  ef0lem  11803  infssuzex  12086  nnwosdc  12176  prmdc  12268  pclemdc  12426  1arith  12505  ennnfonelemdc  12556  ctiunctlemudc  12594  bj-trdc  15244  bj-fadc  15246  bj-dcstab  15248  bj-nndcALT  15250  decidi  15287  decidr  15288  bj-charfunr  15302  bddc  15320  subctctexmid  15491  triap  15519  dceqnconst  15550  dcapnconst  15551  nconstwlpolem0  15553  nconstwlpo  15556  dftest  15565