Nuprl Definition : weak-TI

weak-TI(T;x,y.R[x; y];t.Q[t]) ==  (∀t:T. ((∀s:T. (R[t; s] ⇒ Q[s])) ⇒ Q[t])) ⇒ (∀t:T. Q[t])


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


Date html generated: 2016_05_13-PM-03_50_00
Last ObjectModification: 2015_09_22-PM-05_45_20

Theory : bar-induction


Home Index