Definition df-dc 836

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 854, exmiddc 837, peircedc 915, or notnotrdc 844, 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 835	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 709	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  837  pm2.1dc  838  dcbid  839  dcim  842  dcn  843  notnotrdc  844  stdcndc  846  stdcndcOLD  847  stdcn  848  dcnnOLD  850  nndc  852  condcOLD  855  pm2.61ddc  862  pm5.18dc  884  pm2.13dc  886  pm2.25dc  894  pm2.85dc  906  pm5.12dc  911  pm5.14dc  912  pm5.55dc  914  peircedc  915  pm5.54dc  919  dcan  934  dcor  936  pm5.62dc  946  pm5.63dc  947  pm4.83dc  952  xordc1  1403  biassdc  1405  19.30dc  1637  nfdc  1669  exmodc  2086  moexexdc  2120  dcne  2368  eueq2dc  2922  eueq3dc  2923  abvor0dc  3458  dcun  3545  ifcldcd  3582  ifnotdc  3583  ifandc  3584  ifmdc  3586  exmid01  4210  exmidsssnc  4215  exmidundif  4218  exmidundifim  4219  exmid1stab  4220  ontriexmidim  4533  ontri2orexmidim  4583  dcextest  4592  nndceq0  4629  nndceq  6514  nndcel  6515  fidceq  6883  tridc  6913  finexdc  6916  unsnfidcex  6933  unsnfidcel  6934  undifdcss  6936  dcfi  6994  ctssdccl  7124  nninfisollem0  7142  nninfisollemne  7143  nninfisollemeq  7144  nninfisol  7145  fodjuomnilemdc  7156  omniwomnimkv  7179  exmidonfinlem  7206  exmidfodomrlemr  7215  exmidfodomrlemrALT  7216  exmidaclem  7221  elni2  7327  indpi  7355  distrlem4prl  7597  distrlem4pru  7598  sup3exmid  8928  zdcle  9343  zdclt  9344  uzin  9574  elnn1uz2  9621  eluzdc  9624  xnn0dcle  9816  xrpnfdc  9856  xrmnfdc  9857  fztri3or  10053  fzdcel  10054  fzneuz  10115  exfzdc  10254  fzfig  10444  sumdc  11380  zsumdc  11406  isum  11407  sum0  11410  fisumss  11414  isumss2  11415  fsumsplit  11429  sumsplitdc  11454  isumlessdc  11518  zproddc  11601  iprodap  11602  iprodap0  11604  prod0  11607  fprodssdc  11612  fprodsplitdc  11618  fprodsplit  11619  fprodunsn  11626  ef0lem  11682  infssuzex  11964  nnwosdc  12054  prmdc  12144  pclemdc  12302  1arith  12379  ennnfonelemdc  12414  ctiunctlemudc  12452  bj-trdc  14800  bj-fadc  14802  bj-dcstab  14804  bj-nndcALT  14806  decidi  14843  decidr  14844  bj-charfunr  14858  bddc  14876  subctctexmid  15047  triap  15074  dceqnconst  15105  dcapnconst  15106  nconstwlpolem0  15108  nconstwlpo  15111  dftest  15120