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.
I am confused by your comment. If $\eta$ is the least worldly cardinal in $L[0^\#]$, working in $V_\eta^{L[0^\#]}$, there is no $\alpha$ for which $V_\alpha\models\sf ZF$, but $0^\#$ still exists.
What? Why? Of course not! TG implies there is the same as ZFC+"Proper class of inaccessible cardinals". Reflecting "There are unboundedly many inaccessible cardinals" will give you an inaccessible limit of inaccessible. This is equivalent to ZFC+"Ord is Mahlo".
@NoahSchweber: Well, yeah, but also it may very well be provable from AD that counterexamples exist below the continuum. Maybe some odd Borel equivalence relation...
Andrej, I don't know about other people. But when you go like "Ugh, I'm gonna get comments about this being a thing, because I choose to present my argument in a specific way" it elicit responses, exactly of the kind you're anticipating. Nobody feels the need to defend ZFC. I think I'm just a bit confused with the exasperated tone, and I imagine other people are too.
@NaïmFavier: I'm glad for you. I'm proving theorems by writing proofs. I enjoy programming, and I enjoy doing maths the way I do it. I'd say it's a hobby, but I do have a permanent job as a mathematician and programming is just a side hobby. If you don't mind, I'll keep doing it this way.
To pull from the programming analogy, I agree that writing code in Common Lisp is very different from writing code in assembly. Even if the end result of the CL code is the same exact code. But this comes down to your point of view on mathematics. Are we proving the existence of algorithms and programs, or are we writing code? If it is the former, then how does CL and Asm differ?