Definition df-dc 820

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 838, exmiddc 821, peircedc 899, or notnotrdc 828, 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 819	. 2 wff DECID 𝜑
3	1	wn 3	. . 3 wff ¬ 𝜑
4	1, 3	wo 697	. 2 wff (𝜑 ∨ ¬ 𝜑)
5	2, 4	wb 104	1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

This definition is referenced by:  exmiddc  821  pm2.1dc  822  dcbid  823  dcim  826  dcn  827  notnotrdc  828  stdcndc  830  stdcndcOLD  831  stdcn  832  dcnnOLD  834  nndc  836  condcOLD  839  pm2.61ddc  846  pm5.18dc  868  pm2.13dc  870  pm2.25dc  878  pm2.85dc  890  pm5.12dc  895  pm5.14dc  896  pm5.55dc  898  peircedc  899  pm5.54dc  903  dcan  918  dcor  919  pm5.62dc  929  pm5.63dc  930  pm4.83dc  935  xordc1  1371  biassdc  1373  19.30dc  1606  nfdc  1637  exmodc  2049  moexexdc  2083  dcne  2319  eueq2dc  2857  eueq3dc  2858  abvor0dc  3386  dcun  3473  ifcldcd  3507  ifandc  3508  ifmdc  3509  exmid01  4121  exmidsssnc  4126  exmidundif  4129  exmidundifim  4130  dcextest  4495  nndceq0  4531  nndceq  6395  nndcel  6396  fidceq  6763  tridc  6793  finexdc  6796  unsnfidcex  6808  unsnfidcel  6809  undifdcss  6811  ctssdccl  6996  fodjuomnilemdc  7016  exmidonfinlem  7049  exmidfodomrlemr  7058  exmidfodomrlemrALT  7059  exmidaclem  7064  elni2  7122  indpi  7150  distrlem4prl  7392  distrlem4pru  7393  sup3exmid  8715  zdcle  9127  zdclt  9128  uzin  9358  elnn1uz2  9401  eluzdc  9404  xrpnfdc  9625  xrmnfdc  9626  fztri3or  9819  fzdcel  9820  fzneuz  9881  exfzdc  10017  fzfig  10203  sumdc  11127  zsumdc  11153  isum  11154  sum0  11157  fisumss  11161  isumss2  11162  fsumsplit  11176  sumsplitdc  11201  isumlessdc  11265  ef0lem  11366  infssuzex  11642  ennnfonelemdc  11912  ctiunctlemudc  11950  bj-trdc  12959  bj-fadc  12960  bj-dcstab  12961  bj-nndcALT  12963  decidi  13002  decidr  13003  bddc  13026  exmid1stab  13195  subctctexmid  13196  triap  13224  dftest  13241