Categorial Types and Openmath: Type and Range

• "∀x∈ℝ”: Extensional notation is ambiguous

  • Range of quantification vs. type of variable
  • OpenMath: “range” in definite integration

• Generalized quantifiers will sometimes need type and/or range in addition to “body”

  • Neither: ombind(q,v,e) or oma(q, lv.e)
  • Type: ombind(q,v:t,e) or oma(q,lv:t.e)
  • Range: oma(q,lv.e,r)
  • Both: oma(q,lv:t.e,r)

Notes: