Peter Schuster, Ideal Objects for Finite Methods
Ideal Objects for Finite Methods
Department of Pure Mathematics, University of Leeds, England
Somewhat miraculously, transfinite methods do work for proving quite a few theorems of a fairly finite nature. The corresponding ideal objects typically turn up towards a contradiction— and therefore do hardly exist. We aim at exploring and exploiting this phenomenon: by reducing transfinite proof methods to finite ones, and thus exhibiting the computational content of the virtually inexistent ideal objects. This is work in progress following a bottom-up strategy, i.e. from concrete examples taken from mathematical practice to a possible metamathematics.
First case studies have proved sucessful [1, 2]: several theorems that admit short and elegant proofs by contradiction but with Zorn’s Lemma have turned out to follow in a direct and elementary way from Raoult’s Open Induction , i.e. transfinite induction limited to Scott–open predicates. The extremal elements characteristic of Zorn’s Lemma are eliminated, and it is made possible to pass from classical to intuitionistic logic. If the theorem has finite input data, then a finite partial order carries the needed instance of induction, which thus only requires mathematical induction.
Besides the revised Hilbert Programme a la Kreisel and Feferman, inspirations come from the work on combinatorics by U. Berger and Coquand [4, 5]; from Coste, Lombardi, and Roy’s dy- namical algebra ; and from the interplay between pointwise and point-free topology in Sambin’s basic picture . There further are striking parallels to Maietti and Sambin’s two-level foundations with a forget-restore option [8, 9], and to Sambin’s appeal for allowing the use of ideal objects in real mathematics once this is approved by, say, appropriate conservativity [10, 11].
A PDF version of this abstract with references will be sent by mail to the Oberseminar list.