This makes Savage a better comparison point, since the Savage axioms are more similar to the VNM framework while also trying to construct probability and utility together with one representation theorem.

Sure, I guess I just always talk about VNM instead of Savage because I never bothered to learn how Savage’s version works. Perhaps I should.

As a representation theorem, this makes VNM weaker and JB stronger: VNM requires stronger assumptions (it requires that the preference structure include information about all these probability-distribution comparisons), where JB only requires preference comparison of events which the agent sees as real possibilities.

This might be true if we were idealized agents who do Bayesian updating perfectly without any computational limitations, but as it is, it seems to me that the assumption that there is a fixed prior is unreasonably demanding. People sometimes update probabilities based purely on further thought, rather than empirical evidence, and a framework in which there is a fixed prior which gets conditioned on events, and banishes discussion of any other probability distributions, would seem to have some trouble handling this.

Doesn’t pointless topology allow forsomedistinctions which aren’t meaningful in pointful topology, though?

Sure, for instance, there are many distinct locales that have no points (only one of which is the empty locale), whereas there is only one ordinary topological space with no points.

Isn’t the approach you mention pretty close to JB? You’re not modeling the VNM/Savage thing of arbitrary gambles; you’re just assigning values (and probabilities) to events, like in JB.

Assuming you’re referring to “So a similar thing here would be to treat a utility function as a function from some lattice of subsets of (the Borel subsets, for instance) to the lattice of events”, no. In JB, the set of events is the domain of the utility function, and in what I said, it is the codomain.

α=ωCK1, which makes the claim you made about it vacuous.

Proof: Let ⪯ be any computable well-ordering of N. Let f(n,m) be the number of steps it takes to compute whether or not n⪯m. Let g(n):=maxm≤nf(n,m) (notice I’m using the standard ordering ≤ on N, so this is the maximum of a finite set, and is thus well-defined). g is computable in O(n⋅g(n)) time. Let (,):N2→N be a bijective pairing function such that both the pairing function and its inverse are computable in polynomial time. Now let ~⪯ be the well-ordering of N given by (n,g(n))~⪯(m,g(m))⟺n⪯m, n~⪯(m,g(m)) if n is not (k,g(k)) for any k, and n~⪯m⟺n≤m if neither n nor m is of the form (k,g(k)) for any k. Then ~⪯ is computable in polynomial time, and the order type of ~⪯ is ω plus the order type of ⪯, which is just the same as the order type of ⪯ if that order type is at least ω2.

The fact that you said you think α is ω2 makes me suspect you were thinking of the least countable ordinal such that there is no recursive well-ordering of length α that can be proven to be a recursive well-ordering in a natural theory of arithmetic such that, for every computable function, there’s a program computing that function that the given theory can prove is total iff there’s a program computing that function in polynomial time.