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  2130  moexexdc  2164  dcne  2414  eueq2dc  2980  eueq3dc  2981  abvor0dc  3520  dcun  3606  ifcldcd  3647  ifnotdc  3648  ifandc  3650  ifmdc  3652  exmid01  4294  exmidsssnc  4299  exmidundif  4302  exmidundifim  4303  exmid1stab  4304  ontriexmidim  4626  ontri2orexmidim  4676  dcextest  4685  nndceq0  4722  nndceq  6710  nndcel  6711  fidceq  7099  fidcen  7131  tridc  7132  finexdc  7135  elssdc  7137  eqsndc  7138  unsnfidcex  7155  unsnfidcel  7156  undifdcss  7158  exmidssfi  7174  dcfi  7240  ctssdccl  7370  nninfisollem0  7389  nninfisollemne  7390  nninfisollemeq  7391  nninfisol  7392  fodjuomnilemdc  7403  omniwomnimkv  7426  exmidonfinlem  7464  exmidfodomrlemr  7473  exmidfodomrlemrALT  7474  exmidaclem  7483  elni2  7594  indpi  7622  distrlem4prl  7864  distrlem4pru  7865  sup3exmid  9196  zdcle  9617  zdclt  9618  uzin  9850  elnn1uz2  9902  eluzdc  9905  xnn0dcle  10098  xrpnfdc  10138  xrmnfdc  10139  fztri3or  10336  fzdcel  10337  fzneuz  10398  exfzdc  10549  infssuzex  10556  qdclt  10568  fzfig  10755  fzowrddc  11294  sumdc  11998  zsumdc  12025  isum  12026  sum0  12029  fisumss  12033  isumss2  12034  fsumsplit  12048  sumsplitdc  12073  isumlessdc  12137  zproddc  12220  iprodap  12221  iprodap0  12223  prod0  12226  fprodssdc  12231  fprodsplitdc  12237  fprodsplit  12238  fprodunsn  12245  ef0lem  12301  nnwosdc  12690  prmdc  12782  pclemdc  12941  1arith  13020  ennnfonelemdc  13100  ctiunctlemudc  13138  1loopgruspgr  16244  eupth2lem3lem4fi  16414  bj-trdc  16470  bj-fadc  16472  bj-dcstab  16474  bj-nndcALT  16476  decidi  16513  decidr  16514  bj-charfunr  16526  bddc  16544  subctctexmid  16722  triap  16761  dceqnconst  16793  dcapnconst  16794  nconstwlpolem0  16796  nconstwlpo  16799  dftest  16818