2
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ Not totally related, since this is about many-sorted first-order logic, and not higher-type first-order logic, but: for an example of themany-sorted framework not just being syntactic sugar, consider the "$\mathcal{M}^{eq}$" construction defined e.g. on page 28 of Marker's book on model theory: given a single-sorted structure $\mathcal{M}$, the many-sorted structure $\mathcal{M}^{eq}$ has one sort per parameter-free definable equivalence class on some finite power of $\mathcal{M}$. Since there are always infinitely many sorts, this construction cannot be made first-order in a nice way. $\endgroup$ Commented Jun 5, 2013 at 6:02

0

You must log in to answer this question.

Browse other questions tagged .