The continuum hypothesis is answered positively assuming the axiom of constructibility. Essentially, this is a good axiom if you assume that there are no new ways to construct sets than the ones we are used to (pairing, powerset, etc...).

@JochenGlueck Somehow I forgot to respond to your last question. The answer isn't that we are using the definition of $s_{\alpha_k}$ to "imply that $1\in \langle s_{\alpha_1},\ldots, s_{\alpha_{k-1}}\rangle$". Rather, we are simply using the fact that the ideal generated by a finite list of elements is the same as the ideal generated by the nonzero elements from that list.

I don't know if it has a standard name. For idempotents in rings, usually one considers the reversed relation, which is just the subidempotent relation. I might call it the "absorption" relation.

The finite topology is discussed quite a bit in L. Fuchs's books on (infinite) abelian groups. The concept was first developed (according to Fuchs) by Szele in the paper " On a topology in endomorphism rings of abelian groups". The topology is Hausdorff, linear, and (quite importantly) complete (in the net sense). In my own studies, the summability notion (of adding infinitely many endomorphisms) has been quite important.

I'm excited to look at your book. Great job Bogdan!

Let us continue this discussion in chat.

@SergeiArtemov Thanks for the clarifications! Accepting that selector proofs are a native PA tool, then they only "prove serial properties" when you either (i) expand your sense of formal derivation (as Noah did) or (ii) expand your meta-notion of "prove" to accept serial proofs as a valid means of meta-verification. Sure, this can be like a feature in your car that you never used before. But so is using PA+Con(PA) in your metatheory, which runs counter to not assuming PA is consistent to begin with. (BTW, writing {F(0),F(1),...} starts introducing second order logic into metatheory.)

We have not affected what PA proves or does not prove. We have not changed formal entailment. But we have assumed stronger (non-PA) metatheoretic tools (by allowing selector proofs). Thus, in Artemov's abstract, when he writes "PA proves its own consistency", I believe this means "PA proves a statement that is equivalent (under a stronger theory than PA, but weak in some relevant ways) to consistency".

@AlexKruckman I think the problem is as follows. (Sergei, feel free to correct me if I get something wrong.) There is a metamathematical statement Z that is equivalent to the metamathematical statement "PA is consistent", but the proof of that equivalence uses the idea of selector proofs. This equivalence is not provable in PA, only in a strictly stronger metatheory. We can encode "PA is consistent" as the arithmetic sentence Con(PA), which PA does not prove. We can encode Z as Con^S(PA), which PA does prove. (continued...)

@SergeiArtemov If we allow selector proofs as an additional tool in our toolkit, then doesn't Con^S(PA) fail to capture consistency because it fails to capture that selector proofs provide a possible additional avenue to a contradiction?