> expressive enough to produce

you understand that "expressive enough to produce" are not obvious elements of zfc, that's some average consumer napkin math and not strict formalization.

▲

Almondsetat 39 minutes ago | parent [-]

why should they be obvious? they are derived and have been thoroughly proven.

▲

andriy_koval 31 minutes ago | parent [-]

looks like we are in disagreement

▲

Almondsetat 8 minutes ago | parent [-]

A quick google search shows different proof assistants have been used to obtain the Peano axioms from ZFC, such as Isabelle/ZF and Metamath. I think you're just wrong

	▲	andriy_koval 5 minutes ago \| parent [-]
		you are entitled to have your opinion :-)