Reply to sibling - lean4 doesn't rest on ZF or ZFC. https://lean-lang.org/theorem_proving_in_lean4/Axioms-and-Co... However I believe an equivalence of power has been shown between the two.
replyRoughly, yes. See B. Werner (1997) “Sets in types, types in sets”.
replydo we know if claude's formalization is built on top of zfc and not zfc+extra?
replyzfc itself is not sufficient, you need some layers of extra concepts formalization to fit specific problem domain(e.g. zfc doesn't define even basic arithmetics), which also could have potential issues.
Within a given inference system, one can define concepts. This doesn’t add any axioms. It is, in essence, just a way to abbreviate things.
replyok, you now added some unknown inference system in addition to zfc
reply