Definition df-dc 830

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 848, exmiddc 831, peircedc 909, or notnotrdc 838, 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 829	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 703	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 104	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  831  pm2.1dc  832  dcbid  833  dcim  836  dcn  837  notnotrdc  838  stdcndc  840  stdcndcOLD  841  stdcn  842  dcnnOLD  844  nndc  846  condcOLD  849  pm2.61ddc  856  pm5.18dc  878  pm2.13dc  880  pm2.25dc  888  pm2.85dc  900  pm5.12dc  905  pm5.14dc  906  pm5.55dc  908  peircedc  909  pm5.54dc  913  dcan  928  dcor  930  pm5.62dc  940  pm5.63dc  941  pm4.83dc  946  xordc1  1388  biassdc  1390  19.30dc  1620  nfdc  1652  exmodc  2069  moexexdc  2103  dcne  2351  eueq2dc  2903  eueq3dc  2904  abvor0dc  3438  dcun  3525  ifcldcd  3561  ifnotdc  3562  ifandc  3563  ifmdc  3565  exmid01  4184  exmidsssnc  4189  exmidundif  4192  exmidundifim  4193  ontriexmidim  4506  ontri2orexmidim  4556  dcextest  4565  nndceq0  4602  nndceq  6478  nndcel  6479  fidceq  6847  tridc  6877  finexdc  6880  unsnfidcex  6897  unsnfidcel  6898  undifdcss  6900  dcfi  6958  ctssdccl  7088  nninfisollem0  7106  nninfisollemne  7107  nninfisollemeq  7108  nninfisol  7109  fodjuomnilemdc  7120  omniwomnimkv  7143  exmidonfinlem  7170  exmidfodomrlemr  7179  exmidfodomrlemrALT  7180  exmidaclem  7185  elni2  7276  indpi  7304  distrlem4prl  7546  distrlem4pru  7547  sup3exmid  8873  zdcle  9288  zdclt  9289  uzin  9519  elnn1uz2  9566  eluzdc  9569  xnn0dcle  9759  xrpnfdc  9799  xrmnfdc  9800  fztri3or  9995  fzdcel  9996  fzneuz  10057  exfzdc  10196  fzfig  10386  sumdc  11321  zsumdc  11347  isum  11348  sum0  11351  fisumss  11355  isumss2  11356  fsumsplit  11370  sumsplitdc  11395  isumlessdc  11459  zproddc  11542  iprodap  11543  iprodap0  11545  prod0  11548  fprodssdc  11553  fprodsplitdc  11559  fprodsplit  11560  fprodunsn  11567  ef0lem  11623  infssuzex  11904  nnwosdc  11994  prmdc  12084  pclemdc  12242  1arith  12319  ennnfonelemdc  12354  ctiunctlemudc  12392  bj-trdc  13787  bj-fadc  13789  bj-dcstab  13791  bj-nndcALT  13793  decidi  13830  decidr  13831  bj-charfunr  13845  bddc  13863  exmid1stab  14033  subctctexmid  14034  triap  14061  dceqnconst  14091  dcapnconst  14092  nconstwlpolem0  14094  nconstwlpo  14097  dftest  14104