Definition df-dc 825

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 843, exmiddc 826, peircedc 904, or notnotrdc 833, 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 824	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 698	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 104	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  826  pm2.1dc  827  dcbid  828  dcim  831  dcn  832  notnotrdc  833  stdcndc  835  stdcndcOLD  836  stdcn  837  dcnnOLD  839  nndc  841  condcOLD  844  pm2.61ddc  851  pm5.18dc  873  pm2.13dc  875  pm2.25dc  883  pm2.85dc  895  pm5.12dc  900  pm5.14dc  901  pm5.55dc  903  peircedc  904  pm5.54dc  908  dcan  923  dcor  925  pm5.62dc  935  pm5.63dc  936  pm4.83dc  941  xordc1  1383  biassdc  1385  19.30dc  1615  nfdc  1647  exmodc  2064  moexexdc  2098  dcne  2347  eueq2dc  2899  eueq3dc  2900  abvor0dc  3432  dcun  3519  ifcldcd  3555  ifnotdc  3556  ifandc  3557  ifmdc  3558  exmid01  4177  exmidsssnc  4182  exmidundif  4185  exmidundifim  4186  ontriexmidim  4499  ontri2orexmidim  4549  dcextest  4558  nndceq0  4595  nndceq  6467  nndcel  6468  fidceq  6835  tridc  6865  finexdc  6868  unsnfidcex  6885  unsnfidcel  6886  undifdcss  6888  dcfi  6946  ctssdccl  7076  nninfisollem0  7094  nninfisollemne  7095  nninfisollemeq  7096  nninfisol  7097  fodjuomnilemdc  7108  omniwomnimkv  7131  exmidonfinlem  7149  exmidfodomrlemr  7158  exmidfodomrlemrALT  7159  exmidaclem  7164  elni2  7255  indpi  7283  distrlem4prl  7525  distrlem4pru  7526  sup3exmid  8852  zdcle  9267  zdclt  9268  uzin  9498  elnn1uz2  9545  eluzdc  9548  xnn0dcle  9738  xrpnfdc  9778  xrmnfdc  9779  fztri3or  9974  fzdcel  9975  fzneuz  10036  exfzdc  10175  fzfig  10365  sumdc  11299  zsumdc  11325  isum  11326  sum0  11329  fisumss  11333  isumss2  11334  fsumsplit  11348  sumsplitdc  11373  isumlessdc  11437  zproddc  11520  iprodap  11521  iprodap0  11523  prod0  11526  fprodssdc  11531  fprodsplitdc  11537  fprodsplit  11538  fprodunsn  11545  ef0lem  11601  infssuzex  11882  nnwosdc  11972  prmdc  12062  pclemdc  12220  1arith  12297  ennnfonelemdc  12332  ctiunctlemudc  12370  bj-trdc  13633  bj-fadc  13635  bj-dcstab  13637  bj-nndcALT  13639  decidi  13676  decidr  13677  bj-charfunr  13692  bddc  13710  exmid1stab  13880  subctctexmid  13881  triap  13908  dceqnconst  13938  dcapnconst  13939  nconstwlpolem0  13941  nconstwlpo  13944  dftest  13951