>> A lot of algebra is *not* done within algebraic theories.
In fact, I would say, *most* algebra.
...........
>> Hall's universe of discourse is obviously set theory.
actually, finite set theory, for the most part.
Most of the deep results of group theory are about finite groups,
and can be proved in PRA -- e.g., in nqthm, in principle.
Has anyone tried this on nqthm?
I think this area illustrates why it's hard to formalize mathematics.
Take something simple, like the Sylow theorems.
The proofs are short enough, in "human" terms, but involve
all sorts of "trivial" reasoning about numbers and finite sets,
and it would take a long time to explain this all formally.
You can't really modularize mathematics, as Victor Yodaiken seems to suggest:
>> Why not mechanize algebra, rather than logic or set theory?
If you want to verify a large chunk of mathematics, not just an
isolated result here and there, you need to formalize something like ZFC.
There's nothing sacred about the precise system ZFC;
much weaker systems will suffice for most of mathematics,
whereas some people might prefer stronger theories
(e.g., Mizar adds some inaccessible cardinals for convenience).
But to verify many of the standard results in real analysis, for
example, we have to be able to talk about real numbers, and sets of real
numbers, and sequences of real numbers, and functions on the real numbers.....
So, we need a theory strong enough to construct these objects.
Victor Yodaiken also says:
>> Philosophical aside. The idea that one can and should develop
>> a mathematical system from a small set of axioms and deduction rules
>> in place of an untidy mix of principles derived from physics and
>> arithmetic is not necessarily a correct idea.
Actually, such an "untidy mix" describes very well how humans learn
mathematics, and think about it.
Humans also make a lot of mistakes.
If we want a system that people will believe in, it has
to be founded on a clear and simple set of basic principles.
That is one advantage of set theory. We can start with simple
basic principles, and any "untidy mix" of functions, sequences, numbers,
pairs, etc., can all be constructed within the theory, as needed.
Ken Kunen