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.\!$