Definition df-dc 821

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 839, exmiddc 822, peircedc 900, or notnotrdc 829, 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 820	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 698	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 104	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  822  pm2.1dc  823  dcbid  824  dcim  827  dcn  828  notnotrdc  829  stdcndc  831  stdcndcOLD  832  stdcn  833  dcnnOLD  835  nndc  837  condcOLD  840  pm2.61ddc  847  pm5.18dc  869  pm2.13dc  871  pm2.25dc  879  pm2.85dc  891  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  peircedc  900  pm5.54dc  904  dcan  919  dcor  920  pm5.62dc  930  pm5.63dc  931  pm4.83dc  936  xordc1  1372  biassdc  1374  19.30dc  1607  nfdc  1638  exmodc  2050  moexexdc  2084  dcne  2320  eueq2dc  2861  eueq3dc  2862  abvor0dc  3391  dcun  3478  ifcldcd  3512  ifandc  3513  ifmdc  3514  exmid01  4129  exmidsssnc  4134  exmidundif  4137  exmidundifim  4138  dcextest  4503  nndceq0  4539  nndceq  6403  nndcel  6404  fidceq  6771  tridc  6801  finexdc  6804  unsnfidcex  6816  unsnfidcel  6817  undifdcss  6819  ctssdccl  7004  fodjuomnilemdc  7024  omniwomnimkv  7049  exmidonfinlem  7066  exmidfodomrlemr  7075  exmidfodomrlemrALT  7076  exmidaclem  7081  elni2  7146  indpi  7174  distrlem4prl  7416  distrlem4pru  7417  sup3exmid  8739  zdcle  9151  zdclt  9152  uzin  9382  elnn1uz2  9428  eluzdc  9431  xrpnfdc  9655  xrmnfdc  9656  fztri3or  9850  fzdcel  9851  fzneuz  9912  exfzdc  10048  fzfig  10234  sumdc  11159  zsumdc  11185  isum  11186  sum0  11189  fisumss  11193  isumss2  11194  fsumsplit  11208  sumsplitdc  11233  isumlessdc  11297  zproddc  11380  iprodap  11381  iprodap0  11383  ef0lem  11403  infssuzex  11678  ennnfonelemdc  11948  ctiunctlemudc  11986  bj-trdc  13130  bj-fadc  13131  bj-dcstab  13132  bj-nndcALT  13134  decidi  13173  decidr  13174  bddc  13197  exmid1stab  13368  subctctexmid  13369  triap  13399  dceqnconst  13423  dftest  13432