n-ary OMBIND

[jbs1]

migrated from Trac, where originally posted by kohlhase on 25-Feb-2011 1:12pm

Lars Hellstroem suggests to "lift the restriction on
OMBIND that it must have exactly three children. Rather, I think it should (like OMA) allow any number of children, as long as the first is the binder (typically a symbol) and the second is the OMBVAR with the variables it binds. Since this issue was last up for discussion (two years ago, I think), I have furthermore become aware of a new use-case: Lindström quantifiers."

James Davenport and I have proposed the same extension in an OpenMath paper 2009 (see http://kwarc.info/kohlhase/papers/om09-quantifiers.pdf).

[jbs1]

migrated from Trac, where originally posted by lars_h on 25-Feb-2011 4:27pm

Replying to [ticket:136 kohlhase]:

James Davenport and I have proposed the same extension in an OpenMath paper 2009 (see http://kwarc.info/kohlhase/papers/om09-quantifiers.pdf).

I currently get a 404 (object not found) on that URL.

(However, if it's 7 pages long and titled "Quantifiers and Big Operators in OpenMath", then James mailed that paper to me earlier today.)

[jbs1]

migrated from Trac, where originally posted by kohlhase on 26-Feb-2011 5:00am

sorry for that, the URL should work now.

[jbs1]

migrated from Trac, where originally posted by lars_h on 9-Mar-2011 6:24pm

In order to amend the existing writings on this subject, I have written up an explanation of

1. why one might want to use quantifiers other than the standard \forall and \exists, and
2. how Lindström quantifiers are defined.

I should probably add more references, specifically to articles which use them, but I suspected I should let others comment on what I've written so far.

Is BibTeX preferable, or should we just do a plain \begin{thebibliography}?

[jbs1]

migrated from Trac, where originally posted by lars_h on 14-Mar-2011 4:04pm

Text on Lindström quantifiers

[jbs1]

migrated from Trac, where originally posted by jhd on 28-Mar-2011 5:59pm

Interesting. I like the example of the H"artig quantifier, as one that's very different.

[jbs1]

migrated from Trac, where originally posted by lars_h on 15-May-2014 12:46pm

Also relevant is of course my paper on the 2013 OM workshop, elaborating on the attachment given above:
http://ceur-ws.org/Vol-1010/paper-21.pdf

[kohlhase]

moved to OpenMath/OMSTD#23