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

Definition df-dc 779
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 785, exmiddc 780, peircedc 856, or notnotrdc 787, 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 778 . 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  780  pm2.1dc  781  dcn  782  dcbii  783  dcbid  784  condc  785  notnotrdc  787  pm2.61ddc  794  pm5.18dc  813  pm2.13dc  815  dcim  820  pm2.25dc  828  pm2.85dc  847  pm5.12dc  852  pm5.14dc  853  pm5.55dc  855  peircedc  856  dftest  858  testbitestn  859  stabtestimpdc  860  pm5.54dc  863  dcan  878  dcor  879  pm5.62dc  889  pm5.63dc  890  pm4.83dc  895  xordc1  1327  biassdc  1329  19.30dc  1561  nfdc  1592  exmodc  1995  moexexdc  2029  dcne  2262  eueq2dc  2779  eueq3dc  2780  abvor0dc  3295  ifcldcd  3412  ifandc  3413  ifmdc  3414  exmid01  4008  exmidundif  4011  nndceq0  4406  nndceq  6216  nndcel  6217  fidceq  6539  tridc  6569  finexdc  6572  unsnfidcex  6584  unsnfidcel  6585  undifdcss  6587  fodjuomnilemdc  6746  exmidfodomrlemr  6775  exmidfodomrlemrALT  6776  elni2  6820  indpi  6848  distrlem4prl  7090  distrlem4pru  7091  zdcle  8759  zdclt  8760  uzin  8986  elnn1uz2  9029  eluzdc  9032  fztri3or  9388  fzdcel  9389  fzneuz  9448  exfzdc  9582  fzfig  9768  expival  9859  sumdc  10642  zisum  10668  iisum  10669  sum0  10671  fisumss  10675  isumss2  10676  fsumsplit  10689  infssuzex  10851  nndc  11130  dcdc  11131  decidi  11164  decidr  11165  bddc  11188  bj-dcbi  11288
  Copyright terms: Public domain W3C validator