> 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.<p>I am not sure if it is very pedagogical to teach an unsound logic. How about you try a sound one? No types required: <a href="https://obua.com/publications/philosophy-of-abstraction-logic/2/" rel="nofollow">https://obua.com/publications/philosophy-of-abstraction-logi...</a><p>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!