4 ms·
> But the first problem is, the number of legal transformations is actually infinite. I am fairly certain the number of legal transformations in mathematics is
by grondilu 2y ago
> But the first problem is, the number of legal transformations is actually infinite.
I am fairly certain the number of legal transformations in mathematics is not infinite. There is a finite number of axioms, and all proven statements are derived from axioms through a finite number of steps.
- hwayne 2y agoTechnically speaking one of the foundational axioms of ZFC set theory is actually an axiom schema, or an infinite collection of axioms all grouped together. I have no idea how lean or isabelle treat them.
- fspeech 2y agoWhether it needs to be a schema of an infinite number of axioms depends on how big the sets can be. In higher order logic the quantifiers can range over more types of objects.
- 4ad 2y agoLean (and Coq, and Agda, etc) do not use ZFC, they use variants of MLTT/CiC. Even Isabelle does not use ZFC.
- robinzfc 2y agoIsabelle is generic and supports many object logics, listed in [1]. Isabelle/HOL is most popular, but Isabelle/ZF is also shipped in the distribution bundle for people who prefer set theory (like myself). [1] https://isabelle.in.tum.de/doc/logics.pdf https://isabelle.in.tum.de/doc/logics.pdf