Nuprl Definition : non-forking

non-forking(T;x,y.R[x; y]) ==  ∀x,y,z:T.  (R[x; y] ⇒ R[x; z] ⇒ (y = z ∈ T))


Definitions occuring in Statement :  all: ∀x:A. B[x],  implies: P ⇒ Q,  equal: s = t ∈ T
Definitions occuring in definition :  all: ∀x:A. B[x],  implies: P ⇒ Q,  equal: s = t ∈ T
FDL editor aliases :  non-forking
Latex:
non-forking(T;x,y.R[x;  y])  ==    \mforall{}x,y,z:T.    (R[x;  y]  {}\mRightarrow{}  R[x;  z]  {}\mRightarrow{}  (y  =  z))


Date html generated: 2016_05_15-PM-07_51_41
Last ObjectModification: 2015_09_23-AM-08_19_22

Theory : general


Home Index