I also don’t really have any intuition for what you can or cannot do with stratified formulas.
tailcalled
Karma: 8,245
Poorly behaved categorically. (Admittedly, so are my current drafts too.)
Category theory and similar stuff feels like the main reason you’d even want a set of all sets, so this is a big killer.
So identify a set with its directed ∈ graph? Not sure whether this makes sense.
It makes sense and has been discovered before, but it doesn’t straightforwardly support the set of all sets. Currently I’m representing sets as a term of the shape { x | \phi(x) }, and computing its directed ∈ graph is pretty hard.
Usually the category of sets has functions as morphisms, but I’m trying to build a material set theory, which should distinguish e.g. {0} and {1} despite them being in bijection with each other. One could use the subset relation as morphisms, but then it just reduces to the same definition as I gave.
I’m low-key convinced there must be a way to get “the set of all sets” and associated features to work, without sacrificing so much logic or requiring so much bookkeeping that ordinary mathematics becomes a problem. I’m using Fable for some experiments in doing so, and Fable is very good at mathematics, though it keeps coming up with obstacles.
The last obstacle I was working with is, what is equality for sets? Classically, two sets are equal if they contain the same elements. I basically need to keep that because I don’t think one can do mathematics without it, but when you have non-well-founded sets, it becomes a lot more involved.
Beyond the lexical personality traits: What is the structure of personality?
I guess to add, the thing about constructive math (which avoids excluded middle and unrestricted choice) is that it permits models where everything is computational. What I hope I’ve shown is that in some such models, the obstacle to choice really just boils down to excluded middle. (Probably—again it’s really difficult to combine mutable state with other stuff in pure math.)
I am not an expert, but I think solutions like this have a potential of hitting an infinite recursion, if evaluating some expression inside the code somehow indirectly invokes the axiom of choice, for example if you construct an object specifically for that purpose.
I don’t think you run into this problem.
My understanding of the axiom of choice, and the axioms in general, is that instead of merely describing how things work, they are describing what things are are talking about (by describing how they work). There are multiple concepts (in the Platonic realm) you could plausibly mean when you use the word “set”. The axiom of choice says “I only mean those models that have the property that for any set of sets, there is a selection that works like this, and the selection itself is included in the model of ‘sets’”. There are models that follow the remaining axioms and have the property, and also models that follow the remaining axioms and don’t have the property.
Yes, there are two places where that shows up in my comment. First, “if math allowed mutable state” is a condition on the concepts one might be referring to, as usually those concepts don’t allow mutable state. (In fact combining sets and mutable state is probably the hardest part, because e.g. what does it mean to take a subset {x \in S | phi(x) } if phi might mutate some state as a side-effect?) Secondly, my “proof” reduces the axiom of choice to excluded middle, and excluded middle is again a feature that you might or might not have in your mathematical universe.
familyis a function that witnesses the “nonemptiness” (really, mere inhabitedness) by returning an element of the propositional truncation of the set. So more formally,axiom_of_choicehas type(Πi: I. ||F(i)||) → ||Πi: I. F(i)||. The “choice” comes from the fact thatfamily(due to the propositional truncation) is allowed to return differentF(i)’s from identicali’s, whereaschoice_fnis required to choose a canonicalF(i)for eachi. (The intermediate results are untyped because this is a realizer, not a typed term in a type theory.)😅 This explanation is, I assume, not very helpful to anyone who doesn’t already know what’s going on. But basically in type theory, propositions correspond to (propositionally truncated) types, and proofs correspond to programs/terms with the types in question, so in proving the nonemptiness of the sets, you automatically end up with a witness function that picks out elements—except the witness function may be “nondeterministic” (that’s where the propositional truncation comes in), which is what requires choice to fix.
The propositional truncation is important to understand. There is a version of type theory’s logic that doesn’t include propositional truncation, but in it the axiom of choice is trivial to prove and not really of any use. Unfortunately the intuitive way to explain propositional truncation gives catastrophically wrong intuition for my use-case, as explained here: https://mathstodon.xyz/@MartinEscardo/111014413939196037
If math allowed mutable state, we could reduce the axiom of choice to excluded middle:
def axiom_of_choice(family):
cache = {}
def choice_fn(index):
if index not in cache:
cache[index] = family(index)
return cache[index]
return choice_fnThis relies on excluded middle because the ability to check whether an index is in the cache and if so look it up requires the ability to compare indices by equality.
(Sampling from family(index) is legit. The axiom of choice asserts that dependent products commute with propositional truncation. Propositional truncation does not destroy the computational content of the realizers of the family, it just quotients the realizers to be equal for when it comes to determining the well-definedness of functions. Since we use a cache, the resulting choice_fn still respects equality.
This isn’t valid type theory of course, since type theory has models that don’t permit this stuff and requires propositional truncation to be explicit.)
I think of this as a sort of converse of Diaconescu’s theorem.
This isn’t actually how the effective topos gets countable choice. Instead I believe the effective topos relies on the fact that realizers of functions out of
1. A giant asteroid is hurtling toward the planet, and will arrive very soon. If we mess up and fail to deflect the asteroid, then we all die. This is presumably a classic one-shot scenario, and perhaps few people disagree with that assessment, but I’m not sure.
Couldn’t one have multiple parallel projects to deflect it, thereby giving multiple shots? The difference with AI safety being that if there are multiple parallel projects to build a safe ASI, the fastest one is the one that determines the outcome.
I also wonder about the snowball sampling approach to this. How do people with rare diseases get to know each other? I’d assume the major way is via forums for people trying to work out their rare diseases, which probably skews towards cases that haven’t been adequately handled by the doctors.
You can pursue both goals, but you have chosen not to, and I find that alarming.
My reference to “when you’ve had interactions yourself that you could surely be much more detailed and coherent with” was meant to point the OP at something more informative for protecting vulnerable people from predators.
There are many, many concrete accusations in this post. It doesn’t particularly matter whether there is a “main” one. Vassar is a serial psychological and sexual abuser, and has caused multiple deaths. That is bad.
There was a sexual abuse allegation in the OP (“arch-rapist”). I don’t know if that allegation was among the ones you consider to be concrete, but it’s not among the ones I consider to be concrete, and the OP also dismissed her approach to sexual abuse allegations as “paranoid”, so...
Plex opening up about his experiences with this abuser was a terrifying thing to do. The appropriate response in this circumstance is to respond with empathy. If you aren’t going to do that, it is better not to say anything at all. I understand that we are on LessWrong, and this is where people usually gain status by bantering about epistemic technicalities, but there is more than one genre of post, and this is one where that general rule does not apply.
I’m not convinced, for reasons that might be clearer below.
If you want to know specific pieces of information, you can just ask about those directly without making it sound like you don’t believe him or any of Vassar’s other accusers.
The OP doesn’t even believe Vassar’s other accusers! (“Paranoid”!) Why should I fully believe them?
I have generally been assuming that this is just a case of not knowing how to respond appropriately. But if you actually don’t believe them, just say that and out yourself. Shankar already made it clear that he doesn’t care about people and he would gladly sacrifice their lives to maintain the verbal games he gets to play with his friends. Do you agree with him about that? Do you think structures that differentially protect abusers are good?
I believe that Vassar has been encouraging a worldview that others would call insanely paranoid. I believe that he’s been “pressuring” people to LSD, if by “pressuring” you mean something like “telling people to take it”. (For comparison, one time two men dragged me into a room and forced olanzapine into my mouth; that seems more extreme than telling someone to use a drug, so it seems a bit whiny to me if telling people to take LSD has been upgraded to “pressuring”. I don’t know how appropriate LSD or olanzapine is to use in either of the circumstances.) I am confused about the sexual assault allegations. I believe that people near Vassar have had psychotic breaks, and that Vassar could be a cause of that, though my own experience having a psychotic break makes me think people are making too big of a deal about that.
I also suspect the “insanely paranoid” worldview is to a substantial extent true, and that the surrounding (non-Vassarite) community is essentially abusing the people Vassar talked to by denying it. It’s not clear to me that thing like suicides aren’t better attributed to that abuse than to what Vassar has been doing. I think vague accusations help abusers to reverse the victim and offender, and that the terrifyingness of sharing the whole story may be that the whole story makes things look better for Vassar and worse for plex. (Though a complication here is that one way to become vulnerable to abuse is to be a transgressor, as one’s transgressions give opportunities for blackmail and scapegoating and so on. So abusers might target transgressors, and without protection for the transgressors, it’s hard for them to call out the abusers.)
That said, Vassar has been banned by Lightcone, and I don’t take Lightcone to be the sorts of people who’d gang up on Vassar for no good reason. Maybe I should ask @Ben Pace for more info about why he is banned.
Maybe for context: my most recent Vassar-themed experience was sharing this article with a bunch of rationalists: https://surveyanon.wordpress.com/2025/01/24/hsu-and-morandinis-fraudulent-autogynephilia-study/
They considered the article hyperbolic and told me to stop talking to Vassar.
Which at first glance is weird because the article doesn’t bring up Vassar at all, and Vassar blocked me from contacting him a while ago.But it makes sense because rationalists associate complaining about dishonesty with Vassar and his companions, because that’s something Vassar does a lot.Either way, I still think the article was reasonable, and the fact that rationalists dismiss it as Vassarite nonsense seems like a problem to me. The dissatisfaction with dishonesty might very well be the “paranoia” OP was talking about; it’s hard to tell because they were not very specific about it.
Edit: Oops, I looked at the chat logs and I did bring up Vassar as part of the conversation, so that probably contributed to being told to stop talking to him. But I think the point still stands that people associate him with complaining about dishonesty.
Do you think it is more important to dissect the way that people communicate, or to protect vulnerable people from predators?
Can you explain how these are incompatible goals?
My takeaway from this post is that an exceptionally evil man has caused significant harm to the rationalist community, leading directly to deaths and damaging the community’s ability to do extremely important work. Is that not your primary takeaway?
It’s kind of unclear to me. Unless I’m missing/forgetting something, the main concrete accusation in the OP is the personhood contract, which is pretty weird but seems unlikely to cause this much damage.
I thought Vassar is known to seek out people on the margin who have ongoing crises, which complicates the statistical interpretation of vibes from his interactions. It seems more accurate to focus on what he actually does, and whether that is appropriate for the crises he encounters.
Just of the people in my network this seems counterfactually responsible for: 1 suicides, indirectly I suspect a second, one (double) suicide attempt+psychosis (mine, many years ago), at least two other people having psychosis, two previously stable people driven into states that I can only describe as profoundly unhinged but not actually psychotic, and one explicit physical boundary crossing (grabbing someones arm when she clearly did not want this and was shaken afterwards). No double counting.
Why are you giving vague piecewise references to other people’s interactions with Michael Vassar, when you’ve had interactions yourself that you could surely be much more detailed and coherent with?
Let me check: you mean the grandchildren have the same ex ante expected height as the ex ante expected height of the children. Of course! (Just as the children have the same ex ante expected height as the parents’ ex ante expected height, which is now screened off by knowing their actual height.)
Yes, but in this case because you know the parents’ heights, the children’s ex ante expected height differs from the population mean.
But if you reset your expectations based on the observed children’s heights, you’ll still witness (on average) regression to the mean.
Though not towards the population mean but rather towards the ex ante expected height of the children.
It also doesn’t always happen. For instance if you have two pairs of parents that are far above the average in some partially-heritable trait, then their children will exhibit some regression to the mean and be less above average in the trait, but if the children pair off and have children of their own, then the children of the children will have the same expected trait level as the original children, i.e. no regression to the mean.
The category of sets in NF is not cartesian closed. It’s a non-starter.
This lacks functor categories e.g. Set^Set.