Stream: Beginner Questions

Topic: ✔ when defining HOL, how can I cause λx.x to be a formula?

Adam Dingle (Mar 15 2026 at 12:15):

Suppose that I want to define HOL as a theory in Pure. I might begin by defining the object-level equality operator = with some associated axioms. Then as a next step I could define True as (λx.x = λx.x).

Here's my attempt to do that:

theory hello
imports Pure

begin

typedecl formula

judgment trueprop :: "formula ⇒ prop"  (‹_› 5)

axiomatization eq :: "formula ⇒ formula ⇒ formula" (infixl ‹=› 50) where
  refl: "t = t" and
  subst: "s = t ⟹ P s = P t"

definition true :: formula where
  "true ≡ ((λx. x) = (λx. x))"

end

However, the definition of true above fails to type check. That's because = expects two formulas, yet (λx. x) isn't a formula - it's a pure term of type 'a -> 'a.

So somehow I need λx. x to have type formula, but I don't see how to achieve that. HOL/HOL.thy has

definition True :: bool
  where "True ≡ ((λx::bool. x) = (λx. x))"

so it works there, but doesn't in my minimal example. What am I missing?

Adam Dingle (Mar 15 2026 at 12:28):

I figured out my own mistake: eq should have type 'a => 'a => formula, not formula => formula => formula.

Notification Bot (Mar 15 2026 at 12:28):

Adam Dingle has marked this topic as resolved.

Last updated: Mar 25 2026 at 02:29 UTC