Directory talk:Jon Awbrey/Papers/Functional Logic : Quantification Theory

Work Area

Functional Quantifiers

The umpire measure of type \({\Upsilon : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}}\!\) links the constant proposition \(1 : \mathbb{B}^2 \to \mathbb{B}\!\) to a value of \(1\!\) and every other proposition to a value of \(0.\!\) Expressed in symbolic form:

\(\Upsilon (f) = 1_\mathbb{B} \quad \Leftrightarrow \quad u = 1_{\mathbb{B}^2 \to \mathbb{B}}.\!\)

The umpire operator of type \({\Upsilon : (\mathbb{B}^2 \to \mathbb{B})^2 \to \mathbb{B}}\!\) links pairs of propositions in which the first implies the second to a value of \(1\!\) and every other pair to a value of \(0.\!\) Expressed in symbolic form:

\(\Upsilon (e, f) = 1 \quad \Leftrightarrow \quad e \Rightarrow f.\!\)