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 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 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 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

Detailed syntax breakdown of Definition df-dc

Step	Hyp	Ref	Expression
1		wph	. . 3 wff 𝜑
2	1	wdc 834	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 708	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 105	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

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  2912  eueq3dc  2913  abvor0dc  3448  dcun  3535  ifcldcd  3572  ifnotdc  3573  ifandc  3574  ifmdc  3576  exmid01  4200  exmidsssnc  4205  exmidundif  4208  exmidundifim  4209  exmid1stab  4210  ontriexmidim  4523  ontri2orexmidim  4573  dcextest  4582  nndceq0  4619  nndceq  6502  nndcel  6503  fidceq  6871  tridc  6901  finexdc  6904  unsnfidcex  6921  unsnfidcel  6922  undifdcss  6924  dcfi  6982  ctssdccl  7112  nninfisollem0  7130  nninfisollemne  7131  nninfisollemeq  7132  nninfisol  7133  fodjuomnilemdc  7144  omniwomnimkv  7167  exmidonfinlem  7194  exmidfodomrlemr  7203  exmidfodomrlemrALT  7204  exmidaclem  7209  elni2  7315  indpi  7343  distrlem4prl  7585  distrlem4pru  7586  sup3exmid  8916  zdcle  9331  zdclt  9332  uzin  9562  elnn1uz2  9609  eluzdc  9612  xnn0dcle  9804  xrpnfdc  9844  xrmnfdc  9845  fztri3or  10041  fzdcel  10042  fzneuz  10103  exfzdc  10242  fzfig  10432  sumdc  11368  zsumdc  11394  isum  11395  sum0  11398  fisumss  11402  isumss2  11403  fsumsplit  11417  sumsplitdc  11442  isumlessdc  11506  zproddc  11589  iprodap  11590  iprodap0  11592  prod0  11595  fprodssdc  11600  fprodsplitdc  11606  fprodsplit  11607  fprodunsn  11614  ef0lem  11670  infssuzex  11952  nnwosdc  12042  prmdc  12132  pclemdc  12290  1arith  12367  ennnfonelemdc  12402  ctiunctlemudc  12440  bj-trdc  14543  bj-fadc  14545  bj-dcstab  14547  bj-nndcALT  14549  decidi  14586  decidr  14587  bj-charfunr  14601  bddc  14619  subctctexmid  14789  triap  14816  dceqnconst  14846  dcapnconst  14847  nconstwlpolem0  14849  nconstwlpo  14852  dftest  14861