solid-lean
The tower theory H is the many-sorted first-order theory of a tower of ZFC universes Z_0, Z_1, ... cut at consecutive inaccessible cardinals, with transition maps j_n identifying Z_n with the rank segment V(kappa_n) of Z_{n+1}. H is solid in Enayat's sense. For models M, N, P, with N interpreted in M and P interpreted in N, and an M-definable isomorphism between M and P, there is an M-definable isomorphism between M and N. The registered statement (Palomar/Challenge.lean) writes out the many-sorted first-order logic of H from scratch, with structures, formulas, satisfaction and definability…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-30-000022
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000022/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000022/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'