Nuprl Definition : uniform-TI
uniform-TI(T;x,y.R[x; y];t.Q[t]) == (∀[t:T]. ((∀[s:{s:T| R[t; s]} ]. Q[s]) ⇒ Q[t])) ⇒ (∀[t:T]. Q[t])
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
set: {x:A| B[x]}
Definitions occuring in definition :
implies: P ⇒ Q,
set: {x:A| B[x]} ,
uall: ∀[x:A]. B[x]
FDL editor aliases :
uniform-TI
Latex:
uniform-TI(T;x,y.R[x; y];t.Q[t]) ==
(\mforall{}[t:T]. ((\mforall{}[s:\{s:T| R[t; s]\} ]. Q[s]) {}\mRightarrow{} Q[t])) {}\mRightarrow{} (\mforall{}[t:T]. Q[t])
Date html generated:
2016_05_13-PM-03_49_58
Last ObjectModification:
2015_09_22-PM-05_45_19
Theory : bar-induction
Home
Index