12,080
edits
Changes
MyWikiBiz, Author Your Legacy — Monday November 25, 2024
Jump to navigationJump to searchDirectory:Jon Awbrey/Papers/Functional Logic : Quantification Theory (view source)
Revision as of 04:04, 18 November 2008
, 04:04, 18 November 2008no edit summary
===Umpire Operators===
===Umpire Operators===
In order to get a handle on the space of higher order propositions and eventually to carry out a functional approach to quantification theory, it serves to construct some specialized tools. Specifically, I define a higher order operator Υ, called the "umpire operator", which takes up to three propositions as arguments and returns a single truth value as the result. Formally, this so-called "multi-grade" property of <math>\Upsilon\!</math> can be expressed as a union of function types, in the following manner:
In order to get a handle on the space of higher order propositions and eventually to carry out a functional approach to quantification theory, it serves to construct some specialized tools. Specifically, I define a higher order operator <math>\Upsilon,\!</math> called the ''umpire operator'', which takes up to three propositions as arguments and returns a single truth value as the result. Formally, this so-called ''multi-grade'' property of <math>\Upsilon\!</math> can be expressed as a union of function types, in the following manner:
: <math>\Upsilon : \cup^{m = 1, 2, 3}((\mathbb{B}^k \to \mathbb{B})^m \to \mathbb{B}).</math>
: <math>\Upsilon : \bigcup_{m = 1, 2, 3} ((\mathbb{B}^k \to \mathbb{B})^m \to \mathbb{B}).</math>
In contexts of application the intended sense can be discerned by the number of arguments that actually appear in the argument list. Often, the first and last arguments appear as indices, the one in the middle being treated as the main argument while the other two arguments serve to modify the sense of the operation in question. Thus, we have the following forms:
In contexts of application the intended sense can be discerned by the number of arguments that actually appear in the argument list. Often, the first and last arguments appear as indices, the one in the middle being treated as the main argument while the other two arguments serve to modify the sense of the operation in question. Thus, we have the following forms:
