4 ms·
This 'baggage' are statements like sqrt(17) ∈ log(.) (where (log(.) is the logarithm function) which are syntactically valid and have a truth value, which
by GregarianChild 6y ago
This 'baggage' are statements like
sqrt(17) ∈ log(.)
(where (log(.) is the logarithm function) which are syntactically valid and have a truth value, which depends on the exact nature of how you code up various mathematical things in ZF(C). Your cannot form such propositions in type-theory. The downside of type-theory is that it seems difficult to have simple inclusions like:
Naturals ⊆ Integers ⊆ Rational ⊆ Reals
and that certain natural operations (like quotients) seemingly are labourious in type-theory.
- zozbot234 6y agoThese inclusions are anything but "simple", even in material set theory. Consider the real numbers; in common formalizations, a "real number" is an equivalence class of infinite sequences of rational numbers. You can't understand the 'inclusion' of rationals in reals as material (set theoretical) inclusion; you need an adapter/wrapper function. Type theory works the same way. Quotients are not "natural" from a constructive POV, and that's ultimately where the difficulties you're referencing come from. If you're OK with being non-constructive, quotients can be formalized ad hoc. (One of the positive side effects of homotopy-theoretical foundations is that they might help clarify what exactly is going on when one reasons on quotients.)
- GregarianChild 6y agoIn ZFC, you define reals as you sketch, and then specify rationals, integers etc as specific subsets, then you get inclusions, which mainstream mathematics uses without worries. And yes, mainstream mathematics is non-constructive (as is Isabelle/HOL). (I don't want to have a contentious discussion about FOMs, or which prover is best, just trying to sketch the trade-offs, and historical background.)