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

(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 $(x\to y)\to ({\square }_{p}x\to {\square }_{p}y)$ (weak distributivity) --- which hold for the reasons in the post

Rules of inference:

• Necessitation $⟨x,{\square }_{p}x⟩$
• Modus Ponens $⟨x\to y,x,y⟩$

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 ($⊢x\to y⟹⊢{\square }_{p}x\to {\square }_{p}y$) 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 ${\square }_p$ logic and $\square$ 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!