Definition df-dc 835

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 853, exmiddc 836, peircedc 914, or notnotrdc 843, 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 834	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 708	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  836  pm2.1dc  837  dcbid  838  dcim  841  dcn  842  notnotrdc  843  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnnOLD  849  nndc  851  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.13dc  885  pm2.25dc  893  pm2.85dc  905  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  peircedc  914  pm5.54dc  918  dcan  933  dcor  935  pm5.62dc  945  pm5.63dc  946  pm4.83dc  951  xordc1  1393  biassdc  1395  19.30dc  1625  nfdc  1657  exmodc  2074  moexexdc  2108  dcne  2356  eueq2dc  2908  eueq3dc  2909  abvor0dc  3444  dcun  3531  ifcldcd  3567  ifnotdc  3568  ifandc  3569  ifmdc  3571  exmid01  4193  exmidsssnc  4198  exmidundif  4201  exmidundifim  4202  ontriexmidim  4515  ontri2orexmidim  4565  dcextest  4574  nndceq0  4611  nndceq  6490  nndcel  6491  fidceq  6859  tridc  6889  finexdc  6892  unsnfidcex  6909  unsnfidcel  6910  undifdcss  6912  dcfi  6970  ctssdccl  7100  nninfisollem0  7118  nninfisollemne  7119  nninfisollemeq  7120  nninfisol  7121  fodjuomnilemdc  7132  omniwomnimkv  7155  exmidonfinlem  7182  exmidfodomrlemr  7191  exmidfodomrlemrALT  7192  exmidaclem  7197  elni2  7288  indpi  7316  distrlem4prl  7558  distrlem4pru  7559  sup3exmid  8885  zdcle  9300  zdclt  9301  uzin  9531  elnn1uz2  9578  eluzdc  9581  xnn0dcle  9771  xrpnfdc  9811  xrmnfdc  9812  fztri3or  10007  fzdcel  10008  fzneuz  10069  exfzdc  10208  fzfig  10398  sumdc  11332  zsumdc  11358  isum  11359  sum0  11362  fisumss  11366  isumss2  11367  fsumsplit  11381  sumsplitdc  11406  isumlessdc  11470  zproddc  11553  iprodap  11554  iprodap0  11556  prod0  11559  fprodssdc  11564  fprodsplitdc  11570  fprodsplit  11571  fprodunsn  11578  ef0lem  11634  infssuzex  11915  nnwosdc  12005  prmdc  12095  pclemdc  12253  1arith  12330  ennnfonelemdc  12365  ctiunctlemudc  12403  bj-trdc  14044  bj-fadc  14046  bj-dcstab  14048  bj-nndcALT  14050  decidi  14087  decidr  14088  bj-charfunr  14102  bddc  14120  exmid1stab  14290  subctctexmid  14291  triap  14318  dceqnconst  14348  dcapnconst  14349  nconstwlpolem0  14351  nconstwlpo  14354  dftest  14361