Definition df-dc 777

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 783, exmiddc 778, peircedc 854, or notnotrdc 785, 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 776	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 662	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 103	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  778  pm2.1dc  779  dcn  780  dcbii  781  dcbid  782  condc  783  notnotrdc  785  pm2.61ddc  792  pm5.18dc  811  pm2.13dc  813  dcim  818  pm2.25dc  826  pm2.85dc  845  pm5.12dc  850  pm5.14dc  851  pm5.55dc  853  peircedc  854  dftest  856  testbitestn  857  stabtestimpdc  858  pm5.54dc  861  dcan  876  dcor  877  pm5.62dc  887  pm5.63dc  888  pm4.83dc  893  xordc1  1325  biassdc  1327  19.30dc  1559  nfdc  1590  exmodc  1993  moexexdc  2027  dcne  2260  eueq2dc  2776  eueq3dc  2777  abvor0dc  3289  ifcldcd  3405  exmid01  3996  exmidundif  3999  nndceq0  4394  nndceq  6192  nndcel  6193  fidceq  6515  finexdc  6545  unsnfidcex  6557  unsnfidcel  6558  undifdcss  6560  fodjuomnilemdc  6704  exmidfodomrlemr  6731  exmidfodomrlemrALT  6732  elni2  6776  indpi  6804  distrlem4prl  7046  distrlem4pru  7047  zdcle  8719  zdclt  8720  uzin  8946  elnn1uz2  8989  eluzdc  8992  fztri3or  9348  fzdcel  9349  fzneuz  9408  exfzdc  9540  fzfig  9726  expival  9794  sumdc  10569  infssuzex  10725  nndc  11004  dcdc  11005  decidi  11038  decidr  11039  bddc  11062  bj-dcbi  11162