Stack Exchange network consists of 183 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.
@cody I don't see what being a topos has to do with biinterpretability. For example the category of topological spaces isn't a topos, but one can interpret $\sf{ETCS+R}$ in $\sf{ETCTS+R}$, by looking at the full subcategory on the discrete spaces. One identifies the discrete spaces in the categorical language by saying that they are precisely the objects such that any morphism into them which is both monic and epic is an isomorphism.
@VilleSalo Nice work! I'm still digesting your paper, but I noticed that the first two parts of your Question 1 "Does every finite-support configuration in the image of the Game of Life have a finite-support preimage? A co-finite-support preimage?" can be proved equivalent, because you can convert between the two kinds of preimage using a construction like the pattern shown in this post. Also I noticed a typo in Lemma 1; $R$ is used before it's defined.
@EmilJeřábeksupportsMonica Sorry for taking a while to get back to this. Where would I look for a proof of "If we loosen the definition so as to allow additional sorts, or extension by means of a relative interpretation, then every recursively axiomatizable first-order theory has a finitely axiomatized conservative extension."?
@TLW You try all values of $n$ increasingly. For each $n\times n$ box centred on the pattern you try to find a predecessor of the pattern all of whose live cells are in the box, and if that doesn't work you try to prove the box is an orphan. If neither of these succeeds then you increase $n$ and try again. Eventually you must succeed one way or the other since if the pattern has a predecessor it has a predecessor with finitely many live cells (which your box will eventually contain), and if it doesn't then it has an orphan (which your box will eventually contain).
