Changes

</pre>

</pre>

A piece of syntax like "(p (q))" or "''p'' &rArr; ''q''" is an abstract description, and abstraction is a process that loses information about the objects described.  So when we go to reverse the abstraction, as we do when we look for models of that description, there is a degree of indefiniteness that comes into play.

A piece of syntax like <math>{}^{\backprime\backprime} \texttt{(} p \texttt{(} q \texttt{))} {}^{\prime\prime}</math> or <math>{}^{\backprime\backprime} p \Rightarrow q {}^{\prime\prime}</math> is an abstract description, and abstraction is a process that loses information about the objects described.  So when we go to reverse the abstraction, as we do when we look for models of that description, there is a degree of indefiniteness that comes into play.

For example, the proposition (p (q)) is typically assigned the functional type '''B'''² &rarr; '''B''', but that is only its canonical or its minimal abstract type.  No sooner do we use it in a context that invokes additional variables, as we do when we next consider the proposition (q (r)), than its type is tacitly adjusted to fit the new context, for instance, acquiring the extended type '''B'''³ &rarr; '''B'''. This is one of those things that most people eventually learn to do without blinking an eye, that is to say, unreflectively, and this is precisely what makes the same facility so much trouble to implement properly in computational form.

For example, the proposition <math>\texttt{(} p \texttt{(} q \texttt{))}</math> is typically assigned the functional type <math>\mathbb{B}^2 \to \mathbb{B},</math> but that is only its canonical or its minimal abstract type.  No sooner do we use it in a context that invokes additional variables, as we do when we next consider the proposition <math>\texttt{(} q \texttt{(} r \texttt{))},</math> than its type is tacitly adjusted to fit the new context, for instance, acquiring the extended type <math>\mathbb{B}^3 \to \mathbb{B}.</math>  This is one of those things that most people eventually learn to do without blinking an eye, that is to say, unreflectively, and this is precisely what makes the same facility so much trouble to implement properly in computational form.

Both the fibering operation, that takes us from the function (p (q)) to the relation <nowiki>[|</nowiki> (p (q)) <nowiki>|]</nowiki>, and the tacit extension operation, that takes us from the relation <nowiki>[|</nowiki> (p (q)) <nowiki>|]</nowiki> &sube; '''B:B''' to the relation <nowiki>[|</nowiki> ''q''₂₀₇ <nowiki>|]</nowiki> &sube; '''B:B:B''' have this same character of abstraction-undoing or modelling operations that require us to re-interpret the same pieces of syntax under different types.  This accounts for a large part of the apparent ambiguities.

Both the fibering operation, that takes us from the function <math>\texttt{(} p \texttt{(} q \texttt{))}</math> to the relation <math>[| \texttt{(} p \texttt{(} q \texttt{))} |],</math> and the tacit extension operation, that takes us from the relation <math>[| \texttt{(} p \texttt{(} q \texttt{))} |] \subseteq \mathbb{B}:\mathbb{B}</math> to the relation <math>[| q_{207} |] \subseteq \mathbb{B}:\mathbb{B}:\mathbb{B},</math> have this same character of abstraction-undoing or modelling operations that require us to re-interpret the same pieces of syntax under different types.  This accounts for a large part of the apparent ambiguities.

Up till now I've concentrated mostly on the abstract types of domains and propositions, things like '''B'''^''k'' and '''B'''^''k'' &rarr; '''B''', respectively.  This is a little like trying to do physics all in dimensionless quantities without keeping track of the qualitative physical units.  So much abstraction has its obvious limits, not to mention its hidden dangers.

Up till now I've concentrated mostly on the abstract types of domains and propositions, things like <math>\mathbb{B}^k</math> and <math>\mathbb{B}^k \to \mathbb{B},</math> respectively.  This is a little like trying to do physics all in dimensionless quantities without keeping track of the qualitative physical units.  So much abstraction has its obvious limits, not to mention its hidden dangers.

To remedy this situation I will start to introduce the concrete types of domains and propositions, once again as they pertain to our current collection of examples.

To remedy this situation I will start to introduce the concrete types of domains and propositions, once again as they pertain to our current collection of examples.

We have been using the lower case letters ''p'', ''q'', ''r'' for the basic propositions of abstract type '''B'''³ &rarr; '''B''' and the upper case letters ''P'', ''Q'', ''R'' for the basic regions of the universe of discourse where ''p'', ''q'', ''r'' hold true, respectively.

We have been using the lower case letters <math>p, q, r\!</math> for the basic propositions of abstract type <math>\mathbb{B}^3 \to \mathbb{B}</math> and the upper case letters <math>P, Q, R\!</math> for the basic regions of the universe of discourse where <math>p, q, r,\!</math> respectively, hold true.

The set of signs <font face=calligrapher>X</font> = {"''p''", "''q''", "''r''"} is the ''alphabet'' for the universe of discourse that is notated as ''X''^&nbsp;&bull; = [<font face=calligrapher>X</font>] = [''p'', ''q'', ''r''], already getting sloppy about quotation marks to single out the signs.

The set of signs <font face=calligrapher>X</font> = {"''p''", "''q''", "''r''"} is the ''alphabet'' for the universe of discourse that is notated as ''X''^&nbsp;&bull; = [<font face=calligrapher>X</font>] = [''p'', ''q'', ''r''], already getting sloppy about quotation marks to single out the signs.