Nuprl Definition : inductive-set

If bdd witnesses ⌜Bounded(A,a.R[A;a])⌝ then
for _,S,B,_ = bdd, B is a bound on the "cardinality" of the A's
and ⌜λA.(fst((S A)))⌝ is the set {a | R[A;a]}.

For any set x, the set ⌜closure-set(B;λA.(fst((S A)));x)⌝ will contain
all the sets a for which R[A;a] for some ⌜(A ⊆ x)⌝.

So, the set defined inductively by R is the closure of the
function ⌜λx.closure-set(B;λA.(fst((S A)));x)⌝.

This is proved in Error :inductive-set-property.⋅

inductive-set(bdd) == let _,S,B,_ = bdd in least-closed-set(B;λx.closure-set(B;λz.(fst((S z)));x))

Definitions occuring in Statement : closure-set: closure-set(B;Y;x), least-closed-set: least-closed-set(B;G), spreadn: spread4, pi1: fst(t), apply: f a, lambda: λx.A[x]
Definitions occuring in definition : spreadn: spread4, least-closed-set: least-closed-set(B;G), closure-set: closure-set(B;Y;x), lambda: λx.A[x], pi1: fst(t), apply: f a
FDL editor aliases : inductive-set

Latex:
inductive-set(bdd) == let $_{}$,S,B,$_{}$ = bdd in least-cl\000Cosed-set(B;\mlambda{}x.closure-set(B;\mlambda{}z.(fst((S z)));x)) Date html generated: 2018_07_29-AM-10_10_14 Last ObjectModification: 2018_05_30-PM-06_48_46 Theory : constructive!set!theory Home Index