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

Definition df-stab 801
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 800 . 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  802  stabnot  803  dcstab  814  stdcndc  815  stdcndcOLD  816  stdcn  817  const  822  imanst  858  ddifstab  3178  cnstab  8375  bj-trst  12878  bj-fast  12879  bj-nnbist  12880  bj-stim  12881  bj-stan  12882  bj-stand  12883  bj-stal  12884  bj-pm2.18st  12885  bdstab  12952  exmid1stab  13122  subctctexmid  13123
  Copyright terms: Public domain W3C validator