On 02/06/18 09:33, Ken Kubota wrote: > Set theory (e.g., ZFC, the variant of Zermelo set theory in use today) > takes a very different approach by giving the class status by default, > and giving the set status only to those constructions often used. > Compared with the type theoretic approach this means that the set theoretic > solution is to simply forbid all reasoning first, and then to allow only > certain > constructions (a positive list). > The result (ZFC) is a not systematic solution of the problem (Russell's > antinomy), > but a preliminary solution based on the explored fields of mathematics at > that time.
ZFC is the formalization of the intuitive concept of the cumulative hierarchy of sets. It is not just a collection of ad-hoc axioms. There is a mental trick at play with type theories. They only seem to be more natural than ZFC because the domain of quantification is hidden by default in many proof assistants based on type theories. If you did the same with ZFC, it would likewise be perceived as natural. If you build a proof assistant for set theory you _can_ introduce syntactical sugar for restricted quantification as in type theory and automatic “typing” (sets used as the quantification domain are inferred instead of being made explicit). > For example, ZFC is not sufficient to handle large cardinals (which require an > additional axiom), and it should be easy to construe other examples not > covered > by ZFC by introducing other axioms. It has large enough cardinals for all ordinary purposes. The “large” in “large cardinal axioms” is meant to be interpreted in a relative sense. Adding large cardinals axioms typically gives a model of ZFC, or ZFC+large (but not as large) cardinal. You can even find a diagram of which large cardinal axioms imply the consistency of which ZFC+not so large cardinals. The issue thus is consistency. There is no way to escape that situation by the well known results of Tarski on undefinability of arithmetical truth and Gödel on consistency and completeness. We do not have, say, a set of all ordinals, or of all cardinals, that is because it is incompatible with the separation axiom, so any set theory which has an universal set and separation is inconsistent. Jensen’s version of New Foundations (NFU) has an universal set and a set of all ordinals and moreover can be proved consistent in ZFC (even less than that). The downside is of course, that the separation axiom does not hold. Higher order logic has the counter-part of the axiom of separation in set theory, but it does not have a real universal set. It only has, for each type, the set of all elements of all type, and that is called “universal”, but that is a bit of a misuse. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
