Definition df-dc 776

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 782, exmiddc 777, peircedc 853, or notnotrdc 784, 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 775	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 661	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 103	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  777  pm2.1dc  778  dcn  779  dcbii  780  dcbid  781  condc  782  notnotrdc  784  pm2.61ddc  791  pm5.18dc  810  pm2.13dc  812  dcim  817  pm2.25dc  825  pm2.85dc  844  pm5.12dc  849  pm5.14dc  850  pm5.55dc  852  peircedc  853  dftest  855  testbitestn  856  stabtestimpdc  857  pm5.54dc  860  dcan  875  dcor  876  pm5.62dc  886  pm5.63dc  887  pm4.83dc  892  xordc1  1324  biassdc  1326  19.30dc  1558  nfdc  1589  exmodc  1991  moexexdc  2025  dcne  2256  eueq2dc  2765  eueq3dc  2766  abvor0dc  3269  ifcldcd  3381  nndceq0  4357  nndceq  6100  nndcel  6101  nndifsnid  6103  fidceq  6354  fidifsnid  6356  unsnfidcex  6385  unsnfidcel  6386  elni2  6504  indpi  6532  distrlem4prl  6774  distrlem4pru  6775  zdcle  8424  zdclt  8425  uzin  8651  elnn1uz2  8694  eluzdc  8697  fztri3or  9058  fzdcel  9059  fzneuz  9118  exfzdc  9249  fzfig  9422  expival  9478  infssuzex  10345  nndc  10571  dcdc  10572  bddc  10619  bj-dcbi  10719