ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dc GIF version

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
StepHypRef Expression
1 wph . . 3 wff 𝜑
21wdc 819 . 2 wff DECID 𝜑
31wn 3 . . 3 wff ¬ 𝜑
41, 3wo 697 . 2 wff (𝜑 ∨ ¬ 𝜑)
52, 4wb 104 1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
Colors of variables: wff set class
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  omniwomnimkv  7039  exmidonfinlem  7054  exmidfodomrlemr  7063  exmidfodomrlemrALT  7064  exmidaclem  7069  elni2  7134  indpi  7162  distrlem4prl  7404  distrlem4pru  7405  sup3exmid  8727  zdcle  9139  zdclt  9140  uzin  9370  elnn1uz2  9413  eluzdc  9416  xrpnfdc  9637  xrmnfdc  9638  fztri3or  9831  fzdcel  9832  fzneuz  9893  exfzdc  10029  fzfig  10215  sumdc  11139  zsumdc  11165  isum  11166  sum0  11169  fisumss  11173  isumss2  11174  fsumsplit  11188  sumsplitdc  11213  isumlessdc  11277  ef0lem  11378  infssuzex  11653  ennnfonelemdc  11923  ctiunctlemudc  11961  bj-trdc  13018  bj-fadc  13019  bj-dcstab  13020  bj-nndcALT  13022  decidi  13061  decidr  13062  bddc  13085  exmid1stab  13254  subctctexmid  13255  triap  13285  dftest  13307
  Copyright terms: Public domain W3C validator