Nuprl Definition : SafeForm
SafeForm(f) ==
  Form_ind(f;
           FormVar(v)
⇒ tt;
           FormConst(c)
⇒ tt;
           FormSet(x,phi)
⇒ r.r ∧b PZF_safe(phi;[x]);
           FormEqual(l,r)
⇒ r1,r2.r1 ∧b r2;
           FormMember(e,s)
⇒ r1,r2.r1 ∧b r2;
           FormAnd(l,r)
⇒ r1,r2.r1 ∧b r2;
           FormOr(l,r)
⇒ r1,r2.r1 ∧b r2;
           FormNot(b)
⇒ r1.r1;
           FormAll(x,b)
⇒ r1.r1;
           FormExists(x,b)
⇒ r1.r1) 
Definitions occuring in Statement : 
PZF_safe: PZF_safe(phi;vs)
, 
Form_ind: Form_ind, 
cons: [a / b]
, 
nil: []
, 
band: p ∧b q
, 
btrue: tt
Definitions occuring in definition : 
Form_ind: Form_ind, 
btrue: tt
, 
PZF_safe: PZF_safe(phi;vs)
, 
cons: [a / b]
, 
nil: []
, 
band: p ∧b q
FDL editor aliases : 
SafeForm
SafeForm
Latex:
SafeForm(f)  ==
    Form\_ind(f;
                      FormVar(v){}\mRightarrow{}  tt;
                      FormConst(c){}\mRightarrow{}  tt;
                      FormSet(x,phi){}\mRightarrow{}  r.r  \mwedge{}\msubb{}  PZF\_safe(phi;[x]);
                      FormEqual(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormMember(e,s){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormAnd(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormOr(l,r){}\mRightarrow{}  r1,r2.r1  \mwedge{}\msubb{}  r2;
                      FormNot(b){}\mRightarrow{}  r1.r1;
                      FormAll(x,b){}\mRightarrow{}  r1.r1;
                      FormExists(x,b){}\mRightarrow{}  r1.r1) 
Date html generated:
2018_05_21-PM-11_36_17
Last ObjectModification:
2017_10_12-PM-02_53_37
Theory : PZF
Home
Index