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

Definition df-dc 743
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 749, exmiddc 744, peircedc 820, or notnotrdc 751, 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 742 . 2  wff DECID  ph
31wn 3 . . 3  wff  -.  ph
41, 3wo 629 . 2  wff  ( ph  \/  -.  ph )
52, 4wb 98 1  wff  (DECID  ph  <->  ( ph  \/  -.  ph ) )
Colors of variables: wff set class
This definition is referenced by:  exmiddc  744  pm2.1dc  745  dcn  746  dcbii  747  dcbid  748  condc  749  notnotrdc  751  pm2.61ddc  758  pm5.18dc  777  pm2.13dc  779  dcim  784  pm2.25dc  792  pm2.85dc  811  pm5.12dc  816  pm5.14dc  817  pm5.55dc  819  peircedc  820  dftest  822  testbitestn  823  stabtestimpdc  824  pm5.54dc  827  dcan  842  dcor  843  pm5.62dc  852  pm5.63dc  853  pm4.83dc  858  xordc1  1284  biassdc  1286  19.30dc  1518  nfdc  1549  exmodc  1950  moexexdc  1984  dcne  2214  eueq2dc  2711  eueq3dc  2712  abvor0dc  3239  ifcldcd  3355  nndceq0  4317  nndceq  6055  nndcel  6056  nndifsnid  6058  fidceq  6308  fidifsnid  6310  elni2  6384  indpi  6412  distrlem4prl  6654  distrlem4pru  6655  zdcle  8280  zdclt  8281  uzin  8468  elnn1uz2  8507  eluzdc  8510  fztri3or  8861  fzdcel  8862  fzneuz  8921  fzfig  9075  expival  9126  nndc  9764  dcdc  9765  bddc  9812  bj-dcbi  9912
  Copyright terms: Public domain W3C validator