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  924  pm5.62dc  934  pm5.63dc  935  pm4.83dc  940  xordc1  1382  biassdc  1384  19.30dc  1614  nfdc  1646  exmodc  2063  moexexdc  2097  dcne  2345  eueq2dc  2894  eueq3dc  2895  abvor0dc  3427  dcun  3514  ifcldcd  3550  ifandc  3551  ifmdc  3552  exmid01  4171  exmidsssnc  4176  exmidundif  4179  exmidundifim  4180  ontriexmidim  4493  ontri2orexmidim  4543  dcextest  4552  nndceq0  4589  nndceq  6458  nndcel  6459  fidceq  6826  tridc  6856  finexdc  6859  unsnfidcex  6876  unsnfidcel  6877  undifdcss  6879  dcfi  6937  ctssdccl  7067  nninfisollem0  7085  nninfisollemne  7086  nninfisollemeq  7087  nninfisol  7088  fodjuomnilemdc  7099  omniwomnimkv  7122  exmidonfinlem  7140  exmidfodomrlemr  7149  exmidfodomrlemrALT  7150  exmidaclem  7155  elni2  7246  indpi  7274  distrlem4prl  7516  distrlem4pru  7517  sup3exmid  8843  zdcle  9258  zdclt  9259  uzin  9489  elnn1uz2  9536  eluzdc  9539  xnn0dcle  9729  xrpnfdc  9769  xrmnfdc  9770  fztri3or  9964  fzdcel  9965  fzneuz  10026  exfzdc  10165  fzfig  10355  sumdc  11285  zsumdc  11311  isum  11312  sum0  11315  fisumss  11319  isumss2  11320  fsumsplit  11334  sumsplitdc  11359  isumlessdc  11423  zproddc  11506  iprodap  11507  iprodap0  11509  prod0  11512  fprodssdc  11517  fprodsplitdc  11523  fprodsplit  11524  fprodunsn  11531  ef0lem  11587  infssuzex  11867  prmdc  12041  pclemdc  12197  ennnfonelemdc  12269  ctiunctlemudc  12307  bj-trdc  13466  bj-fadc  13468  bj-dcstab  13470  bj-nndcALT  13472  decidi  13511  decidr  13512  bj-charfunr  13527  bddc  13545  exmid1stab  13714  subctctexmid  13715  triap  13742  dceqnconst  13772  dcapnconst  13773  nconstwlpolem0  13775  nconstwlpo  13778  dftest  13785