The Mathematician's Algorithm & Automated Theory Generation
Mark
to closely capture the process a mathematician goes through in developing
a mathematical theory. In it, you see the concepts of conjectures,
counter-examples and theorems emerge quite naturally.
The term "algorithm" is used somewhat loosely. The steps described herein
need not all be computeable. Nonetheless, the process described provides
an enveloping framework for computational approximations to the 'algorithm'
and also provides the basis for processes that only carry out partial
automation (i.e., computer-aided theory generation).
Contents:
(1) General Description
(2) The Boolean Sieve
(3) Incremental Updates
(4) Initializations
(5) The Algorithm
(6) Theory Generation
(7) Exercises
(A) Derivation of Lattice Theory
(B) Derivation of Abstract Algebra
(1) General Description
Consider the case where we have a set, N, of statements, a set M of
models over the underlying term language, and a set T of theorems
each taking the form of a valid Horn clause formed out of statements
from N.
Let B(N) denote the semantic lattice generated by N and L(N) the free
lattice generated by N. The basic assertion of Proof Theory is that
the natural homomorphism:
a: L(N) -> B(N)
will factor through the quotient lattice L(N)/T:
a = (a/T) . T'
T': L(N) -> L(N)/T;
a/T: L(N)/T -> B(N).
For any g in L(N) and model m, let m'(g) = 1 or 0 depending respectively
on whether m |= g or m |= ~g. Then m' maps L(N) to the boolean lattice
2 = 2^{m}.
Likewise, if M is a set of models, let M': L(N) -> 2^M be defined by
M'(g) = (m'(g): m in M)
Let L(M; N) denote the image of L(N) under the map M'.
The basic assertion of Model Theory is that the homomorphism M': L(N)->L(M;N)
factors through the semantic lattice B(N):
M' = M* . a
a: L(N) -> B(N)
M*: B(N) -> L(M; N).
----------------------------------------
(2) The Boolean Sieve
The net result is that we have a net of homomorphisms:
L(N) -- T' --> L(N)/T -- a/T --> B(N) -- M* --> L(M; N)
that successively approximate B(N) between tighter and tighter
bounds as the sets N and T grow. These bounds converge: as T -> Th(N),
the theory generated by N, then L(N)/T -> B(N); and as M approaches
the class of all models over the underlying term language, then
L(M; N) -> B(N). In general L(N)/T will be monotonically "increasing" in T,
and L(M; N) will be monotonically "decreasing" in M.
The gap between the bounds is represented by the homomorphism
f(M,T): L(N)/T -> L(M; N)
which is, in turn, characterized by the filter:
f(M,T)^{-1}(1^M), subset of L(N)/T.
This filter can be represented as a filter over L(N) modulo T:
f(M,T)^{-1}(1^M) = M'^{-1}(1^M) / T
The filter is, in turn, a prime filter generated by a statement S:
M'^{-1}(1^M) = S^ = { u in L(N): u >= S }
where >= is the lattice ordering. So, writing S in the form:
S = c1 & c2 & ... & cq = & C
where C = {c1,c2,...,cq}
& is the lattice join
we have a set of CONJECTURES that mediates between the gap.
Together, this comprises what I call a BOOLEAN SIEVE.
----------------------------------------
(3) Incremental Updates
Since L(N)/T and L(M; N) are monotonic in T and M respectively, then C
can be efficiently maintained by providing a suitable update formula
corresponding to each increment in T or M.
The statements in C are already taken relative to T,
T |- c, for each c in C.
So, in actuality, we're only seeking an update method for increments in M.
At the same time, the contents of C direct the update process, itself.
For each c in C, we attempt to either find a proof of the inference
T |- c,
itself, or a model m which provides a counter-example to c:
m |= not c.
In the former case, we can safely remove c from the set C and add it
to T. It then represents a conjecture that has been proven as a
theorem. In the latter case, we add the model m to M and then the task
is to update C, itself.
The general properties relating the net f_M = M'^{-1}(1^M) of filters are:
f_M(N) = s(M; N)^ = { u in L(N): u >= s(M; N) }
s(M1 union M2; N) = s(M1; N) v s(M2; N)
s({m}; N) = s(m, N)
where v is the lattice join; and
s(m; N) = & (c: c in N, m |= c) & & (not c: c in N, m |= not c }.
Thus, if the generating statement s(M; N) = c1 & ... & cq = &C, where
C = {c1, ..., cq}, then the updated statement will be:
s(M union {m}; N) = (c1 & ... & cq) v m(C).
This reduces to the expression:
& (c: c in N, m |= c) &
& (c v c': m |= (not c), m |= c') &
& (c' -> c: m |= (not c), m |= (not c')).
So, the set C is modified as follows:
* We take each c in C for which m |= not c and remove it.
It is a conjecture refuted by the model m, which then
provides us with a counter-example to c.
* We replace c by the formulas
c v c', for all c' in C for which m |= c'
c' -> c, for all c' in C for which m |= not c'
adding one such formula to the updated C for each c' in C.
* We reduce C, carrying out basic simplifications and removing
all the redundant statements.
When c is a Horn clause c = &G -> vH, then the updated formulas would
be (in Classical logic) respectively:
(c' -> c) = &({c'} union G) -> V H
(c v c') = G -> V (H union {c'})
The updating preserves the requirement that the filter corresponding to the
homomorphism L(N)/T -> L(M; N) be the subset (&C)^/T of L(N)/T.
----------------------------------------
(4) Initializations
By presumption, our exploration starts out with a concrete application.
So, that means the initial set N of statements comprise all those statements
that are true in the application at hand. If the model corresponding to
this application is m0, then the initial values for C, T and M will be:
C = N, T = {} and M = {m0}.
Since m0 |= n for all n in N, then m0 |= c, for all c in N. Therefore,
s({m0}; N) = &N.
So, the filter corresponding to the homomorphism
L(N) = L(N)/{} -> L({m0}; N)
is just
(&N)^ = (&N)^/{}.
Therefore, with this initialization and the update previously described,
the filter for the homomorphism L(N)/T -> L(M; N) will always be
(&C)^/T.
----------------------------------------
(5) The Algorithm
So, in summary, the algorithm takes on the following form:
GIVEN:
A set N of statements and a model m0 of the underlying term language
such that m0 |= n, for all n in N.
INITIALIZATION:
Set C = N, T = {} and M = {m0}.
UPDATING:
Pick any c0 in C for which either a proof of T |- c0 can be found
or a counter-example m |= not c0.
If T |- c0, then remove c0 from C and add it to T.
If m |= not c0, then add m to M and for each c in C for which m |= not c:
remove c from C
for all c' in C for which m |= c', add (c v c') to C
for all c' in C for which m |= not c', add (c' -> c) to C.
Repeat the update process, reducing C as far as possible.
----------------------------------------
(6) Theory Generation
The set M is ancillary to the algorithm, itself and doesn't need to be
explicitly represented in any form, but is useful to retain as it provides
a catalogue of all the relevant counter-examples.
If C can be reduced to {}, then the set T will provide a complete
characterization of all the logical interrelations that exist amongst the
original set N of statements. From this one can:
(a) read off an axiomatization by taking any minimal subset N0
of N from which N can be generated via the Horn clauses in T
(b) read off all the significant "watersheds" -- subsets of N
which are generated by a large number of different (and usually
much smaller still) subsets.
(c) classify ALL the generalizations -- that is, all the subsets of N
which are closed under T.
So, the net result is that one not only arrives at a theory that formalizes
the statements of interest from the original application but (even more
significantly) a hierarchical classification of the significant
generalizations to this theory.
----------------------------------------
(7) Exercises
The method described is most suitable for application to algebraic
theories. Two useful exercises one may attempt are the following:
(A) Derivation of Lattice Theory
Starting out with the model
{0,1}; AND, OR, NOT, IF-THEN, IFF
with the connectives defined by the standard truth tables
write down a large set of identities (e.g., the set of all the equational
identities that comprise up to 4 variables on the left and 4 on
the right). From this carry out the reduction process to find the
interrelations and from this the significant watersheds.
>From this, one should be able to read off the watersheds corresponding
to Heyting lattices, distributive lattices, modular lattices, etc.
(B) Derivation of Abstract Algebra
Similar exercise, starting out with the model
Q = rational numbers & the arithmetic operations +, -, *, /.
>From this, the structures corresponding to group theory, ring theory,
semigroups, monoids, semirings, etc. should all emerge naturally as
watersheds.
Using this method on the starting structure:
(G, binary -); (G, +, 0, unary -) = Abelian group; a-b = a+(-b)
for instance, one finds the following axiomatizations:
Abelian groups: a-(b-c) = c-(b-a); a-(a-b); 0-0 = 0
Non-abelian groups: a/1 = a; a/a = 1; (a/c)/(b/c) = a/b
and several other interesting equivalent axiomatizations for non-abelian
groups (for Abelian groups, the axiom 0-0 = 0 can be equivalently
replaced by the axiom that the group simply be non-empty).
Mark
>Let B(N) denote the semantic lattice generated by N and L(N) the free
>lattice generated by N. The basic assertion of Proof Theory is that
>the natural homomorphism:
> a: L(N) -> B(N)
>will factor through the quotient lattice L(N)/T:
> a = (a/T) . T'
> T': L(N) -> L(N)/T;
> a/T: L(N)/T -> B(N).
These are meant to be Boolean lattices, so L(N) is the
free Boolean lattice 2^{2^N} generated by N. The homomorphisms
mentioned throughout are Boolean lattice homomorphisms.
I don't know if there is an analogous construction, say, for
Heyting lattices (i.e., a "Heyting sieve"). That, I suppose,
could be posed as a question here.