ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-stab Unicode 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  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 830 . 2  wff STAB  ph
31wn 3 . . . 4  wff  -.  ph
43wn 3 . . 3  wff  -.  -.  ph
54, 1wi 4 . 2  wff  ( -. 
-.  ph  ->  ph )
62, 5wb 105 1  wff  (STAB  ph  <->  ( -.  -.  ph  ->  ph ) )
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  4207  2omotap  7255  bj-trst  14351  bj-fast  14353  bj-nnbist  14356  bj-stim  14358  bj-stan  14359  bj-stand  14360  bj-stal  14361  bj-pm2.18st  14362  bj-con1st  14363  bdstab  14439  subctctexmid  14610
  Copyright terms: Public domain W3C validator