For a CSR
To show that
If
If
tailcalled
Karma: 8,282
I’ve learned some more constructive math since my previous comments, so I thought I should correct myself a bit:
In Coq, the type of truth values is called Prop. In other foundations, it might be encoded differently, including by encoding functions into truth-values as functions out of an arbitrary type.
You would generally not interpret functions into Prop as functions out of an arbitrary type. In predicative foundations, this is the only way to really specify subtypes, but the entire point of predicativity is that you can’t really work with the type of all subtypes, so this doesn’t really work for the real numbers.
For some reason, the standard way people tend to construct the Dedekind reals in predicative systems is to pick some type universe U and define propositions PropU to be the subsingletons of U. Then you can do most things you want to do with it, but the real numbers will not be a member of U for size reasons, and therefore the cuts cannot mention real numbers in their definition, only rational numbers.
I say “for some reason” because I feel like there is a perfectly cromulent alternative: Use the Sierpinski type
Cauchy sequences you’d usually not just use CSRs but also Cauchy sequences of CSRs (and so on, recursively).
This is what the HoTT book does because they don’t want to assume countable choice, and without countable choice, CSRs quotiented by converging to the same point are not necessarily Cauchy-complete.
However, if you are being constructive because you want to be computable, then you can still assume countable choice, so this is not a problem.
When constructed more carefully, every Cauchy sequence corresponds to a Dedekind cut, but it requires something stronger (such as excluded middle) to show that every Dedekind cut corresponds to a Cauchy sequence.
You can show that every Dedekind cut corresponds to a Cauchy sequence using countable choice rather than excluded middle. The binary search argument shows that for any N, there exists a rational number xN within range 1/N of the Dedekind cut. You need countable choice to assemble these into a sequence and thereby have a Cauchy sequence.
The counterexample is the sheaf topos
See also What is the computational content of the axiom of choice? for more on countable choice.
Do note the followup that axiom of countable choice is constructively computable and therefore the choice-using proof goes through computably. The universe that kills countable choice is not the computable universe RT(K1), but rather the continuous universe Sh(ℝ), where everything is a continuous function out of the real numbers. The failure of “For any real number x, there is a sequence x̂ : ℕ → ℚ converging to x.” in that universe translates to the failure of “For any continuous function x : ℝ → ℝ, there exists a continuous family of sequences x̂ : ℝ×ℕ → ℚ converging to x.”. The trouble with that statement is that ℚ is discrete, so x̂ is forced to be constant in its first parameter.
Your proof is perfectly valid in classical math with excluded middle. However, classical math lacks the computational substance that this post centers around.
Start with a = 1, repeat a = a * 2 while |x| > a. This will end in a finite number of steps.
“While |x| > a” requires excluded middle over |x| > a. Constructively, the inequality operator for real numbers only supports a weaker form of excluded middle called comparison: if x < y then x < z or z < y. Not a huge problem for this part of the proof as you could just case split by |x| > a or |x| < a+1.
Though if you do this, because these are overlapping conditions, its no longer deterministic, so a isn’t a function of x.
You essentially just want a rational upper bound for x, though. This does exist (not as a function as that would be discontinuous) and you don’t need to do an algorithm for figuring it out. (Under the hood in RT(K1), this is essentially because representations of real numbers come packaged with an upper and lower rational bound.)
Start with the segment [-a, a]. On each step split it in half and pick the half that contains x (if x is exactly in the middle, pick the left half). Repeat this exactly n times. The last splitting point is x̂(n).
“Pick the half that contains x” requires excluded middle too, for comparing the midpoint with x. Again you could probably add an epsilon of leeway to let comparison go through, but then there’s no functional relationship, and you need countable choice to pin down x̂.
What is the computational substance of the axiom of choice?
There are numerous set theories that allow “set of all sets”, the most well-known of which is probably New Foundations (NF).
The category of sets in NF is not cartesian closed. It’s a non-starter.
There are also some theories such as Morse-Kelley theory that have both classes and sets, and include a class of all sets.
This lacks functor categories e.g. Set^Set.
I also don’t really have any intuition for what you can or cannot do with stratified formulas.
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.
The propositions in this case are open sets, but propositions in general can be whatever they want. Unless one uses
Unfortunately I don’t really have any intuition for this. 😅 I have been thinking a bit about