Hostname: page-component-7c8c6479df-ws8qp Total loading time: 0 Render date: 2024-03-28T11:50:45.281Z Has data issue: false hasContentIssue false

A logical approach to abstract algebra

Published online by Cambridge University Press:  11 October 2006

THIERRY COQUAND
Affiliation:
Computer Science and Engineering, Chalmers University of Technology and Göteborg University, 412 96 Göteborg, Sweden Email: coquand@cs.chalmers.se
HENRI LOMBARDI
Affiliation:
Computer Science and Engineering, Chalmers University of Technology and Göteborg University, 412 96 Göteborg, Sweden Email: coquand@cs.chalmers.se

Abstract

Recent work in constructive mathematics shows 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 the highly abstract proofs of ‘concrete’ statements into elementary proofs. Surprisingly, the arguments we produce 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. For this we use a general method to transform some logically complex first-order formulae into a geometrical form, which may be interesting in itself.

Type
Paper
Copyright
2006 Cambridge University Press

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)