Applications of proof interpretations in nonlinear analysis

For enkelthets skyld tar jeg her utgangspunkt i den populærvitenskapelige framstillingen fra prosjektets forrige framdriftsrapport (med rapporteringsfrist 20111001) som kjent bakgrunnsstoff. Hovedsaklig har jeg i perioden etter dette arbeidet med å vide reutvikle funksjonalinterpretasjonen for ikke-standard aritmetikk i alle endelige typer (Dst-interpretasjonen), noe som er et (uformelt) samarbeid med Benno van den Berg fra universitetet i Amsterdam og Pavol Safarik fra det tekniske universitetet i Dar mstadt. En viktig del av arbeidet har vært å finne ut av om Dst-interpretasjonen lar seg anvende også på svakere logiske systemer enn de som bygges over full Peano-aritmetikk i alle endelige typer -- eksempelvis systemer med svært begrensete former for in duksjonsaksiomer. Vi fant at ved å finjustere Dst-interpretasjonen på visse tekniske måter kunne vi behandle også slike systemer. Dette er relevant for anvendelser av disse Proof Mining-teknikkene innen andre deler av matematikken fordi vi derved ser at D st-interpretasjonen ikke skaper "unødig kompleksitet": Hvis et bevis for et passelig teorem er formalisert i et svakt system vil Dst-interpretasjonen finne relevant kvantitativ informasjon som vokser forholdsmessig langsomt -- bare hvis beviset er formali sert i et sterkt system kan det skje at den kvantitative informasjonen "eksploderer i kompleksitet". Videre har vi også gått i diametralt motsatt retning: I stedet for å se på svakere systemer har vi da sett på logiske prinsipper som ville gi enda sterker e systemer -- og har undersøkt om Dst-interpretasjonen kan håndtere også disse. Spesifikt har vi vært interessert i et ikke-effektivt prinsipp som kalles "Weak König's Lemma", og også såkalte satureringsprinsipper. Disse spiller en viktig rolle i ikke-sta ndard analyse, spesielt fordi de tilsynelatende er sentrale i konstruksjonen av Loeb-mål, som igjen er viktige i mange av de mest slående anvendelsene av ikke-standard analyse. Vi har klart å utvide interpretasjonen til å også gjelde for Weak König's Lemm a kombinert med klassisk logikk, og også et tellbart satureringsprinsipp kombinert med intuisjonistisk logikk. Derimot er det fremdeles uklart om interpretasjonen kan hanskes med tellbare satureringsprinsipper kombinert med klassisk logikk. Arbeidet me d Dst-interpretasjonen er nært knyttet til prosjektets mål om å studere situasjoner der teoremer som grovt sett er på formen "for alle x finnes en y slik at for alle z gjelder A(x,y,z)" kan behandles som de fundamentalt enklere tilfellene "for alle x finn es en y slik at A(x,y)" når det gjelder å finne kvantitativ informasjon. Enkelt sagt bunner denne sammenhengen i at vi i de ikke-standard logiske systemene skiller mellom "alle z" og "alle standard z", og bare det siste får konsekvenser for ekstraksjonen av kvantitativt innhold. Utover dette har jeg som anvendelser av Proof Mining-teknikker arbeidet med å finne eksplisitte konvergensrater for to typer selvavbildninger på henholdsvis Hilbertrom og generelle metriske rom. Den første klassen selvabildning er er en type sterke pseudokontraksjoner med et unikt fikspunkt, men her har jeg bare svært foreløpige resultater. Den andre klassen, der resultatene er mer tilfredstillende, er en viss type generaliserte kontraksjoner, også disse med et unikt fikspunkt.

The project will be connected to proof mining as developed by Kohlenbach et al. since the 1990s. Proof mining concerns the analysis of given mathematical proofs using proof-theoretic tools and insights, with the aim of obtaining new information such as ef fective bounds or rates of convergence. The main areas of application have been nonlinear functional analysis, approximation theory, and ergodic theory, and recent metatheorems by Kohlenbach/Gerhardy concerning formal systems for analysis with various abs tract spaces as new ground types make possible the extraction of effective bounds from ineffective proofs of for-all-exist-statements s.t. the bounds are uniform in all parameters except through certain local bounds. These results can be used e.g. to obta in effective rates of metastability (in the sense of Tao) for iteration sequences, but not easily full rates of convergence - which is in general impossible. This reflects the fundamental difference between for-all-exist-for-all-statements and for-all-exi st-statements when it comes to obtaining effective bounds, and this situation obtains in many areas of mathematics. We have earlier nonetheless constructed explicit full rates of convergence for Picard iteration sequences of selfmaps of metric spaces in t wo case studies where there is convergence to a unique fixed point, and we gave an explanation for this (restricted to the bounded case) in the form of general conditions under which we in this setting can transform a for-all-exist-for-all-statement into a for-all-exist-statement via an argument involving product spaces. We aim mainly to clarify to what extent this approach can be lifted out of the particular setting of Picard iteration sequences in bounded metric spaces converging to a unique fixed point . Establishing nontrivial conditions under which a for-all-exist-for-all-statement behaves like a for-all-exist-statement is highly desirable in many areas of mathematics with respect to extracting effective bounds.