> Unlike conventional theorem provers, Holbert’s term language is just the untyped lambda calculus. While this technically makes the logic unsound, it is much simpler to use as a pedagogical tool.
I've come to the conclusion that Abstraction Logic (AL) is actually the golden middle between FOL (first-order logic) and HOL (simply-typed higher-order logic with Henkin semantics): You can view it both as FOL plus operators/general variable binding, and as HOL minus static types!
I am not sure if it is very pedagogical to teach an unsound logic. How about you try a sound one? No types required: https://obua.com/publications/philosophy-of-abstraction-logi...
I've come to the conclusion that Abstraction Logic (AL) is actually the golden middle between FOL (first-order logic) and HOL (simply-typed higher-order logic with Henkin semantics): You can view it both as FOL plus operators/general variable binding, and as HOL minus static types!