Nuprl Definition : wellfounded
WellFnd{i}(A;x,y.R[x; y]) == ∀[P:A ⟶ ℙ]. ((∀j:A. ((∀k:A. (R[k; j] ⇒ P[k])) ⇒ P[j])) ⇒ {∀n:A. P[n]})
Definitions occuring in Statement :
uall: ∀[x:A]. B[x],
prop: ℙ,
guard: {T},
so_apply: x[s],
all: ∀x:A. B[x],
implies: P ⇒ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
uall: ∀[x:A]. B[x],
function: x:A ⟶ B[x],
prop: ℙ,
implies: P ⇒ Q,
guard: {T},
all: ∀x:A. B[x],
so_apply: x[s]
FDL editor aliases :
wellfounded
Latex:
WellFnd\{i\}(A;x,y.R[x; y]) ==
\mforall{}[P:A {}\mrightarrow{} \mBbbP{}]. ((\mforall{}j:A. ((\mforall{}k:A. (R[k; j] {}\mRightarrow{} P[k])) {}\mRightarrow{} P[j])) {}\mRightarrow{} \{\mforall{}n:A. P[n]\})
Date html generated:
2016_05_13-PM-03_18_09
Last ObjectModification:
2016_01_04-AM-10_27_03
Theory : well_fnd
Home
Index