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

Definition df-stab 816
 Description: Propositions where a double-negative can be removed are called stable. See Chapter 2 [Moschovakis] p. 2. Our notation for stability is a connective STAB which we place before the formula in question. For example, STAB 𝑥 = 𝑦 corresponds to "𝑥 = 𝑦 is stable". (Contributed by David A. Wheeler, 13-Aug-2018.)
Assertion
Ref Expression
df-stab (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))

Detailed syntax breakdown of Definition df-stab
StepHypRef Expression
1 wph . . 3 wff 𝜑
21wstab 815 . 2 wff STAB 𝜑
31wn 3 . . . 4 wff ¬ 𝜑
43wn 3 . . 3 wff ¬ ¬ 𝜑
54, 1wi 4 . 2 wff (¬ ¬ 𝜑𝜑)
62, 5wb 104 1 wff (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
 Colors of variables: wff set class This definition is referenced by:  stbid  817  stabnot  818  dcstab  829  stdcndc  830  stdcndcOLD  831  stdcn  832  const  837  imanst  873  ddifstab  3203  cnstab  8400  bj-trst  12940  bj-fast  12941  bj-nnbist  12942  bj-stim  12943  bj-stan  12944  bj-stand  12945  bj-stal  12946  bj-pm2.18st  12947  bdstab  13014  exmid1stab  13184  subctctexmid  13185
 Copyright terms: Public domain W3C validator