ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-stab Unicode 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  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 773 . 2  wff STAB  ph
31wn 3 . . . 4  wff  -.  ph
43wn 3 . . 3  wff  -.  -.  ph
54, 1wi 4 . 2  wff  ( -. 
-.  ph  ->  ph )
62, 5wb 103 1  wff  (STAB  ph  <->  ( -.  -.  ph  ->  ph ) )
Colors of variables: wff set class
This definition is referenced by:  stbid  775  stabnot  776  imanst  777  dcimpstab  788  stabtestimpdc  860  ddifstab  3118  bdstab  11075
  Copyright terms: Public domain W3C validator