Definition df-dc 843

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 861, exmiddc 844, peircedc 922, or notnotrdc 851, 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 842	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 716	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  844  pm2.1dc  845  dcbid  846  dcim  849  dcn  850  notnotrdc  851  stdcndc  853  stdcndcOLD  854  stdcn  855  dcnnOLD  857  nndc  859  condcOLD  862  pm2.61ddc  869  pm5.18dc  891  pm2.13dc  893  pm2.25dc  901  pm2.85dc  913  pm5.12dc  918  pm5.14dc  919  pm5.55dc  921  peircedc  922  pm5.54dc  926  dcand  941  dcor  944  pm5.62dc  954  pm5.63dc  955  pm4.83dc  960  ifpdc  988  xordc1  1438  biassdc  1440  dcfromnotnotr  1493  dcfromcon  1494  dcfrompeirce  1495  19.30dc  1676  nfdc  1707  exmodc  2133  moexexdc  2167  dcne  2425  eueq2dc  2993  eueq3dc  2994  abvor0dc  3536  dcun  3623  ifcldcd  3664  ifnotdc  3665  ifandc  3667  ifmdc  3669  ifeqeqxdc  3673  exmid01  4316  exmidsssnc  4321  exmidundif  4324  exmidundifim  4325  exmid1stab  4326  ontriexmidim  4649  ontri2orexmidim  4699  dcextest  4708  nndceq0  4745  nndceq  6745  nndcel  6746  fidceq  7137  fidcen  7169  tridc  7170  finexdc  7173  elssdc  7175  eqsndc  7176  unsnfidcex  7193  unsnfidcel  7194  undifdcss  7196  exmidssfi  7212  fissfi  7229  dcfi  7281  ctssdccl  7415  nninfisollem0  7434  nninfisollemne  7435  nninfisollemeq  7436  nninfisol  7437  fodjuomnilemdc  7448  omniwomnimkv  7471  exmidonfinlem  7509  exmidfodomrlemr  7518  exmidfodomrlemrALT  7519  exmidaclem  7528  elni2  7645  indpi  7673  distrlem4prl  7915  distrlem4pru  7916  sup3exmid  9248  zdcle  9671  zdclt  9672  uzin  9905  elnn1uz2  9957  eluzdc  9960  xnn0dcle  10154  xrpnfdc  10194  xrmnfdc  10195  fztri3or  10393  fzdcel  10394  fzneuz  10457  exfzdc  10608  infssuzex  10615  qdclt  10629  fzfig  10816  fzowrddc  11364  sumdc  12068  zsumdc  12095  isum  12096  sum0  12099  fisumss  12103  isumss2  12104  fsumsplit  12118  sumsplitdc  12143  isumlessdc  12207  zproddc  12290  iprodap  12291  iprodap0  12293  prod0  12296  fprodssdc  12301  fprodsplitdc  12307  fprodsplit  12308  fprodunsn  12315  ef0lem  12371  nnwosdc  12760  prmdc  12852  pclemdc  13011  1arith  13090  ballotfilemcdc  13167  ennnfonelemdc  13234  ctiunctlemudc  13272  1loopgruspgr  16424  eupth2lem3lem4fi  16594  bj-trdc  16650  bj-fadc  16652  bj-dcstab  16654  bj-nndcALT  16656  decidi  16693  decidr  16694  bj-charfunr  16706  bddc  16724  subctctexmid  16900  triap  16939  dceqnconst  16972  dcapnconst  16973  nconstwlpolem0  16975  nconstwlpo  16978  dftest  16987