Re: [isabelle] Where to learn about HOL vs FOL?
On 1/31/2013 8:04 AM, Gottfried Barrow wrote:
The standard text that keeps getting mentioned by the logic gurus here
is Andrews' text, which starts with propositional logic and FOL, and
then covers type theory, where types would be the beginning of the
foundation of HOL in general:
When I'm only qualified to provide links, and I start speaking
authoritatively, then I quickly get in trouble.
Lambda calculus would be the beginning, and types comes next. I was
speaking of lambda calculus and types as being monolithic. In my mind,
it must be that lambda calculus and types are part of the same
foundation. That perception might be eliminated if I read more of the
books, or it might become stronger.
This archive was generated by a fusion of
Pipermail (Mailman edition) and