A logical approach to abstract algebra
A logical approach to abstract algebra.
with Thierry Coquand.
Math. Struct. in Comput. Science
16, (2006), 885-900.
Recent work in constructive mathematics show that Hilbert's program works
for a large part of abstract algebra. Using in an essential way the ideas
contained in the classical arguments, we can transform most of highly
abstract proofs of "concrete" statements in elementary proofs.
Surprisingly the arguments we get are not only elementary but also
mathematically clearer and not necessarily longer. We present an example
where the simplification was significant enough to suggest an improved
version of a classical theorem.