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  1467  dcfromcon  1468  dcfrompeirce  1469  19.30dc  1650  nfdc  1682  exmodc  2104  moexexdc  2138  dcne  2387  eueq2dc  2946  eueq3dc  2947  abvor0dc  3484  dcun  3570  ifcldcd  3608  ifnotdc  3609  ifandc  3610  ifmdc  3612  exmid01  4242  exmidsssnc  4247  exmidundif  4250  exmidundifim  4251  exmid1stab  4252  ontriexmidim  4570  ontri2orexmidim  4620  dcextest  4629  nndceq0  4666  nndceq  6585  nndcel  6586  fidceq  6966  tridc  6996  finexdc  6999  unsnfidcex  7017  unsnfidcel  7018  undifdcss  7020  dcfi  7083  ctssdccl  7213  nninfisollem0  7232  nninfisollemne  7233  nninfisollemeq  7234  nninfisol  7235  fodjuomnilemdc  7246  omniwomnimkv  7269  exmidonfinlem  7301  exmidfodomrlemr  7310  exmidfodomrlemrALT  7311  exmidaclem  7320  elni2  7427  indpi  7455  distrlem4prl  7697  distrlem4pru  7698  sup3exmid  9030  zdcle  9449  zdclt  9450  uzin  9681  elnn1uz2  9728  eluzdc  9731  xnn0dcle  9924  xrpnfdc  9964  xrmnfdc  9965  fztri3or  10161  fzdcel  10162  fzneuz  10223  exfzdc  10369  infssuzex  10376  qdclt  10388  fzfig  10575  fzowrddc  11100  sumdc  11669  zsumdc  11695  isum  11696  sum0  11699  fisumss  11703  isumss2  11704  fsumsplit  11718  sumsplitdc  11743  isumlessdc  11807  zproddc  11890  iprodap  11891  iprodap0  11893  prod0  11896  fprodssdc  11901  fprodsplitdc  11907  fprodsplit  11908  fprodunsn  11915  ef0lem  11971  nnwosdc  12360  prmdc  12452  pclemdc  12611  1arith  12690  ennnfonelemdc  12770  ctiunctlemudc  12808  bj-trdc  15688  bj-fadc  15690  bj-dcstab  15692  bj-nndcALT  15694  decidi  15731  decidr  15732  bj-charfunr  15746  bddc  15764  subctctexmid  15937  triap  15968  dceqnconst  15999  dcapnconst  16000  nconstwlpolem0  16002  nconstwlpo  16005  dftest  16014