Changes

To encapsulate the form of this general result, I define a composition that takes an imagination <math>\underline{f} = (f_1, \ldots, f_k) \in (X \to \underline\mathbb{B})^k</math> and a boolean connection <math>F : \underline\mathbb{B}^k \to \underline\mathbb{B}</math> and gives a proposition <math>p : X \to \underline\mathbb{B}.</math>  Depending on the situation, specifically, according to whether many <math>F\!</math> and many <math>\underline{f},</math> a single <math>F\!</math> and many <math>\underline{f},</math> or many <math>F\!</math> and a single <math>\underline{f}</math> are being considered, respectively, the proposition <math>p\!</math> thus constructed may be referred to under one of three descriptions:

To encapsulate the form of this general result, I define a composition that takes an imagination <math>\underline{f} = (f_1, \ldots, f_k) \in (X \to \underline\mathbb{B})^k</math> and a boolean connection <math>F : \underline\mathbb{B}^k \to \underline\mathbb{B}</math> and gives a proposition <math>p : X \to \underline\mathbb{B}.</math>  Depending on the situation, specifically, according to whether many <math>F\!</math> and many <math>\underline{f},</math> a single <math>F\!</math> and many <math>\underline{f},</math> or many <math>F\!</math> and a single <math>\underline{f}</math> are being considered, respectively, the proposition <math>p\!</math> thus constructed may be referred to under one of three descriptions:

<pre>

<ol style="list-style-type:decimal">

1. In a general setting, where the connection F and the imagination f are both permitted to take up a variety of concrete possibilities, call P the "stretch of F and f from U to B", and write it in the style of a composition as "F $ f".  This is meant to suggest that the symbol "$", here read as "stretch", denotes an operator of the form  

 

<li>

<p>In a general setting, where the connection <math>F\!</math> and the imagination <math>\underline{f}</math> are both permitted to take up a variety of concrete possibilities, call <math>p\!</math> the ''stretch of <math>F\!</math> and <math>\underline{f}</math> from <math>X\!</math> to <math>\underline\mathbb{B},</math>'', and write it in the style of a composition as <math>F ~\$~ \underline{f}.</math> This is meant to suggest that the symbol <math>^{\backprime\backprime} $ ^{\prime\prime},</math> here read as ''stretch'', denotes an operator of the form:</p>

 

$ : (Bk -> B) x (U -> B)k -> (U -> B).

</ol>

2. In a setting where the connection F is fixed but the imagination f is allowed to vary over a wide range of possibilities, call P the "stretch of F to f on U", and write it in the style "F$f", exactly as if "F$" denotes an operator F$ : (U -> B)k -> (U -> B) that is derived from F and applied to f, ultimately yielding a proposition F$f : U -> B.

2. In a setting where the connection F is fixed but the imagination f is allowed to vary over a wide range of possibilities, call P the "stretch of F to f on U", and write it in the style "F$f", exactly as if "F$" denotes an operator F$ : (U -> B)k -> (U -> B) that is derived from F and applied to f, ultimately yielding a proposition F$f : U -> B.