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

Definition df-dc 731
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 737, exmiddc 732, peircedc 808, or notnot2dc 739, 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 730 . 2 wff DECID φ
31wn 3 . . 3 wff ¬ φ
41, 3wo 616 . 2 wff (φ ¬ φ)
52, 4wb 98 1 wff (DECID φ ↔ (φ ¬ φ))
Colors of variables: wff set class
This definition is referenced by:  exmiddc  732  pm2.1dc  733  dcn  734  dcbii  735  dcbid  736  condc  737  notnot2dc  739  pm2.61ddc  746  pm5.18dc  765  pm2.13dc  767  dcim  772  pm2.25dc  780  pm2.85dc  799  pm5.12dc  804  pm5.14dc  805  pm5.55dc  807  peircedc  808  dftest  810  testbitestn  811  stabtestimpdc  812  pm5.54dc  815  dcan  828  dcor  829  pm5.62dc  838  pm5.63dc  839  pm4.83dc  844  xordc1  1265  biassdc  1267  19.30dc  1496  nfdc  1527  exmodc  1928  moexexdc  1962  eueq2dc  2687  eueq3dc  2688  abvor0dc  3215  nndceq0  4262  nndceq  5986  nndcel  5987  elni2  6168  distrlem4prl  6417  distrlem4pru  6418  nndc  7199  dcdc  7200  bddc  7247  bj-dcbi  7343
  Copyright terms: Public domain W3C validator