Quantifiers and n-ary binders : an OpenMath standard enhancement proposal

• It is proposed that the restriction in the OpenMath standard that an OMBIND element must have exactly three children should be lifted, to support more general binder symbols. The case of logics with generalised quantifiers is described in some detail, since these turn out to not have a natural encoding within OpenMath 2.0, because of precisely this restriction. That restricting quantifiers to a single body should have such consequences is not trivial, but follows from a theorem in the Logic branch of Philosophy.

Ämnesord

NATURVETENSKAP  -- Matematik -- Algebra och logik (hsv//swe)

NATURAL SCIENCES  -- Mathematics -- Algebra and Logic (hsv//eng)

NATURVETENSKAP  -- Data- och informationsvetenskap -- Programvaruteknik (hsv//swe)

NATURAL SCIENCES  -- Computer and Information Sciences -- Software Engineering (hsv//eng)

Nyckelord

OpenMath

binder

XML encoding

binary encoding

Lindström quantifier

second-order logic

general logics

condition clause

Mathematics/Applied Mathematics

matematik/tillämpad matematik

Publikations- och innehållstyp

ref (ämneskategori)

kon (ämneskategori)