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  4281  exmidsssnc  4286  exmidundif  4289  exmidundifim  4290  exmid1stab  4291  ontriexmidim  4613  ontri2orexmidim  4663  dcextest  4672  nndceq0  4709  nndceq  6643  nndcel  6644  fidceq  7027  tridc  7057  finexdc  7060  unsnfidcex  7078  unsnfidcel  7079  undifdcss  7081  dcfi  7144  ctssdccl  7274  nninfisollem0  7293  nninfisollemne  7294  nninfisollemeq  7295  nninfisol  7296  fodjuomnilemdc  7307  omniwomnimkv  7330  exmidonfinlem  7367  exmidfodomrlemr  7376  exmidfodomrlemrALT  7377  exmidaclem  7386  elni2  7497  indpi  7525  distrlem4prl  7767  distrlem4pru  7768  sup3exmid  9100  zdcle  9519  zdclt  9520  uzin  9751  elnn1uz2  9798  eluzdc  9801  xnn0dcle  9994  xrpnfdc  10034  xrmnfdc  10035  fztri3or  10231  fzdcel  10232  fzneuz  10293  exfzdc  10441  infssuzex  10448  qdclt  10460  fzfig  10647  fzowrddc  11174  sumdc  11864  zsumdc  11890  isum  11891  sum0  11894  fisumss  11898  isumss2  11899  fsumsplit  11913  sumsplitdc  11938  isumlessdc  12002  zproddc  12085  iprodap  12086  iprodap0  12088  prod0  12091  fprodssdc  12096  fprodsplitdc  12102  fprodsplit  12103  fprodunsn  12110  ef0lem  12166  nnwosdc  12555  prmdc  12647  pclemdc  12806  1arith  12885  ennnfonelemdc  12965  ctiunctlemudc  13003  bj-trdc  16074  bj-fadc  16076  bj-dcstab  16078  bj-nndcALT  16080  decidi  16117  decidr  16118  bj-charfunr  16131  bddc  16149  subctctexmid  16325  triap  16356  dceqnconst  16387  dcapnconst  16388  nconstwlpolem0  16390  nconstwlpo  16393  dftest  16402