Definition df-dc 784

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 "x = y is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 790, exmiddc 785, peircedc 861, or notnotrdc 792, 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 783	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 667	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 104	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  785  pm2.1dc  786  dcn  787  dcbii  788  dcbid  789  condc  790  notnotrdc  792  pm2.61ddc  799  pm5.18dc  818  pm2.13dc  820  dcim  825  pm2.25dc  833  pm2.85dc  852  pm5.12dc  857  pm5.14dc  858  pm5.55dc  860  peircedc  861  dftest  863  testbitestn  864  stabtestimpdc  865  pm5.54dc  868  dcan  883  dcor  884  pm5.62dc  894  pm5.63dc  895  pm4.83dc  900  xordc1  1336  biassdc  1338  19.30dc  1570  nfdc  1601  exmodc  2005  moexexdc  2039  dcne  2273  eueq2dc  2802  eueq3dc  2803  abvor0dc  3325  dcun  3412  ifcldcd  3446  ifandc  3447  ifmdc  3448  exmid01  4053  exmidundif  4058  exmidundifim  4059  nndceq0  4459  nndceq  6300  nndcel  6301  fidceq  6665  tridc  6695  finexdc  6698  unsnfidcex  6710  unsnfidcel  6711  undifdcss  6713  fodjuomnilemdc  6887  exmidfodomrlemr  6925  exmidfodomrlemrALT  6926  elni2  6970  indpi  6998  distrlem4prl  7240  distrlem4pru  7241  sup3exmid  8515  zdcle  8921  zdclt  8922  uzin  9150  elnn1uz2  9193  eluzdc  9196  xrpnfdc  9408  xrmnfdc  9409  fztri3or  9602  fzdcel  9603  fzneuz  9664  exfzdc  9800  fzfig  9986  sumdc  10917  zsumdc  10943  isum  10944  sum0  10947  fisumss  10951  isumss2  10952  fsumsplit  10966  sumsplitdc  10991  isumlessdc  11055  ef0lem  11115  infssuzex  11388  nndc  12385  dcdc  12386  decidi  12419  decidr  12420  bddc  12443  bj-dcbi  12543