Changes

<p><math>\$ : (\underline\mathbb{B}^k \to \underline\mathbb{B}) \times (X \to \underline\mathbb{B})^k \to (X \to \underline\mathbb{B}).</math></p></li>

<p><math>\$ : (\underline\mathbb{B}^k \to \underline\mathbb{B}) \times (X \to \underline\mathbb{B})^k \to (X \to \underline\mathbb{B}).</math></p></li>

</ol>

</ol>

<pre>

<pre>

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.

Because this notation is only used in settings where the imagination f : (U -> B)k and the connection F : Bk -> B are distinguished by their types, it does not really matter whether one writes "F $ f" or "f $ F" for the initial composition.

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

Just as a sentence is a sign that denotes a proposition, which thereby serves to indicate a set, a propositional connective is a provision of syntax whose mediate effect is to denote an operation on propositions, which thereby manages to indicate the result of an operation on sets.  In order to see how these compound forms of indication can be defined, it is useful to go through the steps that are needed to construct them.  In general terms, the ingredients of the construction are as follows:

Because this notation is only used in settings where the imagination f : (U �> B)k and the connection F : Bk �> B are distinguished by their types, it does not really matter whether one writes "F $ f" or "f $ F" for the initial composition.

Just as a sentence is a sign that denotes a proposition, which thereby serves to indicate a set, a propositional connective is a provision of syntax whose mediate effect is to denote an operation on propositions, which thereby manages to indicate the result of an operation on sets.  In order to see how these compound forms of indication can be defined, it is useful to go through the steps that are needed to construct them. In general terms, the ingredients of the construction are as follows:

1.  An imagination of degree k on U, in other words, a k-tuple of propositions fj : U -> B, for j = 1 to k, or an object of the form f = <f1, ..., fk> : (U -> B)k.

1. An imagination of degree k on U, in other words, a k�tuple of propositions fj : U �> B, for j = 1 to k, or an object of the form f = <f1, ..., fk> : (U �> B)k.

2. A connection of degree k, in other words, a proposition about things in Bk, or a boolean function of the form F : Bk -> B.

From these materials, it is required to construct a proposition P : U -> B such that P(u) = F(f1(u), ..., fk(u)), for all u C U.  The desired construction is determined as follows:

From these materials, it is required to construct a proposition P : U �> B such that P(u) = F(f1(u), ..., fk(u)), for all u C U.  The desired construction is determined as follows:

The cartesian power Bk, as a cartesian product, is characterized by the possession of a "projective imagination" p = <p1, ..., pk> of degree k on Bk, along with the property that any imagination f = <f1, ..., fk> of degree k on an arbitrary set W determines a unique map f! : W �> Bk, the play of whose projective images <p1(f!(w), ..., pk(f!(w)) on the functional image f!(w) matches the play of images <f1(w), ..., fk(w)> under f, term for term and at every element w in W.

The cartesian power Bk, as a cartesian product, is characterized by the possession of a "projective imagination" p = <p1, ..., pk> of degree k on Bk, along with the property that any imagination f = <f1, ..., fk> of degree k on an arbitrary set W determines a unique map f! : W -> Bk, the play of whose projective images <p1(f!(w), ..., pk(f!(w)) on the functional image f!(w) matches the play of images <f1(w), ..., fk(w)> under f, term for term and at every element w in W.

Just to be on the safe side, I state this again in more standard terms.  The cartesian power Bk, as a cartesian product, is characterized by the possession of k projection maps pj : Bk �> B, for j = 1 to k, along with the property that any k maps fj : W �> B, from an arbitrary set W to B, determine a unique map f! : W �> Bk such that pj(f!(w)) = fj(w), for all j = 1 to k, and for all w C W.

Just to be on the safe side, I state this again in more standard terms.  The cartesian power Bk, as a cartesian product, is characterized by the possession of k projection maps pj : Bk -> B, for j = 1 to k, along with the property that any k maps fj : W -> B, from an arbitrary set W to B, determine a unique map f! : W -> Bk such that pj(f!(w)) = fj(w), for all j = 1 to k, and for all w C W.

Now suppose that the arbitrary set W in this construction is just the relevant universe U.  Given that the function f! : U �> Bk is uniquely determined by the imagination f : (U �> B)k, that is, by the k�tuple of propositions f = <f1, ..., fk>, it is safe to identify f! and f as being a single function, and this makes it convenient on many occasions to refer to the identified function by means of its explicitly descriptive name "<f1, ..., fk>".  This facility of address is especially appropriate whenever a concrete term or a constructive precision is demanded by the context of discussion.

Now suppose that the arbitrary set W in this construction is just the relevant universe U.  Given that the function f! : U -> Bk is uniquely determined by the imagination f : (U -> B)k, that is, by the k-tuple of propositions f = <f1, ..., fk>, it is safe to identify f! and f as being a single function, and this makes it convenient on many occasions to refer to the identified function by means of its explicitly descriptive name "<f1, ..., fk>".  This facility of address is especially appropriate whenever a concrete term or a constructive precision is demanded by the context of discussion.

</pre>

</pre>