Hacker News Reader

Comment by ajs1998 | Hacker News Reader

ajs1998

ZFC is probably the biggest foundation, and only Choice is apparently controversial. The results aren't that weird, they're just different and occasionally more useful than using !Choice.

View on HN

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.

Roughly, yes. See B. Werner (1997) “Sets in types, types in sets”.

do we know if claude's formalization is built on top of zfc and not zfc+extra?

zfc 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.

ok, you now added some unknown inference system in addition to zfc

No, it is the same inference system. They are just abbreviations.

and what is that system?

ZFC

zfc is a bunch of axioms and not inference system. It is commonly assumed that it is built on top of some unspecified first order logic which commonly assumed to include bunch of inference rules. There is no ground truth in my understanding where this all is formally defined.

If you want to use “ZFC” to refer to the axioms without any rules of inference, I guess you can do that, but when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

> when someone refers to “ZFC” when they are filling a slot that needs a (axioms + rules of inference), the obvious interpretation is that they are referring to the usual system of ZFC.

its bro-math. In formal math you need to be specific what inference system you use. There are many of them. Then you need to have formal proof that in that system you can derive concept of function and then think about question if it won't make paradoxes and contradictions with ZFC.

Claude’s formalisation, being in Lean, is based on the calculus of inductive constructions, not ZFC. In Lean 3, per Carneiro, any theorem of Lean 3’s theory can be proved in ZFC plus some finite number of inaccessible cardinals (and, IIRC, vice versa). The precise strength of Lean 4 is not quite clear yet, I think (I guess this is partly what Lean4Lean is hoping to address).

Reply on news.ycombinator.com