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

[Askar Safin]

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
http://vk.com/safinaskar
Kazan, Russia