Dialectica interpretation of well‐founded induction
Helmut Schwichtenberg · Mathematical logic quarterly · 2008
Abstract From a classical proof that the gcd of natural numbers a1 and a2 is a linear combination of the two, we extract by Gödel's Dialectica interpretation an algorithm computing the coefficients. The proof uses the minimum principle. We show generally how well‐founded recursion can be used to Dialectica interpret well‐founded induction, which is needed in the proof of the minimum principle. In the special case of the example above it turns out that we obtain a reasonable extracted term, representing an algorithm close to Euclid's. (© 2008 WILEY‐VCH Verlag GmbH & Co. KGaA, Weinheim)