Minlog

We extract on the computer a number of moduli of uniform continuity for the first few elements of a sequence of closed terms t of G¨odel’s T of type (N→N)→(N→N). The generic solution may then be quickly inferred by the human. The automated synthesis of such moduli proceeds from a proof of the hereditarily extensional equality (≈) of t to itself, hence a proof in a weakly extensional variant of BergerBuchholz-Schwichtenberg’s system Z of t ≈(N→N)→(N→N) t. We use an implementation on the machine, in Schwichtenberg’s MinLog proof-system, of a non-literal adaptation to Natural Deduction of Kohlenbach’s monotone functional interpretation. This new version of the Monotone Dialectica produces terms in NbEnormal form by means of a recurrent partial NbE-normalization. Such partial evaluation is strictly necessary.

• Type: Conference
• Year: 2006
• Where: TPHOL
• Authors: Helmut Schwichtenberg
• Keywords: Artificial Intelligence, Extensional Equality, Moduli Proceeds, TPHOL 2006, Weakly Extensional Variant