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

Definition df-stab 774
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 "x = y 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 773 . 2 wff STAB 𝜑
31wn 3 . . . 4 wff ¬ 𝜑
43wn 3 . . 3 wff ¬ ¬ 𝜑
54, 1wi 4 . 2 wff (¬ ¬ 𝜑𝜑)
62, 5wb 103 1 wff (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
Colors of variables: wff set class
This definition is referenced by:  stabnot  775  dcimpstab  786  stabtestimpdc  858  ddifstab  3105  bdstab  10803
  Copyright terms: Public domain W3C validator