I've read (somewhere) that types in typed first-order logic is just 'syntactic sugar'.
But, surely there is more to than that?
For example: the upper-bound property of the reals can't be expressed in first order logic, but it can be in second. Now with Henkin semantics this is the same as typed first-order logic, so although the property can't be expressed in first-order logic, it can be if it is typed.
Are there useful ideas/theorems that make essential use of types in typed first-order logic?