[FOM] Wiki: type theoretic fnds

[Arnold Neumaier]

On 04/01/2016 08:02 AM, Harvey Friedman wrote:
> On Thu, Mar 31, 2016 at 12:08 AM, Mario Carneiro <di.gama at gmail.com> wrote:
>> One obvious property of type theory in general, that has been mentioned
>> several times on related threads, is that type theory has a much stronger
>> ability to reject statements as ill-formed, which is a *good thing*. In set
>> theory, you are not allowed to write "x in in y". Why?
> 
> The cost is of course that lots of very natural things that you want
> to say are now barred. I believe that the cure is much worse than the
> disease.

As a mathematician, I fully agree that strong typing is a *bad thing*.
See my essay
   Foundations of Mathematics
   http://www.mat.univie.ac.at/~neum/FMathL/foundations.html
criticizing structural set theory as described, e.g., in
   https://ncatlab.org/nlab/show/structural+set+theory


>> "0 in 1" is perfectly valid, even though many mathematicians will tell you
>> this is meaningless. (If you spend too much time with ZFC, you will become
>> convinced that this is a normal question, since it is well-formed according
>> to ZFC, and the answer is "yes" if those are defined as von Neumann
>> ordinals.)

In ZF + global choice - the foundations used by Bourbaki, the masters of
structural mathematics,
    https://en.wikipedia.org/wiki/Choice_function
it is easy to removing all problems associated with ''mistyped''
statements in an untyped set theory language without complicating
anything.

Global choice means the existence of a choice operator \tau that
assigns to each satisfiable predicate P(x) a distinguished element
x=\tau(P) satisfying it. Letting Peano(x) be the statement ''x
satisfies the Peano axioms'' and defining the natural numbers by
N:=\tau(Peano), and 0,1 as the first two elements in N makes the
statement 0 in 1 undecidable rather than true or false. This is
sufficient to remove any dependence of N on the way it is constructed
(which can be done in arbitrarily many different ways, in some of which
0 in 1 and some of which where this is false).

The same can be done for all standard objects and concepts.


Arnold Neumaier