Flexary operators for formalized mathematics

Abstract

We study representation formats that allow formally defining what we call flexary operators: functions that take arbitrarily many arguments, like Σk=1n ak or binders that bind arbitrarily many variables, like ∀x1,... xn. F. Concretely, we define a flexary logical framework based on LF, and use it as a meta-language to define flexary first-order logic and flexary simple type theory. We use these to formalize several flexary mathematical concepts including arithmetical and logical operators, matrices, and polynomials. © 2014 Springer International Publishing.