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 MHonArc.