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  2911  eueq3dc  2912  abvor0dc  3447  dcun  3534  ifcldcd  3571  ifnotdc  3572  ifandc  3573  ifmdc  3575  exmid01  4199  exmidsssnc  4204  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  ontriexmidim  4522  ontri2orexmidim  4572  dcextest  4581  nndceq0  4618  nndceq  6500  nndcel  6501  fidceq  6869  tridc  6899  finexdc  6902  unsnfidcex  6919  unsnfidcel  6920  undifdcss  6922  dcfi  6980  ctssdccl  7110  nninfisollem0  7128  nninfisollemne  7129  nninfisollemeq  7130  nninfisol  7131  fodjuomnilemdc  7142  omniwomnimkv  7165  exmidonfinlem  7192  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202  exmidaclem  7207  elni2  7313  indpi  7341  distrlem4prl  7583  distrlem4pru  7584  sup3exmid  8914  zdcle  9329  zdclt  9330  uzin  9560  elnn1uz2  9607  eluzdc  9610  xnn0dcle  9802  xrpnfdc  9842  xrmnfdc  9843  fztri3or  10039  fzdcel  10040  fzneuz  10101  exfzdc  10240  fzfig  10430  sumdc  11366  zsumdc  11392  isum  11393  sum0  11396  fisumss  11400  isumss2  11401  fsumsplit  11415  sumsplitdc  11440  isumlessdc  11504  zproddc  11587  iprodap  11588  iprodap0  11590  prod0  11593  fprodssdc  11598  fprodsplitdc  11604  fprodsplit  11605  fprodunsn  11612  ef0lem  11668  infssuzex  11950  nnwosdc  12040  prmdc  12130  pclemdc  12288  1arith  12365  ennnfonelemdc  12400  ctiunctlemudc  12438  bj-trdc  14507  bj-fadc  14509  bj-dcstab  14511  bj-nndcALT  14513  decidi  14550  decidr  14551  bj-charfunr  14565  bddc  14583  subctctexmid  14753  triap  14780  dceqnconst  14810  dcapnconst  14811  nconstwlpolem0  14813  nconstwlpo  14816  dftest  14825