| First, all of these properties are relative to a particular basis. For example, a singular proposition with respect to a basis <math>\mathcal{A}</math> will not remain singular if <math>\mathcal{A}</math> is extended by a number of new and independent features. Even if we stick to the original set of pairwise options <math>\{a_i\} \cup \{(a_i)\}</math> to select a new basis, the sets of linear and positive propositions are determined by the choice of simple propositions, and this determination is tantamount to the conventional choice of a cell as origin. | | First, all of these properties are relative to a particular basis. For example, a singular proposition with respect to a basis <math>\mathcal{A}</math> will not remain singular if <math>\mathcal{A}</math> is extended by a number of new and independent features. Even if we stick to the original set of pairwise options <math>\{a_i\} \cup \{(a_i)\}</math> to select a new basis, the sets of linear and positive propositions are determined by the choice of simple propositions, and this determination is tantamount to the conventional choice of a cell as origin. |
− | Second, the singular propositions '''B'''<sup>''n''</sup> <font face=symbol>'''××>'''</font> '''B''', picking out as they do a single cell or a coordinate tuple of '''B'''<sup>''n''</sup>, become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms '''B'''<sup>''n''</sup> and ('''B'''<sup>''n''</sup> <font face=symbol>'''××>'''</font> '''B''') and infects the whole hierarchy of types built on them. In plainer language, the terms that signify the interpretations ''x'' : '''B'''<sup>''n''</sup> and the singular propositions ''x'' : '''B'''<sup>''n''</sup> <font face=symbol>'''××>'''</font> '''B''' are fully equivalent in information, and this means that every | + | Second, the singular propositions <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B},</math> picking out as they do a single cell or a coordinate tuple <math>\mathbf{x}</math> of <math>\mathbb{B}^n,</math> become the carriers or the vehicles of a certain type-ambiguity that vacillates between the dual forms <math>\mathbb{B}^n</math> and <math>(\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B})</math> and infects the whole hierarchy of types built on them. In other words, the terms that signify the interpretations <math>\mathbf{x} : \mathbb{B}^n</math> and the singular propositions <math>\mathbf{x} : \mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}</math> are fully equivalent in information, and this means that every token of the type <math>\mathbb{B}^n</math> can be reinterpreted as an appearance of the subtype <math>\mathbb{B}^n \xrightarrow{\mathbf{x}} \mathbb{B}.</math> And vice versa, the two types can be exchanged with each other everywhere that they turn up. In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples. |
− | token of the type '''B'''<sup>''n''</sup> can be reinterpreted as an appearance of the subtype '''B'''<sup>''n''</sup> <font face=symbol>'''××>'''</font> '''B'''. And vice versa, the two types can be exchanged with each other everywhere that they turn up. In practical terms, this allows the use of singular propositions as a way of denoting points, forming an alternative to coordinate tuples. | |
| For example, relative to the universe of discourse [''a''<sub>1</sub>, ''a''<sub>2</sub>, ''a''<sub>3</sub>] the singular proposition ''a''<sub>1</sub> ''a''<sub>2</sub> ''a''<sub>3</sub> : '''B'''<sup>3</sup> <font face=symbol>'''××>'''</font> '''B''' could be explicitly retyped as ''a''<sub>1</sub> ''a''<sub>2</sub> ''a''<sub>3</sub> : '''B'''<sup>3</sup> to indicate the point <font face=system>‹1, 1, 1›</font>, but in most cases the proper interpretation could be gathered from context. Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points. When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity. | | For example, relative to the universe of discourse [''a''<sub>1</sub>, ''a''<sub>2</sub>, ''a''<sub>3</sub>] the singular proposition ''a''<sub>1</sub> ''a''<sub>2</sub> ''a''<sub>3</sub> : '''B'''<sup>3</sup> <font face=symbol>'''××>'''</font> '''B''' could be explicitly retyped as ''a''<sub>1</sub> ''a''<sub>2</sub> ''a''<sub>3</sub> : '''B'''<sup>3</sup> to indicate the point <font face=system>‹1, 1, 1›</font>, but in most cases the proper interpretation could be gathered from context. Both notations remain dependent on a particular basis, but the code that is generated under the singular option has the advantage in its self-commenting features, in other words, it constantly reminds us of its basis in the process of denoting points. When the time comes to put a multiplicity of different bases into play, and to search for objects and properties that remain invariant under the transformations between them, this infinitesimal potential advantage may well evolve into an overwhelming practical necessity. |