First page Back Continue Last page Overview Graphics
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: