12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositional Equation Reasoning Systems (view source)
Revision as of 02:15, 16 August 2009
, 02:15, 16 August 2009→Variations on a theme of transitivity: TeX markup
Let us make the following definitions:
Let us make the following definitions:
{| align="center" cellpadding="8" width="90%"
|
<math>\begin{matrix}
P\ddagger & = & X_p & = & \{ \texttt{(} p \texttt{)}, p \},
\\[4pt]
Q\ddagger & = & X_q & = & \{ \texttt{(} q \texttt{)}, q \},
\\[4pt]
R\ddagger & = & X_r & = & \{ \texttt{(} r \texttt{)}, r \}.
\end{matrix}</math>
|}
An abstract reference to a point of ''X'' is a triple in '''B'''<sup>3</sup>. A concrete reference to a point of ''X'' is a conjunction of signs from the dimensions ''P''‡, ''Q''‡, ''R''‡, picking exactly one sign from each dimension.
These are three sets of two abstract signs each, altogether staking out the qualitative dimensions of the universe of discourse <math>X^\circ</math>.
Given this framework, the concrete type of the space <math>X\!</math> is <math>{P\ddagger} \times {Q\ddagger} \times {R\ddagger} \cong \mathbb{B}^3</math> and the concrete type of each proposition in <math>X^\uparrow = (X \to \mathbb{B})</math> is <math>{P\ddagger} \times {Q\ddagger} \times {R\ddagger} \to \mathbb{B}.</math> Given the length of the type markers, we will often omit the cartesian product symbols and write just <math>{P\ddagger}~{Q\ddagger}~{R\ddagger}.</math>
An abstract reference to a point of <math>X\!</math> is a triple in <math>\mathbb{B}^3.</math> A concrete reference to a point of <math>X\!</math> is a conjunction of signs from the dimensions <math>P\ddagger, Q\ddagger, R\ddagger,</math> picking exactly one sign from each dimension.
To illustrate the use of concrete coordinates for points and concrete types for spaces and propositions, Figure 35 translates the contents of Figure 33 into the new language.
To illustrate the use of concrete coordinates for points and concrete types for spaces and propositions, Figure 35 translates the contents of Figure 33 into the new language.