Changes

Strictly speaking, however, there is a subtle distinction in type between the function <math>f_i : X \to \mathbb{B}</math> and the corresponding function <math>g_j : \operatorname{E}X \to \mathbb{B},</math> even though they share the same logical expression.  Naturally, we want to maintain the logical equivalence of expressions that represent the same proposition while appreciating the full diversity of that proposition's functional and typical representatives.  Both perspectives, and all the levels of abstraction extending through them, have their reasons, as will develop in time.

Strictly speaking, however, there is a subtle distinction in type between the function <math>f_i : X \to \mathbb{B}</math> and the corresponding function <math>g_j : \operatorname{E}X \to \mathbb{B},</math> even though they share the same logical expression.  Naturally, we want to maintain the logical equivalence of expressions that represent the same proposition while appreciating the full diversity of that proposition's functional and typical representatives.  Both perspectives, and all the levels of abstraction extending through them, have their reasons, as will develop in time.

Because this special circumstance points up an important general theme, it is a good idea to discuss it more carefully.  Whenever there arises a situation like this, where one alphabet <math>\mathcal{X}</math> is a subset of another alphabet <math>\mathcal{Y},</math> then we say that any proposition <math>f : \langle \mathcal{X} \rangle \to \mathbb{B}</math> has a ''tacit extension'' to a proposition <math>\epsilon f : \langle \mathcal{Y} \rangle \to \mathbb{B},</math> and that the space <math>(\langle \mathcal{X} \rangle \to \mathbb{B})</math> has an ''automatic embedding'' within the space <math>(\langle \mathcal{Y} \rangle \to \mathbb{B}).</math>  The extension is defined in such a way that <math>\epsilon</math>''f'' puts the same constraint on the variables of <font face="lucida calligraphy">X</font> that are contained in <font face="lucida calligraphy">Y</font> as the proposition ''f'' initially did, while it puts no constraint on the variables of <font face="lucida calligraphy">Y</font> outside of <font face="lucida calligraphy">X</font>, in effect, conjoining the two constraints.

Because this special circumstance points up an important general theme, it is a good idea to discuss it more carefully.  Whenever there arises a situation like this, where one alphabet <math>\mathcal{X}</math> is a subset of another alphabet <math>\mathcal{Y},</math> then we say that any proposition <math>f : \langle \mathcal{X} \rangle \to \mathbb{B}</math> has a ''tacit extension'' to a proposition <math>\epsilon f : \langle \mathcal{Y} \rangle \to \mathbb{B},</math> and that the space <math>(\langle \mathcal{X} \rangle \to \mathbb{B})</math> has an ''automatic embedding'' within the space <math>(\langle \mathcal{Y} \rangle \to \mathbb{B}).</math>  The extension is defined in such a way that <math>\epsilon f\!</math> puts the same constraint on the variables of <math>\mathcal{X}</math> that are contained in <math>\mathcal{Y}</math> as the proposition <math>f\!</math> initially did, while it puts no constraint on the variables of <math>\mathcal{Y}</math> outside of <math>\mathcal{X},</math> in effect, conjoining the two constraints.

If the variables in question are indexed as <font face="lucida calligraphy">X</font>&nbsp;=&nbsp;{''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n''} and <font face="lucida calligraphy">Y</font>&nbsp;=&nbsp;{''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n'',&nbsp;&hellip;,&nbsp;''x''_''n''+''k''}, then the definition of the tacit extension from <font face="lucida calligraphy">X</font> to <font face="lucida calligraphy">Y</font> may be expressed in the form of an equation:

If the variables in question are indexed as <font face="lucida calligraphy">X</font>&nbsp;=&nbsp;{''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n''} and <font face="lucida calligraphy">Y</font>&nbsp;=&nbsp;{''x''₁,&nbsp;&hellip;,&nbsp;''x''_''n'',&nbsp;&hellip;,&nbsp;''x''_''n''+''k''}, then the definition of the tacit extension from <font face="lucida calligraphy">X</font> to <font face="lucida calligraphy">Y</font> may be expressed in the form of an equation: