Definition df-dc 840

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 858, exmiddc 841, peircedc 919, or notnotrdc 848, 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 839	. 2 wff DECID ph
3	1	wn 3	. . 3 wff -. ph
4	1, 3	wo 713	. 2 wff ( ph \/ -. ph )
5	2, 4	wb 105	1 wff (DECID ph <-> ( ph \/ -. ph ) )

This definition is referenced by:  exmiddc  841  pm2.1dc  842  dcbid  843  dcim  846  dcn  847  notnotrdc  848  stdcndc  850  stdcndcOLD  851  stdcn  852  dcnnOLD  854  nndc  856  condcOLD  859  pm2.61ddc  866  pm5.18dc  888  pm2.13dc  890  pm2.25dc  898  pm2.85dc  910  pm5.12dc  915  pm5.14dc  916  pm5.55dc  918  peircedc  919  pm5.54dc  923  dcand  938  dcor  941  pm5.62dc  951  pm5.63dc  952  pm4.83dc  957  ifpdc  985  xordc1  1435  biassdc  1437  dcfromnotnotr  1490  dcfromcon  1491  dcfrompeirce  1492  19.30dc  1673  nfdc  1705  exmodc  2128  moexexdc  2162  dcne  2411  eueq2dc  2976  eueq3dc  2977  abvor0dc  3515  dcun  3601  ifcldcd  3640  ifnotdc  3641  ifandc  3643  ifmdc  3645  exmid01  4282  exmidsssnc  4287  exmidundif  4290  exmidundifim  4291  exmid1stab  4292  ontriexmidim  4614  ontri2orexmidim  4664  dcextest  4673  nndceq0  4710  nndceq  6645  nndcel  6646  fidceq  7031  tridc  7061  finexdc  7064  unsnfidcex  7082  unsnfidcel  7083  undifdcss  7085  dcfi  7148  ctssdccl  7278  nninfisollem0  7297  nninfisollemne  7298  nninfisollemeq  7299  nninfisol  7300  fodjuomnilemdc  7311  omniwomnimkv  7334  exmidonfinlem  7371  exmidfodomrlemr  7380  exmidfodomrlemrALT  7381  exmidaclem  7390  elni2  7501  indpi  7529  distrlem4prl  7771  distrlem4pru  7772  sup3exmid  9104  zdcle  9523  zdclt  9524  uzin  9755  elnn1uz2  9802  eluzdc  9805  xnn0dcle  9998  xrpnfdc  10038  xrmnfdc  10039  fztri3or  10235  fzdcel  10236  fzneuz  10297  exfzdc  10446  infssuzex  10453  qdclt  10465  fzfig  10652  fzowrddc  11179  sumdc  11869  zsumdc  11895  isum  11896  sum0  11899  fisumss  11903  isumss2  11904  fsumsplit  11918  sumsplitdc  11943  isumlessdc  12007  zproddc  12090  iprodap  12091  iprodap0  12093  prod0  12096  fprodssdc  12101  fprodsplitdc  12107  fprodsplit  12108  fprodunsn  12115  ef0lem  12171  nnwosdc  12560  prmdc  12652  pclemdc  12811  1arith  12890  ennnfonelemdc  12970  ctiunctlemudc  13008  bj-trdc  16116  bj-fadc  16118  bj-dcstab  16120  bj-nndcALT  16122  decidi  16159  decidr  16160  bj-charfunr  16173  bddc  16191  subctctexmid  16366  triap  16397  dceqnconst  16428  dcapnconst  16429  nconstwlpolem0  16431  nconstwlpo  16434  dftest  16443