Definition df-dc 840

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 858, exmiddc 841, peircedc 919, or notnotrdc 848, 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 839	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 713	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  841  pm2.1dc  842  dcbid  843  dcim  846  dcn  847  notnotrdc  848  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnnOLD  854  nndc  856  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.13dc  890  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifpdc  985  xordc1  1435  biassdc  1437  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  19.30dc  1673  nfdc  1705  exmodc  2128  moexexdc  2162  dcne  2411  eueq2dc  2976  eueq3dc  2977  abvor0dc  3515  dcun  3601  ifcldcd  3640  ifnotdc  3641  ifandc  3643  ifmdc  3645  exmid01  4282  exmidsssnc  4287  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  ontriexmidim  4614  ontri2orexmidim  4664  dcextest  4673  nndceq0  4710  nndceq  6653  nndcel  6654  fidceq  7039  fidcen  7069  tridc  7070  finexdc  7073  elssdc  7075  eqsndc  7076  unsnfidcex  7093  unsnfidcel  7094  undifdcss  7096  dcfi  7159  ctssdccl  7289  nninfisollem0  7308  nninfisollemne  7309  nninfisollemeq  7310  nninfisol  7311  fodjuomnilemdc  7322  omniwomnimkv  7345  exmidonfinlem  7382  exmidfodomrlemr  7391  exmidfodomrlemrALT  7392  exmidaclem  7401  elni2  7512  indpi  7540  distrlem4prl  7782  distrlem4pru  7783  sup3exmid  9115  zdcle  9534  zdclt  9535  uzin  9767  elnn1uz2  9814  eluzdc  9817  xnn0dcle  10010  xrpnfdc  10050  xrmnfdc  10051  fztri3or  10247  fzdcel  10248  fzneuz  10309  exfzdc  10458  infssuzex  10465  qdclt  10477  fzfig  10664  fzowrddc  11194  sumdc  11884  zsumdc  11910  isum  11911  sum0  11914  fisumss  11918  isumss2  11919  fsumsplit  11933  sumsplitdc  11958  isumlessdc  12022  zproddc  12105  iprodap  12106  iprodap0  12108  prod0  12111  fprodssdc  12116  fprodsplitdc  12122  fprodsplit  12123  fprodunsn  12130  ef0lem  12186  nnwosdc  12575  prmdc  12667  pclemdc  12826  1arith  12905  ennnfonelemdc  12985  ctiunctlemudc  13023  bj-trdc  16171  bj-fadc  16173  bj-dcstab  16175  bj-nndcALT  16177  decidi  16214  decidr  16215  bj-charfunr  16228  bddc  16246  subctctexmid  16425  triap  16457  dceqnconst  16488  dcapnconst  16489  nconstwlpolem0  16491  nconstwlpo  16494  dftest  16503