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

Definition df-dc 821
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 839, exmiddc 822, peircedc 900, or notnotrdc 829, 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 820 . 2  wff DECID  ph
31wn 3 . . 3  wff  -.  ph
41, 3wo 698 . 2  wff  ( ph  \/  -.  ph )
52, 4wb 104 1  wff  (DECID  ph  <->  ( ph  \/  -.  ph ) )
Colors of variables: wff set class
This definition is referenced by:  exmiddc  822  pm2.1dc  823  dcbid  824  dcim  827  dcn  828  notnotrdc  829  stdcndc  831  stdcndcOLD  832  stdcn  833  dcnnOLD  835  nndc  837  condcOLD  840  pm2.61ddc  847  pm5.18dc  869  pm2.13dc  871  pm2.25dc  879  pm2.85dc  891  pm5.12dc  896  pm5.14dc  897  pm5.55dc  899  peircedc  900  pm5.54dc  904  dcan  919  dcor  920  pm5.62dc  930  pm5.63dc  931  pm4.83dc  936  xordc1  1372  biassdc  1374  19.30dc  1607  nfdc  1638  exmodc  2050  moexexdc  2084  dcne  2320  eueq2dc  2858  eueq3dc  2859  abvor0dc  3387  dcun  3474  ifcldcd  3508  ifandc  3509  ifmdc  3510  exmid01  4125  exmidsssnc  4130  exmidundif  4133  exmidundifim  4134  dcextest  4499  nndceq0  4535  nndceq  6399  nndcel  6400  fidceq  6767  tridc  6797  finexdc  6800  unsnfidcex  6812  unsnfidcel  6813  undifdcss  6815  ctssdccl  7000  fodjuomnilemdc  7020  omniwomnimkv  7045  exmidonfinlem  7062  exmidfodomrlemr  7071  exmidfodomrlemrALT  7072  exmidaclem  7077  elni2  7142  indpi  7170  distrlem4prl  7412  distrlem4pru  7413  sup3exmid  8735  zdcle  9147  zdclt  9148  uzin  9378  elnn1uz2  9424  eluzdc  9427  xrpnfdc  9651  xrmnfdc  9652  fztri3or  9846  fzdcel  9847  fzneuz  9908  exfzdc  10044  fzfig  10230  sumdc  11155  zsumdc  11181  isum  11182  sum0  11185  fisumss  11189  isumss2  11190  fsumsplit  11204  sumsplitdc  11229  isumlessdc  11293  ef0lem  11394  infssuzex  11669  ennnfonelemdc  11939  ctiunctlemudc  11977  bj-trdc  13113  bj-fadc  13114  bj-dcstab  13115  bj-nndcALT  13117  decidi  13156  decidr  13157  bddc  13180  exmid1stab  13351  subctctexmid  13352  triap  13382  dcapncf  13406  dftest  13415
  Copyright terms: Public domain W3C validator