Nuprl Definition : Regularset
Regular(A) is a generalization of regular(A) where the relation R
can be any extensional relation (not necessarily given by a set).
So, Regular(A) ⇒ regular(A) (see Regularset-regularset).
Aczel's "regular extension axiom" is that every set is a subset of
a regular set (in fact of a Regular set).
see Error :RegularExtension ⋅
Regular(A) ==
transitive-set(A)
∧ (∀B:Set{i:l}
((B ∈ A)
⇒ (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
(SetRelation(R) ⇒ R:(B ⇒ A) ⇒ (∃b:Set{i:l}. ((b ∈ A) ∧ R:(B ⇒ b) ∧ R:(B ─>> b)))))))
Definitions occuring in Statement :
onto-map: R:(A ─>> B),
mv-map: R:(A ⇒ B),
set-relation: SetRelation(R),
transitive-set: transitive-set(s),
setmem: (x ∈ s),
Set: Set{i:l},
prop: ℙ,
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
function: x:A ⟶ B[x]
Definitions occuring in definition :
onto-map: R:(A ─>> B),
mv-map: R:(A ⇒ B),
and: P ∧ Q,
setmem: (x ∈ s),
Set: Set{i:l},
exists: ∃x:A. B[x],
implies: P ⇒ Q,
set-relation: SetRelation(R),
prop: ℙ,
function: x:A ⟶ B[x],
all: ∀x:A. B[x],
transitive-set: transitive-set(s)
FDL editor aliases :
Regularset
Latex:
Regular(A) ==
transitive-set(A)
\mwedge{} (\mforall{}B:Set\{i:l\}
((B \mmember{} A)
{}\mRightarrow{} (\mforall{}R:Set\{i:l\} {}\mrightarrow{} Set\{i:l\} {}\mrightarrow{} \mBbbP{}'
(SetRelation(R)
{}\mRightarrow{} R:(B {}\mRightarrow{} A)
{}\mRightarrow{} (\mexists{}b:Set\{i:l\}. ((b \mmember{} A) \mwedge{} R:(B {}\mRightarrow{} b) \mwedge{} R:(B {}>> b)))))))
Date html generated:
2018_05_29-PM-01_52_40
Last ObjectModification:
2018_05_25-PM-02_13_43
Theory : constructive!set!theory
Home
Index