Nuprl Definition : TI

TI is the principle of "transfinite induction" for the
given relation R on type T.
Unfortunately, it is well-formed only when Q[t] is a proposition
on type T, so it can't be used to prove that some Q' is a proposition.⋅

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 : all: ∀x:A. B[x], implies: P ⇒ Q, set: {x:A| B[x]}
Definitions occuring in definition : implies: P ⇒ Q, set: {x:A| B[x]} , all: ∀x:A. B[x]
FDL editor aliases : TI

Latex:
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_07_08-PM-04_47_11 Last ObjectModification: 2015_09_22-PM-05_45_19 Theory : bar-induction Home Index