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

Definition df-dc 742
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 748, exmiddc 743, peircedc 819, or notnot2dc 750, 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 φ ↔ (φ ¬ φ))

Detailed syntax breakdown of Definition df-dc
StepHypRef Expression
1 wph . . 3 wff φ
21wdc 741 . 2 wff DECID φ
31wn 3 . . 3 wff ¬ φ
41, 3wo 628 . 2 wff (φ ¬ φ)
52, 4wb 98 1 wff (DECID φ ↔ (φ ¬ φ))
Colors of variables: wff set class
This definition is referenced by:  exmiddc  743  pm2.1dc  744  dcn  745  dcbii  746  dcbid  747  condc  748  notnot2dc  750  pm2.61ddc  757  pm5.18dc  776  pm2.13dc  778  dcim  783  pm2.25dc  791  pm2.85dc  810  pm5.12dc  815  pm5.14dc  816  pm5.55dc  818  peircedc  819  dftest  821  testbitestn  822  stabtestimpdc  823  pm5.54dc  826  dcan  841  dcor  842  pm5.62dc  851  pm5.63dc  852  pm4.83dc  857  xordc1  1281  biassdc  1283  19.30dc  1515  nfdc  1546  exmodc  1947  moexexdc  1981  dcne  2211  eueq2dc  2708  eueq3dc  2709  abvor0dc  3236  nndceq0  4282  nndceq  6015  nndcel  6016  elni2  6298  indpi  6326  distrlem4prl  6558  distrlem4pru  6559  zdcle  8053  zdclt  8054  uzin  8241  elnn1uz2  8280  eluzdc  8283  fztri3or  8633  fzdcel  8634  fzneuz  8693  fzfig  8847  expival  8871  nndc  9169  dcdc  9170  bddc  9217  bj-dcbi  9313
  Copyright terms: Public domain W3C validator