Premium
Dialectica interpretation of well‐founded induction
Author(s) -
Schwichtenberg Helmut
Publication year - 2008
Publication title -
mathematical logic quarterly
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.473
H-Index - 28
eISSN - 1521-3870
pISSN - 0942-5616
DOI - 10.1002/malq.200710045
Subject(s) - recursion (computer science) , interpretation (philosophy) , mathematics , term (time) , mathematical induction , combinatorics , calculus (dental) , discrete mathematics , algorithm , physics , computer science , quantum mechanics , geometry , medicine , dentistry , programming language
Abstract From a classical proof that the gcd of natural numbers a 1 and a 2 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)