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  1468  dcfromcon  1469  dcfrompeirce  1470  19.30dc  1651  nfdc  1683  exmodc  2106  moexexdc  2140  dcne  2389  eueq2dc  2953  eueq3dc  2954  abvor0dc  3492  dcun  3578  ifcldcd  3617  ifnotdc  3618  ifandc  3620  ifmdc  3622  exmid01  4258  exmidsssnc  4263  exmidundif  4266  exmidundifim  4267  exmid1stab  4268  ontriexmidim  4588  ontri2orexmidim  4638  dcextest  4647  nndceq0  4684  nndceq  6608  nndcel  6609  fidceq  6992  tridc  7022  finexdc  7025  unsnfidcex  7043  unsnfidcel  7044  undifdcss  7046  dcfi  7109  ctssdccl  7239  nninfisollem0  7258  nninfisollemne  7259  nninfisollemeq  7260  nninfisol  7261  fodjuomnilemdc  7272  omniwomnimkv  7295  exmidonfinlem  7332  exmidfodomrlemr  7341  exmidfodomrlemrALT  7342  exmidaclem  7351  elni2  7462  indpi  7490  distrlem4prl  7732  distrlem4pru  7733  sup3exmid  9065  zdcle  9484  zdclt  9485  uzin  9716  elnn1uz2  9763  eluzdc  9766  xnn0dcle  9959  xrpnfdc  9999  xrmnfdc  10000  fztri3or  10196  fzdcel  10197  fzneuz  10258  exfzdc  10406  infssuzex  10413  qdclt  10425  fzfig  10612  fzowrddc  11138  sumdc  11784  zsumdc  11810  isum  11811  sum0  11814  fisumss  11818  isumss2  11819  fsumsplit  11833  sumsplitdc  11858  isumlessdc  11922  zproddc  12005  iprodap  12006  iprodap0  12008  prod0  12011  fprodssdc  12016  fprodsplitdc  12022  fprodsplit  12023  fprodunsn  12030  ef0lem  12086  nnwosdc  12475  prmdc  12567  pclemdc  12726  1arith  12805  ennnfonelemdc  12885  ctiunctlemudc  12923  bj-trdc  15888  bj-fadc  15890  bj-dcstab  15892  bj-nndcALT  15894  decidi  15931  decidr  15932  bj-charfunr  15945  bddc  15963  subctctexmid  16139  triap  16170  dceqnconst  16201  dcapnconst  16202  nconstwlpolem0  16204  nconstwlpo  16207  dftest  16216