All,

I'm trying to understand how a unification engine works by designing
and programming a simple one.

I'm trying to avoid tree or list data structures in favor of matrices
for the sake
of speed. What I have so far is this:

Suppose I have a set of terms T0 through Tn. Let predicate P of any
two
terms be represented by a 2D bitmap whose axes are enumerated 0
through n. Let predicates Q and R be similar bitmaps distinct from
P
and each other.

Then I state as facts: P(T0,T1). Q (T1, T0). R(T1, T1).

Thus the bitmap representing predicate P would then have the bit at
intersection 0,1 raised, the one representing Q would be raised
at intersection 1,0 and the one representing R would be raised
at intersection 1, 1.

I suppose the primitive recursive functions are supposed
to be those functions that provably terminate, is that right?
But there are functions that are not primitive recursive
that provably terminate.

It seems like the more useful approach would be just
to speak in terms of what provably terminates. That's
the important quality, is it not? For example, structurally
recursive functions provably always terminate, but I don't
see that they meet the definition of primitive recursive.
Any function with an algorithm that is recursive, has a
nonrecursive base case, and for which an order exists
for some subset of its arguments, such that recursive
invocations of the function (i.e., not the base case) uses
arguments that are strictly less than the previous invocation,
and whose domain is a set of elements greater than or
equal than the base case, provably terminates. This
is old hat stuff, but isn't covered by "primitive recursive."

Michael Potter(Cambridge)recently gave a talk entitled 'where does
arithmetic fit into transcendental philosophy?' He drew a diagram
showing three concentric rings. In the centre he wrote 'monadic logic',
in the next ring he wrote 'diadic logic', in the outer ring he wrote
'arithmetic'.

What does he mean by monadic and diadic logic, and why would they be
drawn so? Any other observations?

I was reading through the presentation of Simon Thomas
on a result in descriptive set theory of finitely generated groups.

On page 5 of:
< http://www.math.rutgers.edu/~sthomas/oxford-short.pdf >,

a standard Borel space is defined as a complete separable
metric space equipped with its sigma-algebra of Borel subsets.

So some examples of standard Borel spaces would be:

(a) X = metric space [0, 1], where the usual metric gives the topology for
the metric space and the sigma-algebra generated by the open
subsets of [0, 1].

(b) Y = lR (the reals) , proceeding as in (a)

(c) R^2, R^3 and so on.

According to a well-known theorem of Kuratowski,

if (X, S) is an uncountable standard Borel
space, then (X, S) is measurably isomorphic
to the unit interval [ 0, 1] equipped with
its sigma-algebra of Borel sets.
[ Note: S a sigma-algebra on X]