Definition df-dc 842

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 860, exmiddc 843, peircedc 921, or notnotrdc 850, 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 841	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 715	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  843  pm2.1dc  844  dcbid  845  dcim  848  dcn  849  notnotrdc  850  stdcndc  852  stdcndcOLD  853  stdcn  854  dcnnOLD  856  nndc  858  condcOLD  861  pm2.61ddc  868  pm5.18dc  890  pm2.13dc  892  pm2.25dc  900  pm2.85dc  912  pm5.12dc  917  pm5.14dc  918  pm5.55dc  920  peircedc  921  pm5.54dc  925  dcand  940  dcor  943  pm5.62dc  953  pm5.63dc  954  pm4.83dc  959  ifpdc  987  xordc1  1437  biassdc  1439  dcfromnotnotr  1492  dcfromcon  1493  dcfrompeirce  1494  19.30dc  1675  nfdc  1707  exmodc  2130  moexexdc  2164  dcne  2413  eueq2dc  2979  eueq3dc  2980  abvor0dc  3518  dcun  3604  ifcldcd  3643  ifnotdc  3644  ifandc  3646  ifmdc  3648  exmid01  4288  exmidsssnc  4293  exmidundif  4296  exmidundifim  4297  exmid1stab  4298  ontriexmidim  4620  ontri2orexmidim  4670  dcextest  4679  nndceq0  4716  nndceq  6667  nndcel  6668  fidceq  7056  fidcen  7088  tridc  7089  finexdc  7092  elssdc  7094  eqsndc  7095  unsnfidcex  7112  unsnfidcel  7113  undifdcss  7115  exmidssfi  7131  dcfi  7180  ctssdccl  7310  nninfisollem0  7329  nninfisollemne  7330  nninfisollemeq  7331  nninfisol  7332  fodjuomnilemdc  7343  omniwomnimkv  7366  exmidonfinlem  7404  exmidfodomrlemr  7413  exmidfodomrlemrALT  7414  exmidaclem  7423  elni2  7534  indpi  7562  distrlem4prl  7804  distrlem4pru  7805  sup3exmid  9137  zdcle  9556  zdclt  9557  uzin  9789  elnn1uz2  9841  eluzdc  9844  xnn0dcle  10037  xrpnfdc  10077  xrmnfdc  10078  fztri3or  10274  fzdcel  10275  fzneuz  10336  exfzdc  10486  infssuzex  10493  qdclt  10505  fzfig  10692  fzowrddc  11228  sumdc  11919  zsumdc  11946  isum  11947  sum0  11950  fisumss  11954  isumss2  11955  fsumsplit  11969  sumsplitdc  11994  isumlessdc  12058  zproddc  12141  iprodap  12142  iprodap0  12144  prod0  12147  fprodssdc  12152  fprodsplitdc  12158  fprodsplit  12159  fprodunsn  12166  ef0lem  12222  nnwosdc  12611  prmdc  12703  pclemdc  12862  1arith  12941  ennnfonelemdc  13021  ctiunctlemudc  13059  1loopgruspgr  16156  bj-trdc  16351  bj-fadc  16353  bj-dcstab  16355  bj-nndcALT  16357  decidi  16394  decidr  16395  bj-charfunr  16408  bddc  16426  subctctexmid  16604  triap  16636  dceqnconst  16667  dcapnconst  16668  nconstwlpolem0  16670  nconstwlpo  16673  dftest  16692