Definition df-dc 837

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 855, exmiddc 838, peircedc 916, or notnotrdc 845, 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 836	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 710	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  838  pm2.1dc  839  dcbid  840  dcim  843  dcn  844  notnotrdc  845  stdcndc  847  stdcndcOLD  848  stdcn  849  dcnnOLD  851  nndc  853  condcOLD  856  pm2.61ddc  863  pm5.18dc  885  pm2.13dc  887  pm2.25dc  895  pm2.85dc  907  pm5.12dc  912  pm5.14dc  913  pm5.55dc  915  peircedc  916  pm5.54dc  920  dcand  935  dcor  938  pm5.62dc  948  pm5.63dc  949  pm4.83dc  954  xordc1  1413  biassdc  1415  dcfromnotnotr  1467  dcfromcon  1468  dcfrompeirce  1469  19.30dc  1650  nfdc  1682  exmodc  2104  moexexdc  2138  dcne  2387  eueq2dc  2946  eueq3dc  2947  abvor0dc  3484  dcun  3570  ifcldcd  3608  ifnotdc  3609  ifandc  3610  ifmdc  3612  exmid01  4243  exmidsssnc  4248  exmidundif  4251  exmidundifim  4252  exmid1stab  4253  ontriexmidim  4571  ontri2orexmidim  4621  dcextest  4630  nndceq0  4667  nndceq  6587  nndcel  6588  fidceq  6968  tridc  6998  finexdc  7001  unsnfidcex  7019  unsnfidcel  7020  undifdcss  7022  dcfi  7085  ctssdccl  7215  nninfisollem0  7234  nninfisollemne  7235  nninfisollemeq  7236  nninfisol  7237  fodjuomnilemdc  7248  omniwomnimkv  7271  exmidonfinlem  7303  exmidfodomrlemr  7312  exmidfodomrlemrALT  7313  exmidaclem  7322  elni2  7429  indpi  7457  distrlem4prl  7699  distrlem4pru  7700  sup3exmid  9032  zdcle  9451  zdclt  9452  uzin  9683  elnn1uz2  9730  eluzdc  9733  xnn0dcle  9926  xrpnfdc  9966  xrmnfdc  9967  fztri3or  10163  fzdcel  10164  fzneuz  10225  exfzdc  10371  infssuzex  10378  qdclt  10390  fzfig  10577  fzowrddc  11103  sumdc  11702  zsumdc  11728  isum  11729  sum0  11732  fisumss  11736  isumss2  11737  fsumsplit  11751  sumsplitdc  11776  isumlessdc  11840  zproddc  11923  iprodap  11924  iprodap0  11926  prod0  11929  fprodssdc  11934  fprodsplitdc  11940  fprodsplit  11941  fprodunsn  11948  ef0lem  12004  nnwosdc  12393  prmdc  12485  pclemdc  12644  1arith  12723  ennnfonelemdc  12803  ctiunctlemudc  12841  bj-trdc  15725  bj-fadc  15727  bj-dcstab  15729  bj-nndcALT  15731  decidi  15768  decidr  15769  bj-charfunr  15783  bddc  15801  subctctexmid  15974  triap  16005  dceqnconst  16036  dcapnconst  16037  nconstwlpolem0  16039  nconstwlpo  16042  dftest  16051