3
$\begingroup$

Now that Holmes had proven the consistency of adding Extensionality to Stratified Comprehension (i.e. $\sf NF$), a question along the same vein presents itself:

Is Aczel's Extensionality axiom consistent with $\sf ML$?

In $\sf ML$ we can phrase Aczel's Extensionality as: any sets whose transitive closures are isomorphic on membership, are equal.

$\endgroup$
8
  • $\begingroup$ To be clear: you intend the axiom Aczel calls “$AFA_2$” in his book, stating that every graph has at most one decoration? $\endgroup$ Commented Sep 8 at 21:04
  • $\begingroup$ @PeterLeFanuLumsdaine, yes! $\endgroup$ Commented Sep 8 at 21:41
  • $\begingroup$ This might be sensitive to how you define transitive closure. In $\mathsf{NF}$, for instance, there's going to be a least transitive set containing any given set $X$ (obtained by taking the intersection of all transitive sets $Y \supseteq X$), but there might be definable transitive subclasses of this set containing $X$. In principle one might define the strong extensionality axiom using a more restrictive definition of transitive closure that isn't actually a set. $\endgroup$ Commented Sep 9 at 0:01
  • $\begingroup$ In any case, a place to look would be Thomas Forster's book Set Theory with a Universal Set, which has some discussion of strong extensionality axioms in $\mathsf{NF}$. $\endgroup$ Commented Sep 9 at 0:04
  • $\begingroup$ Actually now that I think about it that argument doesn't even establish the existence of transitive closures because the definition of transitivity isn't stratified. $\endgroup$ Commented Sep 9 at 2:58

0

You must log in to answer this question.

Browse other questions tagged .