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

Definition df-dc 777
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  x  =  y corresponds to "x = y is decidable".

We could transform intuitionistic logic to classical logic by adding unconditional forms of condc 783, exmiddc 778, peircedc 854, or notnotrdc 785, 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  ph  <->  ( ph  \/  -.  ph ) )

Detailed syntax breakdown of Definition df-dc
StepHypRef Expression
1 wph . . 3  wff  ph
21wdc 776 . 2  wff DECID  ph
31wn 3 . . 3  wff  -.  ph
41, 3wo 662 . 2  wff  ( ph  \/  -.  ph )
52, 4wb 103 1  wff  (DECID  ph  <->  ( ph  \/  -.  ph ) )
Colors of variables: wff set class
This definition is referenced by:  exmiddc  778  pm2.1dc  779  dcn  780  dcbii  781  dcbid  782  condc  783  notnotrdc  785  pm2.61ddc  792  pm5.18dc  811  pm2.13dc  813  dcim  818  pm2.25dc  826  pm2.85dc  845  pm5.12dc  850  pm5.14dc  851  pm5.55dc  853  peircedc  854  dftest  856  testbitestn  857  stabtestimpdc  858  pm5.54dc  861  dcan  876  dcor  877  pm5.62dc  887  pm5.63dc  888  pm4.83dc  893  xordc1  1325  biassdc  1327  19.30dc  1559  nfdc  1590  exmodc  1993  moexexdc  2027  dcne  2260  eueq2dc  2774  eueq3dc  2775  abvor0dc  3285  ifcldcd  3399  exmid01  3988  exmidundif  3991  nndceq0  4385  nndceq  6163  nndcel  6164  fidceq  6425  unsnfidcex  6464  unsnfidcel  6465  undifdcss  6467  elni2  6618  indpi  6646  distrlem4prl  6888  distrlem4pru  6889  zdcle  8557  zdclt  8558  uzin  8784  elnn1uz2  8827  eluzdc  8830  fztri3or  9186  fzdcel  9187  fzneuz  9246  exfzdc  9378  fzfig  9564  expival  9627  sumdc  10396  infssuzex  10552  nndc  10831  dcdc  10832  decidi  10865  decidr  10866  bddc  10886  bj-dcbi  10986
  Copyright terms: Public domain W3C validator