-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathinfinity.tex
295 lines (274 loc) · 14.1 KB
/
infinity.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
\section{Blending and the infinite}
\label{sec:infinity}
%\note{Marco, Ewen, Alan, Felix}
%In this paper we want to follow Goguen's proposal \cite{Go99c} for
%implementing blending, but slightly simplified (like in
%\cite{KuMoHoBhBa12}): we will only deal with
%the well-known notion of colimit in a category \cite{Gog91}, instead of
%using $\frac{3}{2}$-colimits.
%
%In the examples here considered we will be using colimits of V-shaped
%diagrams (cf.~Figure??). Thus, in each of the cases we have to specify
%two morphisms between a source conceptual space and a target conceptual
%space, with the restriction that both morphisms share the same source
%conceptual space.
%
%Additionally we will assume that the involved conceptual spaces are
%always given using a
%CASL specification \cite{MoHaSaTa08} and that the morphisms are theorem
%preserving (but perhaps not axiom preserving). The reason to these
%assumptions
%is that in these cases it is well-known how to compute colimits
%\cite{Mo98a}; the colimit specification essentially corresponds to the
%disjoint union of the two target conceptual spaces except for not
%repeating the symbols given in the common source conceptual space.
%Moreover, we will be using
%the HETS system \parencite{MossakowskiEA06} to compute such colimits.
%\subsection{Naturals and Integers}
\subsection{Example Revisited -- the Integers}
As a first demonstration of the machinery involved in blending
mathematical theories, we consider combining a theory of natural
numbers with the concept of the inverse of a function to obtain the
integers. Let us assume a simple partial axiomatisation of the natural
numbers (without order axioms) as shown in Listing \ref{fig:nats}, and
call this theory $\SIdIndex{Nat}$. Now let us also define a simple theory
which introduces the concept of a function with an inverse as shown in
Listing \ref{fig:inv}, and call this theory $\SIdIndex{Func}$.
\begin{listing}[!ht]
\begin{mdframed}
\begin{hetcasl}
\SPEC \=\SIdIndex{Nat} \Ax{=}\\
\> \SORT \Id{Nat}\\
\> \OPS \=\Id{zero} \Ax{:} \Id{Nat};\\
\>\> \Id{s} \Ax{:} \=\Id{Nat} \Ax{\rightarrow} \Id{Nat};\\
\>\> \Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{Nat} \Ax{\times} \Id{Nat} \Ax{\rightarrow} \Id{Nat}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{Nat} \\
%\> \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{y} \Ax{\wedge} \=\Id{s}(\Id{x}) \Ax{=} \Id{z} \Ax{\Rightarrow} \=\Id{y} \Ax{=} \Id{z}\\
\> \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{s}(\Id{y}) \Ax{\Rightarrow} \=\Id{x} \Ax{=} \Id{y}\\
%\> \Ax{\bullet} \=\Ax{\exists} \Id{a} \Ax{:} \Id{Nat} \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{a}\\
\> \Ax{\bullet} \Ax{\neg} \=\Id{zero} \Ax{=} \Id{s}(\Id{x}) \\
%\> \Ax{\bullet} \Ax{\neg} \=\Id{s}(\Id{x}) \Ax{=} \Id{zero}\\
\> \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{+} \Id{y} \Ax{=} \Id{s}(\=\Id{x} \Ax{+} \Id{y})\\
\> \Ax{\bullet} \=\Id{zero} \Ax{+} \Id{y} \Ax{=} \Id{y}\\
\KW{end}
\end{hetcasl}
\end{mdframed}
\caption{A theory of the natural numbers without order}
\label{fig:nats}
\end{listing}
\begin{listing}[!ht]
\begin{mdframed}
\begin{hetcasl}
\SPEC \=\SIdIndex{Func} \Ax{=}\\
\> \SORT \Id{X}\\
\> \OP \=\Id{f} \Ax{:} \=\Id{X} \Ax{\rightarrow} \Id{X}\\
\> \OP \=\Id{finv} \Ax{:} \=\Id{X} \Ax{\rightarrow} \Id{X}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{X} \\
\> \Ax{\bullet} \=\Id{f}(\Id{finv}(\Id{x})) \Ax{=} \Id{x}\\
\> \Ax{\bullet} \=\Id{finv}(\Id{f}(\Id{x})) \Ax{=} \Id{x}\\
\KW{end}
\end{hetcasl}
\end{mdframed}
\caption{A theory with a function and its inverse defined}
\label{fig:inv}
\end{listing}
\subsubsection{Identifying a Generic Space}
In order to incorporate the notion of blending here we want to be able
to identify a ``generic'' component of each theory and compute the
%colimit (also known as pushout).
colimit.
%as discusses in \S\ref{sec:background}.
We can use the
HDTP system \parencite{GustKS2006,Schmidt2010} to discover a common theory
and signature morphism between symbols in the
two theories $\SIdIndex{Nat}$ and $\SIdIndex{Func}$. The Generic theory
$\SIdIndex{Gen}$
contains a sort $\Id{N}$ and a function $\Id{func}$, and the morphisms from the
Generic theory to $\SIdIndex{Nat}$ and $\SIdIndex{Func}$ are:
\begin{align}
%s&&\leftarrow_{g_\SIdIndex{Nat}}&&func&&\rightarrow_{g_\SIdIndex{Func}}&&f\\
%Nat&&\leftarrow_{g_\SIdIndex{Nat}}&&N&&\rightarrow_{g_\SIdIndex{Func}}&&X
\Id{s}&&\leftarrow_{\phi(G,\SIdIndex{NAT})}&&\Id{func}&&\rightarrow_{\phi(G,\SIdIndex{FUNC})}&&\Id{f}\\
\Id{Nat}&&\leftarrow_{\phi(G,\SIdIndex{NAT})}&&\Id{N}&&\rightarrow_{\phi(G,\SIdIndex{FUNC})}&&\Id{X}
\end{align}
Here the successor function is identified in the mapping with the
function in the theory $\SIdIndex{Func}$.
%function in the theory $\SIdIndex{Func}$, and $g_K$ (where $K$ is either
%$\SIdIndex{NAT}$ or $\SIdIndex{FUNC}$) is the label for
%the set of symbol mappings determined by the signature morphism from
%the Generic space to the theory $K$.
\subsubsection{Computing the Colimit}
The HETS system \parencite{MossakowskiEA06} can then be exploited to
find a new theory by computing the colimit:
%%\begin{center}
%% \begin{diagram}[size=7mm]
%% & & $Gen$ & & \\
%% & \ldTo^{\rotatebox{-45}{$g_\SIdIndex{Nat}$}} & &
%% \rdTo^{\rotatebox{45}{$g_\SIdIndex{Func}$}} & \\
%% \SIdIndex{Nat} & & & & \SIdIndex{Func} \\
%% & \rdTo_{\rotatebox{45}{$b_\SIdIndex{Nat}$}} & &
%% \ldTo_{\rotatebox{-45}{$b_\SIdIndex{Func}$}} & \\
%% & & $Blend$ & &
%% \end{diagram}
%%\end{center}
%\begin{center}
% \begin{tikzcd}[column sep=normal, row sep=small]
% & \SIdIndex{Blend}
% \\
% \SIdIndex{NAT} \arrow{ur}{b_\SIdIndex{NAT}} & & \SIdIndex{FUNC}
% \arrow{ul}[swap]{b_\SIdIndex{FUNC}} \\
% & \SIdIndex{Gen} \arrow{ul}{g_\SIdIndex{NAT}}
% \arrow{ur}[swap]{g_\SIdIndex{FUNC}}
% \end{tikzcd}
%\end{center}
\begin{center}
\begin{tikzcd}[column sep=small, row sep=tiny]
& \SIdIndex{Blend}
\\
\SIdIndex{NAT} \arrow{ur} & & \SIdIndex{FUNC}
\arrow{ul} \\
& \SIdIndex{Gen} \arrow{ul}
\arrow{ur}
\end{tikzcd}
\end{center}
This generates the theory shown in Listing \ref{fig:inconsistentintegers}
(for the sake of understanding it is used $\Id{p}$, for predecessor, instead of $\Id{sinv}$).
\begin{listing}[!ht]
\begin{mdframed}
%\begin{hetcasl}
%\SPEC \=\SIdIndex{Spec} \Ax{=}\\
%\> \SORT \Id{N}\\
%\> \OP \=\Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{N} \Ax{\times} \Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{p} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{s} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{zero} \Ax{:} \Id{N}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{y} \Ax{\wedge} \=\Id{s}(\Id{x}) \Ax{=} \Id{z} \Ax{\Rightarrow} \=\Id{y} \Ax{=} \Id{z} \`{\small{}\KW{\%}(1)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{s}(\Id{y}) \Ax{\Rightarrow} \=\Id{x} \Ax{=} \Id{y} \`{\small{}\KW{\%}(2)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Ax{\exists} \Id{a} \Ax{:} \Id{N} \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{a} \`{\small{}\KW{\%}(3)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \Ax{\neg} \=\Id{s}(\Id{x}) \Ax{=} \Id{zero} \`{\small{}\KW{\%}(4)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{+} \Id{y} \Ax{=} \Id{s}(\=\Id{x} \Ax{+} \Id{y}) \`{\small{}\KW{\%}(5)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{zero} \Ax{+} \Id{y} \Ax{=} \Id{y} \`{\small{}\KW{\%}(6)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{p}(\Id{x})) \Ax{=} \Id{x} \`{\small{}\KW{\%}(1\Ax{\_}7)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet}
%\=\Id{p}(\Id{s}(\Id{x})) \Ax{=} \Id{x}
%\`{\small{}\KW{\%}(2\Ax{\_}8)\KW{\%}}\\
%\KW{end}
%\end{hetcasl}
\begin{hetcasl}
\SPEC \=\SIdIndex{Spec} \Ax{=}\\
\> \SORT \Id{N}\\
\> \OP \=\Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{N} \Ax{\times} \Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{p} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{s} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{zero} \Ax{:} \Id{N}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{y} \Ax{\wedge} \=\Id{s}(\Id{x}) \Ax{=} \Id{z} \Ax{\Rightarrow} \=\Id{y} \Ax{=} \Id{z} \`{\small{}\KW{\%}(1)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{x}) \Ax{=} \Id{s}(\Id{y}) \Ax{\Rightarrow} \=\Id{x} \Ax{=}
\Id{y}\\% \`{\small{}\KW{\%}(1)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Ax{\exists} \Id{a} \Ax{:} \Id{N} \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{a} \`{\small{}\KW{\%}(3)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \Ax{\neg}
\=\Id{zero} \Ax{=} \Id{s}(\Id{x})\\% \`{\small{}\KW{\%}(2)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \Ax{\neg} \=\Id{s}(\Id{x}) \Ax{=} \Id{zero} \`{\small{}\KW{\%}(2)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{x}) \Ax{+} \Id{y} \Ax{=} \Id{s}(\=\Id{x} \Ax{+} \Id{y})\\% \`{\small{}\KW{\%}(3)\KW{\%}}\\
\> \Ax{\forall} \=\Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{zero} \Ax{+}
\Id{y} \Ax{=} \Id{y}\\% \`{\small{}\KW{\%}(4)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{p}(\Id{x})) \Ax{=} \Id{x}\\% \`{\small{}\KW{\%}(1\Ax{\_}5)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{p}(\Id{s}(\Id{x})) \Ax{=} \Id{x}\\% \`{\small{}\KW{\%}(2\Ax{\_}6)\KW{\%}}\\
\KW{end}
\end{hetcasl}
\end{mdframed}
\caption{An inconsistent partial approach to the integers (without order)}
\label{fig:inconsistentintegers}
\end{listing}
\subsubsection{Removal of Inconsistencies}
This theory is automatically determined to be inconsistent due to the axioms
\begin{equation}
\forall x : \mathbb{Z} . \neg \:\: \Id{zero} = \Id{s}(x)
\label{eq:limnat1}
\end{equation}
\begin{equation}
\forall x : \mathbb{Z} . \:\: \Id{s} (\Id{p}(x)) = x
\label{eq:sucpre}
\end{equation}
%\begin{eqnarray}
%%\forall x : \mathbb{Z} . \neg s(x) &=& 0 \label{eq:limnat1}\\
% \forall x : \mathbb{Z} . \neg \: \Id{zero} &=& \Id{s}(x) \label{eq:limnat1}\\
% \forall x : \mathbb{Z} . \: \Id{s} (\Id{p}(x)) &=& x \label{eq:sucpre}
%\end{eqnarray}
%Removal from Listing~\ref{fig:nats} of the limiting axiom (\ref{eq:limnat1})
Removal
of the limiting axiom (\ref{eq:limnat1})
from Listing~\ref{fig:nats}
%Removal from Listing~\ref{fig:nats} of the axiom
%%$\forall x. \neg \: 0 = s(x)$
%%$\forall x. \neg \: \Id{zero} = s(x)$
%$\forall x: \Id{Nat}. \neg \: \Id{zero} = s(x)$
results in generating a blend theory which is very
similar to what we understand to be the integers as shown in
Listing~\ref{fig:integers}.
\begin{listing}[!ht]
\begin{mdframed}
%\begin{hetcasl}
%\SPEC \=\SIdIndex{Spec} \Ax{=}\\
%\> \SORT \Id{N}\\
%\> \OP \=\Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{N} \Ax{\times} \Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{p} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{s} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
%\> \OP \=\Id{zero} \Ax{:} \Id{N}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{y} \Ax{\wedge} \=\Id{s}(\Id{x}) \Ax{=} \Id{z} \Ax{\Rightarrow} \=\Id{y} \Ax{=} \Id{z} \`{\small{}\KW{\%}(1)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{s}(\Id{y}) \Ax{\Rightarrow} \=\Id{x} \Ax{=} \Id{y} \`{\small{}\KW{\%}(2)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Ax{\exists} \Id{a} \Ax{:} \Id{N} \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{a} \`{\small{}\KW{\%}(3)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{+} \Id{y} \Ax{=} \Id{s}(\=\Id{x} \Ax{+} \Id{y}) \`{\small{}\KW{\%}(4)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{zero} \Ax{+} \Id{y} \Ax{=} \Id{y} \`{\small{}\KW{\%}(5)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{p}(\Id{x})) \Ax{=} \Id{x} \`{\small{}\KW{\%}(1\Ax{\_}7)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{p}(\Id{s}(\Id{x})) \Ax{=} \Id{x} \`{\small{}\KW{\%}(2\Ax{\_}8)\KW{\%}}\\
%\KW{end}
%\end{hetcasl}
\begin{hetcasl}
\SPEC \=\SIdIndex{Spec} \Ax{=}\\
\> \SORT \Id{N}\\
\> \OP \=\Ax{\_\_}\Ax{+}\Ax{\_\_} \Ax{:} \=\Id{N} \Ax{\times} \Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{p} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{s} \Ax{:} \=\Id{N} \Ax{\rightarrow} \Id{N}\\
\> \OP \=\Id{zero} \Ax{:} \Id{N}\\
%\> \Ax{\forall} \=\Id{x}, \Id{y}, \Id{z} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{y} \Ax{\wedge} \=\Id{s}(\Id{x}) \Ax{=} \Id{z} \Ax{\Rightarrow} \=\Id{y} \Ax{=} \Id{z} \`{\small{}\KW{\%}(1)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{x}) \Ax{=} \Id{s}(\Id{y}) \Ax{\Rightarrow} \=\Id{x} \Ax{=}
\Id{y}\\% \`{\small{}\KW{\%}(1)\KW{\%}}\\
%\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Ax{\exists} \Id{a} \Ax{:} \Id{N} \Ax{\bullet} \=\Id{s}(\Id{x}) \Ax{=} \Id{a} \`{\small{}\KW{\%}(3)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x}, \Id{y} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{x}) \Ax{+} \Id{y} \Ax{=} \Id{s}(\=\Id{x} \Ax{+} \Id{y})\\% \`{\small{}\KW{\%}(2)\KW{\%}}\\
\> \Ax{\forall} \=\Id{y} \Ax{:} \Id{N} \=\Ax{\bullet} \=\Id{zero} \Ax{+}
\Id{y} \Ax{=} \Id{y}\\% \`{\small{}\KW{\%}(3)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{s}(\Id{p}(\Id{x})) \Ax{=} \Id{x}\\% \`{\small{}\KW{\%}(1\Ax{\_}4)\KW{\%}}\\
\> \Ax{\forall} \=\Id{x} \Ax{:} \Id{N} \=\Ax{\bullet}
\=\Id{p}(\Id{s}(\Id{x})) \Ax{=} \Id{x}\\% \`{\small{}\KW{\%}(2\Ax{\_}5)\KW{\%}}\\
\KW{end}
\end{hetcasl}
\end{mdframed}
\caption{A consistent partial approach to the integers (without order)}
\label{fig:integers}
\end{listing}
\subsubsection{Running the Blend}
% Running the blend refers to discovering axioms or definitions which
% make the blend incomplete.
Running the blend refers to discovering definitions or adding axioms
to flesh out the blend. In the example of the version in Listing
\ref{fig:integers}, the definition of plus needs to be extended to
understand how to calculate with the predecessor function:
$$
p(x) + y = p(x+y)
$$
\noindent from which theorems such as
$$
p(x) + s(y) = x+y
$$
\noindent can be proved.
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "mathsICCC"
%%% End: