Definition df-dc 835

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 853, exmiddc 836, peircedc 914, or notnotrdc 843, 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 834	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 708	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  836  pm2.1dc  837  dcbid  838  dcim  841  dcn  842  notnotrdc  843  stdcndc  845  stdcndcOLD  846  stdcn  847  dcnnOLD  849  nndc  851  condcOLD  854  pm2.61ddc  861  pm5.18dc  883  pm2.13dc  885  pm2.25dc  893  pm2.85dc  905  pm5.12dc  910  pm5.14dc  911  pm5.55dc  913  peircedc  914  pm5.54dc  918  dcan  933  dcor  935  pm5.62dc  945  pm5.63dc  946  pm4.83dc  951  xordc1  1393  biassdc  1395  19.30dc  1627  nfdc  1659  exmodc  2076  moexexdc  2110  dcne  2358  eueq2dc  2910  eueq3dc  2911  abvor0dc  3446  dcun  3533  ifcldcd  3570  ifnotdc  3571  ifandc  3572  ifmdc  3574  exmid01  4196  exmidsssnc  4201  exmidundif  4204  exmidundifim  4205  exmid1stab  4206  ontriexmidim  4519  ontri2orexmidim  4569  dcextest  4578  nndceq0  4615  nndceq  6495  nndcel  6496  fidceq  6864  tridc  6894  finexdc  6897  unsnfidcex  6914  unsnfidcel  6915  undifdcss  6917  dcfi  6975  ctssdccl  7105  nninfisollem0  7123  nninfisollemne  7124  nninfisollemeq  7125  nninfisol  7126  fodjuomnilemdc  7137  omniwomnimkv  7160  exmidonfinlem  7187  exmidfodomrlemr  7196  exmidfodomrlemrALT  7197  exmidaclem  7202  elni2  7308  indpi  7336  distrlem4prl  7578  distrlem4pru  7579  sup3exmid  8908  zdcle  9323  zdclt  9324  uzin  9554  elnn1uz2  9601  eluzdc  9604  xnn0dcle  9796  xrpnfdc  9836  xrmnfdc  9837  fztri3or  10032  fzdcel  10033  fzneuz  10094  exfzdc  10233  fzfig  10423  sumdc  11357  zsumdc  11383  isum  11384  sum0  11387  fisumss  11391  isumss2  11392  fsumsplit  11406  sumsplitdc  11431  isumlessdc  11495  zproddc  11578  iprodap  11579  iprodap0  11581  prod0  11584  fprodssdc  11589  fprodsplitdc  11595  fprodsplit  11596  fprodunsn  11603  ef0lem  11659  infssuzex  11940  nnwosdc  12030  prmdc  12120  pclemdc  12278  1arith  12355  ennnfonelemdc  12390  ctiunctlemudc  12428  bj-trdc  14275  bj-fadc  14277  bj-dcstab  14279  bj-nndcALT  14281  decidi  14318  decidr  14319  bj-charfunr  14333  bddc  14351  subctctexmid  14521  triap  14548  dceqnconst  14578  dcapnconst  14579  nconstwlpolem0  14581  nconstwlpo  14584  dftest  14593