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

Definition df-dc 727
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 733, exmiddc 728, peircedc 804, or notnot2dc 735, 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 726 . 2 wff DECID φ
31wn 3 . . 3 wff ¬ φ
41, 3wo 613 . 2 wff (φ ¬ φ)
52, 4wb 98 1 wff (DECID φ ↔ (φ ¬ φ))
Colors of variables: wff set class
This definition is referenced by:  exmiddc  728  pm2.1dc  729  dcn  730  dcbii  731  dcbid  732  condc  733  notnot2dc  735  pm2.61ddc  742  pm5.18dc  761  pm2.13dc  763  dcim  768  pm2.25dc  776  pm2.85dc  795  pm5.12dc  800  pm5.14dc  801  pm5.55dc  803  peircedc  804  dftest  806  testbitestn  807  stabtestimpdc  808  pm5.54dc  811  dcan  824  dcor  825  pm5.62dc  834  pm5.63dc  835  pm4.83dc  840  xordc1  1262  biassdc  1264  19.30dc  1491  nfdc  1522  exmodc  1923  moexexdc  1957  dcne  2186  eueq2dc  2682  eueq3dc  2683  abvor0dc  3210  nndceq0  4254  nndceq  5978  nndcel  5979  elni2  6160  distrlem4prl  6409  distrlem4pru  6410  nndc  8165  dcdc  8166  bddc  8213  bj-dcbi  8309
  Copyright terms: Public domain W3C validator