>>11222458>completeness theoremI am not familiar with those, but...
>unless you accept that "E->F" is not interpreted as F^E but a subset of it, or a variant like a third set M(E,F) and a dedicated "apply" map a_{E,F}: M(E,F)xE -> F )This is related to how types are like a specification or a program right? So if you have a Nat, in type theory you cannot directly iterate over every possible element of that type, but in set theory you can over the set Nat.
I kind of see this as an advantage though. Yes, it is true that in type theory you can do less out of the box as a consequence of the operations themselves being more primitive. But on the other hand, sets themselves are too complex as data structures to be the foundation. Before you can talk about sets you really should talk about lists, and before you talk about lists you should talk about natural numbers.
Type theory gets the natural order of concepts right, and the fact that it can be compiled and used on a computer is a great argument in its favor as a foundation of mathematics.
Set theory really only has an advantage over type theory if you are doing things on pen and paper and you want to cram down the size of the proof. Then things being less primitive is good. But computers exist in this era and math should go the way of programming.
