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 x = y 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 ph <-> ( ph \/ -. ph ) )

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff ph
2	1	wdc 783	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 667	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 104	1 wff (DECID ph <-> ( ph \/ -. ph ) )

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  10901  zsumdc  10927  isum  10928  sum0  10931  fisumss  10935  isumss2  10936  fsumsplit  10950  sumsplitdc  10975  isumlessdc  11039  ef0lem  11099  infssuzex  11372  nndc  12369  dcdc  12370  decidi  12403  decidr  12404  bddc  12427  bj-dcbi  12527