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

Definition df-stab 799
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  x  =  y corresponds to " x  =  y is stable".

(Contributed by David A. Wheeler, 13-Aug-2018.)

Assertion
Ref Expression
df-stab  |-  (STAB  ph  <->  ( -.  -.  ph  ->  ph ) )

Detailed syntax breakdown of Definition df-stab
StepHypRef Expression
1 wph . . 3  wff  ph
21wstab 798 . 2  wff STAB  ph
31wn 3 . . . 4  wff  -.  ph
43wn 3 . . 3  wff  -.  -.  ph
54, 1wi 4 . 2  wff  ( -. 
-.  ph  ->  ph )
62, 5wb 104 1  wff  (STAB  ph  <->  ( -.  -.  ph  ->  ph ) )
Colors of variables: wff set class
This definition is referenced by:  stbid  800  stabnot  801  dcstab  812  stdcndc  813  stdcndcOLD  814  stdcn  815  const  820  imanst  856  ddifstab  3176  cnstab  8369  bj-trst  12753  bj-fast  12754  bj-nnbist  12755  bj-stim  12756  bj-stan  12757  bj-stand  12758  bj-stal  12759  bj-pm2.18st  12760  bdstab  12827  exmid1stab  12997  subctctexmid  12998
  Copyright terms: Public domain W3C validator