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

Definition df-stab 831
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 830 . 2 wff STAB 𝜑
31wn 3 . . . 4 wff ¬ 𝜑
43wn 3 . . 3 wff ¬ ¬ 𝜑
54, 1wi 4 . 2 wff (¬ ¬ 𝜑𝜑)
62, 5wb 105 1 wff (STAB 𝜑 ↔ (¬ ¬ 𝜑𝜑))
Colors of variables: wff set class
This definition is referenced by:  stbid  832  stabnot  833  dcstab  844  stdcndc  845  stdcndcOLD  846  stdcn  847  const  852  imanst  888  ddifstab  3267  exmid1stab  4208  2omotap  7257  bj-trst  14461  bj-fast  14463  bj-nnbist  14466  bj-stim  14468  bj-stan  14469  bj-stand  14470  bj-stal  14471  bj-pm2.18st  14472  bj-con1st  14473  bdstab  14549  subctctexmid  14720
  Copyright terms: Public domain W3C validator