Changes

72 bytes removed ,  12:32, 14 December 2008
→‎Functional Quantifiers: sub concrete domain X for abstract domain B^2 to prevent possible confusion
Line 429: Line 429:  
==Functional Quantifiers==
 
==Functional Quantifiers==
   −
The '''umpire measure''' of type <math>\Upsilon : (\mathbb{B}^2 \to \mathbb{B}) \to \mathbb{B}</math> links the constant proposition <math>1 : \mathbb{B}^2 \to \mathbb{B}</math> to a value of 1 and every other proposition to a value of 0.  Expressed in symbolic form:
+
The '''umpire measure''' of type <math>\Upsilon : (X \to \mathbb{B}) \to \mathbb{B}</math> links the constant proposition <math>1 : X \to \mathbb{B}</math> to a value of 1 and every other proposition to a value of 0.  Expressed in symbolic form:
    
{| align="center" cellpadding="8"
 
{| align="center" cellpadding="8"
| <math>\Upsilon \langle u \rangle = 1_\mathbb{B} \quad \Leftrightarrow \quad u = 1_{\mathbb{B}^2 \to \mathbb{B}}.</math>
+
| <math>\Upsilon (u) = 1_\mathbb{B} \quad \Leftrightarrow \quad u = 1_{X \to \mathbb{B}}.</math>
 
|}
 
|}
   −
The '''umpire operator''' of type <math>\Upsilon : (\mathbb{B}^2 \to \mathbb{B})^2 \to \mathbb{B}</math> 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:
+
The '''umpire operator''' of type <math>\Upsilon : (X \to \mathbb{B})^2 \to \mathbb{B}</math> 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:
    
{| align="center" cellpadding="8"
 
{| align="center" cellpadding="8"
| <math>\Upsilon \langle u, v \rangle = 1 \quad \Leftrightarrow \quad u \Rightarrow v.</math>
+
| <math>\Upsilon (u, v) = 1 \quad \Leftrightarrow \quad u \Rightarrow v.</math>
 
|}
 
|}
  
12,080

edits