Simple Type Theory doesn't have type variables. Since HOL (by Mike Gordon) has type variables, it is not Simple Type Theory, but Polymorphic Type Theory.
____________________________________________________ Ken Kubota doi.org/10.4444/100 <https://doi.org/10.4444/100> > Am 10.03.2020 um 20:45 schrieb 'fl' via Metamath <[email protected]>: > > What would be interesting and relevant would be a formalization of the > different types of theories of types applied to lambda calculus. > At the moment we have the Simple Type Theory (i.e. HOL) developed by Mario > Carneiro but there are many type theories. > Dependent Type Theory is only one of them. Of course it would need a lot of > commentary and references to book sources. > > -- > FL > > -- > You received this message because you are subscribed to the Google Groups > "Metamath" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected] > <mailto:[email protected]>. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/2337506c-0c61-4269-be58-cde052ed7ec7%40googlegroups.com > > <https://groups.google.com/d/msgid/metamath/2337506c-0c61-4269-be58-cde052ed7ec7%40googlegroups.com?utm_medium=email&utm_source=footer>. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/AD74C364-2196-412D-BAC8-78DE47FEAA3A%40kenkubota.de.
