Yudhister Kumar
(very naive take) I would suspect this is medium-easily automatable by making detailed enough specs of existing hardware systems & bugs in them, or whatever (maybe synthetically generate weak systems with semi-obvious bugs and train on transcripts which allows generalization to harder ones). it also seems like the sort of thing that is particularly susceptible to AI >> human; the difficulty here is generating the appropriate data & the languages for doing so already exist ?
but only the dialogues?
actually, it probably needs a re-ordering. place the really terse stuff in an appendix, put the dialogues in the beginning, etc.
I’m less interested in what existing groups of things we call “species” and more interested in what the platonic ideal of a species is & how we can use it as an intuition pump. This is also why I restrict “species” in the blogpost to “macrofauna species”, which have less horizontal gene transfer & asexual reproduction.
I haven’t looked much at the extended phenotype literature, although that is changing as we speak. Thanks for pointing me in that direction!
The thing I wanted to communicate was less “existing groups of things we call species are perfect examples of how super-organisms should work” and more “the definition of an ideal species captures something quite salient about what it means for a super-organism to be distinct from other super-organisms and its environment.” In practice, yes, looking at structure does seem to be better.
Payor’s Lemma holds in provability logic, distributivity is invoked when moving from step 1) to step 2) and this can be accomplished by considering all instances of distributivity to be true by axiom & using modus ponens. This section should probably be rewritten with the standard presentation of K to avoid confusion.
W.r.t. to this presentation of probabilistic logic, let’s see what the analogous generator would be:
Axioms:
all tautologies of Christiano’s logic
all instances of (weak distributivity) --- which hold for the reasons in the post
Rules of inference:
Necessitation
Modus Ponens
Then, again, step 1 to 2 of the proof of the probabilistic payor’s lemma is shown by considering the axiom of weak distributivity and using modus ponens.
(actually, these are pretty rough thoughts. Unsure what the mapping is to the probabilistic version, and if the axiom schema holds in the same way)
No particular reason (this is the setup used by Demski in his original probabilistic Payor post).
I agree this is nonstandard though! To consider necessitation as a rule of inference & not mentioning modus ponens. Part of the justification is that probabilistic weak distributivity () seems to be much closer to a ‘rule of inference’ than an axiom for me (or, at least, given the probabilistic logic setup we’re using it’s already a tautology?).
On reflection, this presentation makes more sense to me (or at least gives me a better sense of what’s going on / what’s different between logic and logic). I am pretty sure they’re interchangeable however.
Yep! Thanks!
Yep! Fixed.
We know that the self-referential probabilistic logic proposed in Christiano 2012 is consistent. So, if we can get probabilistic Payor in this logic, then as we are already operating within a consistent system this should be a legitimate result.
Will respond more in depth later!
Language mix-up. Meant improper integrals.
Now that I’m thinking about it, my memory’s fuzzy on how you’d actually calculate them rigorously w/infinitesimals. Will get back to you with an example.
Have updated the definition of the derivative to specify the differences between over the hyperreals and over the reals.
I think the natural way to extend your to the hyperreals is for it to take values in an infinitesimal neighborhood surrounding rationals to 0 and all other values to 1. Using this, the derivative is in fact undefined, as
I agree. This is what I was going for in that paragraph. If you define derivatives & integrals with infinitesimals, then you can actually do things like treating dy/dx as a fraction without partaking in the half-in half-out dance that calc 1 teachers currently have to do.
I don’t think the pedagogical benefit of nonstandard analysis is to replace Analysis I courses, but rather to give a rigorous backing to doing algebra with infinitesimals (“an infinitely small thing plus a real number is the same real number, an infinitely small thing times a real number is zero”). *Improper integrals would make a lot more sense this way, IMO.
Here the magic lies in depending on the axiom of choice to get a non-principal ultrafilter. And I believe I see a crack in the above definition of the derivative. f is a function on the non-standard reals, but its derivative is defined to only take standard values, so it will be constant in the infinitesimal range around any standard real. If , then its derivative should surely be everywhere. The above definition only gives you that for standard values of .
Yep, the definition is wrong. If then let denote the natural extension of this function to the hyperreals (considering behaves like this should work in most cases). Then, I think the derivative should be
W.r.t. what the derivative of should be, I imagine you can describe it similarly in terms of , which by the transfer principle should exist (which applies because of Łoś′s theorem, which I don’t claim to fully understand).
For the derivative then is:
I’m familiar with \setminus being used to denote set complements, so \not\in seemed more appropriate to me ( is not an element of ). I interpret as “the elements of not in ,” which is the empty set in this case? (also the elements of are sets of naturals while the elements of are naturals, so it’s unclear to me how much this makes sense)
The post is wrong in saying that U contains only cofinite sets. It obviously must contain plenty of sets that are neither finite nor cofinite, because the complements of those sets are also neither finite nor cofinite. Possibly the author intended to type “contains all cofinite sets” instead.
Yep, this is correct! I’ve updated the post to reflect this.
E.g. if an ultrafilter contains the set of all even naturals, it won’t contain the set of all odd naturals, neither of which are finite or cofinite.
Thanks for the advice! Still learning how to phrase things correctly & effectively.
I wasn’t aware that you can’t actually explicitly construct a nonprincipal ultrafilter—this is interesting and nonintuitive to me!
yeah this is straightforwardly wrong, thanks. the first part should be read like “this is a way you can construct a physical realization of an automata corresponding to a type-3 grammar, this is in principle possible for all sorts of them”
will get back to you with something more rigorous