Hostname: page-component-745bb68f8f-s22k5 Total loading time: 0 Render date: 2025-02-01T17:06:28.272Z Has data issue: false hasContentIssue false
  • English
  • Français

A logical approach to abstract algebra

Published online by Cambridge University Press:  11 October 2006

THIERRY COQUAND  and
HENRI LOMBARDI
THIERRY COQUAND
Affiliation:
Computer Science and Engineering, Chalmers University of Technology and Göteborg University, 412 96 Göteborg, Sweden Email: [email protected]
HENRI LOMBARDI
Affiliation:
Computer Science and Engineering, Chalmers University of Technology and Göteborg University, 412 96 Göteborg, Sweden Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

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
Information
Mathematical Structures in Computer Science , Volume 16 , Issue 5 , October 2006 , pp. 885 - 900
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.)