[isabelle-dev] What is this 3 levels of lambda calculi?

Askar Safin safinaskar at mail.ru
Mon Mar 2 22:27:10 CET 2015

Hi. Isabelle docs says that the system contains "3 levels of lambda calculi with corresponding arrows =>, !! (aka \<And>) and ==>". What this means? Docs are not clear about this. What exactly is this 3 levels and why are they lambda calculi? Also, \<And> doesn't seem for me as arrow. Not because it is not look like arrow, of course, but for deeper reason: it doesn't construct "function type" for any lambda calculus. In other words: there is lambda calculus of objects with application "a b" and lambda constructor "%x. P x" and corresponding arrow "=>" for building function types for this calculus. Also, there is lambda calculus of proofs with meta modus ponens as application and deduction as lambda constructor and corresponding arrow "==>" for building "function types" for this proof calculus. But what about \<And>? I see 2 levels of calculi only

Askar Safin
Kazan, Russia

More information about the isabelle-dev mailing list