A Logical Approach to Abstract Algebra

L APPROACH TO ABSTRACT ALGEBRA THIERRY COQUAND AND HENRI LOMBARDI Recent work in constructive mathematics show that Hilbert’s program works rge part of abstract algebra. Using in an essential way the ideas contained in the l arguments, we can transform a large number of abstract non effective proofs of “concrete” statements into 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.

• Type: Conference
• Year: 2005
• Where: CIE
• Authors: Thierry Coquand
• Keywords: Abstract Algebra, ALGEBRA THIERRY COQUAND, CIE 2005, Non Effective Proofs