Condensation sentence for the constructible hierarchy (source code)

= Condensation sentence for the constructible hierarchy

A condensation sentence is a fixed first-order sentence $\sigma$ such that every transitive set satisfying $\sigma$ is $L_\lambda$ for a limit ordinal $\lambda$. It combines a sufficiently strong finite fragment of set theory, the assertion that every set is constructible, and the absence of a largest ordinal.