ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-dc GIF 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 𝑥 = 𝑦 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 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))

Detailed syntax breakdown of Definition df-dc
StepHypRef Expression
1 wph . . 3 wff 𝜑
21wdc 753 . 2 wff DECID 𝜑
31wn 3 . . 3 wff ¬ 𝜑
41, 3wo 639 . 2 wff (𝜑 ∨ ¬ 𝜑)
52, 4wb 102 1 wff (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
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  2737  eueq3dc  2738  abvor0dc  3270  ifcldcd  3386  nndceq0  4367  nndceq  6108  nndcel  6109  nndifsnid  6111  fidceq  6361  fidifsnid  6363  elni2  6470  indpi  6498  distrlem4prl  6740  distrlem4pru  6741  zdcle  8375  zdclt  8376  uzin  8601  elnn1uz2  8641  eluzdc  8644  fztri3or  9005  fzdcel  9006  fzneuz  9065  fzfig  9370  expival  9422  nndc  10287  dcdc  10288  bddc  10335  bj-dcbi  10435
  Copyright terms: Public domain W3C validator