Church tried to reduce logic to his invention, the untyped lambda calculus, but failed in a first attempt [1]. He then proceeded later on to invent the simple t

Church tried to reduce logic to his invention, the untyped lambda calculus, but failed in a first attempt [1]. He then proceeded later on to invent the simple theory of types, [2], and type theory is pretty much a descendant of that. My argument with abstraction logic is that trying to use lambda+types for logic is actually misguided and overly restrictive. Abstraction logic is simpler, and can nevertheless also express variable binding naturally. You are kind of lucky that you are relatively fresh to all this, so you can approach both type theory and abstraction logic with an open mind, and see for yourself which you find more appealing. [1] S. C. Kleene, J. B. Rosser. The Inconsistency of Certain Formal Logics. Annals of Mathematics, 1935. [2] Alonzo Church. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic, 1940.