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

Definition df-dc 805
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 823, exmiddc 806, peircedc 884, or notnotrdc 813, 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 804 . 2 wff DECID 𝜑
31wn 3 . . 3 wff ¬ 𝜑
41, 3wo 682 . 2 wff (𝜑 ∨ ¬ 𝜑)
52, 4wb 104 1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
Colors of variables: wff set class
This definition is referenced by:  exmiddc  806  pm2.1dc  807  dcbid  808  dcim  811  dcn  812  notnotrdc  813  stdcndc  815  stdcndcOLD  816  stdcn  817  dcnnOLD  819  nndc  821  condcOLD  824  pm2.61ddc  831  pm5.18dc  853  pm2.13dc  855  pm2.25dc  863  pm2.85dc  875  pm5.12dc  880  pm5.14dc  881  pm5.55dc  883  peircedc  884  pm5.54dc  888  dcan  903  dcor  904  pm5.62dc  914  pm5.63dc  915  pm4.83dc  920  xordc1  1356  biassdc  1358  19.30dc  1591  nfdc  1622  exmodc  2027  moexexdc  2061  dcne  2296  eueq2dc  2830  eueq3dc  2831  abvor0dc  3356  dcun  3443  ifcldcd  3477  ifandc  3478  ifmdc  3479  exmid01  4091  exmidsssnc  4096  exmidundif  4099  exmidundifim  4100  dcextest  4465  nndceq0  4501  nndceq  6363  nndcel  6364  fidceq  6731  tridc  6761  finexdc  6764  unsnfidcex  6776  unsnfidcel  6777  undifdcss  6779  ctssdccl  6964  fodjuomnilemdc  6984  exmidonfinlem  7017  exmidfodomrlemr  7026  exmidfodomrlemrALT  7027  exmidaclem  7032  elni2  7090  indpi  7118  distrlem4prl  7360  distrlem4pru  7361  sup3exmid  8679  zdcle  9085  zdclt  9086  uzin  9314  elnn1uz2  9357  eluzdc  9360  xrpnfdc  9580  xrmnfdc  9581  fztri3or  9774  fzdcel  9775  fzneuz  9836  exfzdc  9972  fzfig  10158  sumdc  11082  zsumdc  11108  isum  11109  sum0  11112  fisumss  11116  isumss2  11117  fsumsplit  11131  sumsplitdc  11156  isumlessdc  11220  ef0lem  11280  infssuzex  11554  ennnfonelemdc  11823  ctiunctlemudc  11861  bj-trdc  12855  bj-fadc  12856  bj-dcstab  12857  bj-nndcALT  12859  decidi  12898  decidr  12899  bddc  12922  exmid1stab  13091  subctctexmid  13092  triap  13120  dftest  13136
  Copyright terms: Public domain W3C validator