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

Definition df-dc 754
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 760, exmiddc 755, peircedc 831, or notnotrdc 762, 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 753 . 2  wff DECID  ph
31wn 3 . . 3  wff  -.  ph
41, 3wo 639 . 2  wff  ( ph  \/  -.  ph )
52, 4wb 102 1  wff  (DECID  ph  <->  ( ph  \/  -.  ph ) )
Colors of variables: wff set class
This definition is referenced by:  exmiddc  755  pm2.1dc  756  dcn  757  dcbii  758  dcbid  759  condc  760  notnotrdc  762  pm2.61ddc  769  pm5.18dc  788  pm2.13dc  790  dcim  795  pm2.25dc  803  pm2.85dc  822  pm5.12dc  827  pm5.14dc  828  pm5.55dc  830  peircedc  831  dftest  833  testbitestn  834  stabtestimpdc  835  pm5.54dc  838  dcan  853  dcor  854  pm5.62dc  863  pm5.63dc  864  pm4.83dc  869  xordc1  1300  biassdc  1302  19.30dc  1534  nfdc  1565  exmodc  1966  moexexdc  2000  dcne  2231  eueq2dc  2736  eueq3dc  2737  abvor0dc  3269  ifcldcd  3385  nndceq0  4366  nndceq  6107  nndcel  6108  nndifsnid  6110  fidceq  6360  fidifsnid  6362  elni2  6469  indpi  6497  distrlem4prl  6739  distrlem4pru  6740  zdcle  8374  zdclt  8375  uzin  8600  elnn1uz2  8640  eluzdc  8643  fztri3or  9004  fzdcel  9005  fzneuz  9064  fzfig  9369  expival  9421  nndc  10266  dcdc  10267  bddc  10314  bj-dcbi  10414
  Copyright terms: Public domain W3C validator