I just read that Hermann Weyl used a certain type of type theory as the foundation of mathematics in his book "The Continuum" and he was able to derive calculus without the use of infinite sets. Naturally, I'm going to read it ASAP but I wanted to ask right away what it's fundamental flaws are, since obviously its not taken as the conventional foundation (instead of ZFC). I'm inclined to assume that it's nothing detrimental to mathematical physics, since that was Weyl's primary field.


You can see Hermann Weyl:

In Das Kontinuum he tries to overcome this [the vicious circles he believed being involved with set-theoretical approach to foundations] by providing analysis with a predicative formulation — not, as Russell and Whitehead had attempted, by introducing a hierarchy of logically ramified types, which Weyl seems to have regarded as excessively complicated — but rather by confining the comprehension principle to formulas whose bound variables range over just the initial given entities (numbers). Accordingly he restricts analysis to what can be done in terms of natural numbers with the aid of three basic logical operations, together with the operation of substitution and the process of “iteration”, i.e., primitive recursion.

Weyl recognized that the effect of this restriction would be to render unprovable many of the central results of classical analysis — e.g., Dirichlet’s principle that any bounded set of real numbers has a least upper bound — but he was prepared to accept this as part of the price that must be paid for the security of mathematics.

  • $\begingroup$ Interestingly, there are two different kinds of completeness for the reals: (1) Any bounded set of reals has a supremum ; (2) Any bounded sequence (function from N into R) has a limit supremum. (1) easily implies (2) in any reasonable formal system, but to get (1) from (2), the naive proof requires DC (dependent choice), and the more clever proof needs CC (countable choice): Let $q$ enumerate the non-negative rationals. Take any set $S$ of reals with upper bound $b$. Let $f(n) = \cases{ q_n & if $b-q_n \ge x$ for any $x \in S$ \\ 0 & otherwise }$. Let $c = \sup(f)$. ... Then $b-c = \sup(S)$.) $\endgroup$ – user21820 Aug 26 '16 at 14:55

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.