## Hilbert's program vindicated

### Programma

Proof theory has its origin in what has been called ‘Hilbert’s program’: Since the 19th century noneffective and nonfinitary (set-theoretic) principles became increasingly important which raised the issue of their legitimacy. Hilbert’s approach was to establish the consistency of a suitable formalization T of mathematics (first number theory and then analysis and set theory) within some finitary reasoning FIN. This would then imply that any purely universal number theoretic (‘real’) statement which is provable in T would already be provable in FIN. So nonconstructive (‘ideal’) elements in proofs of real statements could in principle be eliminated. Hilbert already and then later, in particular, Kreisel considered the broader goal to achieve this for more general statements such as ∀∃-statements φ in number theory (i.e. Π^0_2-statements). In fact, the proof-theoretic tools developed in the course of the consistency program by Hilbert and his school extract - as was hightlighted first by Kreisel - explicit algorithms p witnessing the existential quantifier in φ from a proof of φ in - say - Peano arithmetic PA. Whereas often Hilbert’s concept of finitary reasoning FIM
is identified with primitive recursive arithmetic PRA, Hilbert himself saw in 1925 that an extension of PRA to the primitive recursive functionals of finite types (nowadays called Godel’s T) is necessary already for number theory and in 1941 Godel showed by means of his functional interpretation that any proof of a theorem (of any complexity) in Peano arithmetic PA allows for a suitable algorithmic reading in terms of T.

In this talk we view Hilbert’s program in this applied form due to Kreisel as the program to eliminate ideal elements from proofs of computationally meaningful statements with the goal of extracting explicit numerical information such as bounds etc. In fact, already in the larger Hilbert school, this was approached e.g. in the context of abstract algebra in Grete Hermann’s dissertation (written under the supervision of Emmy Noether).
Since 1990, the author has launched the program of ‘proof mining’ which aims to achieve this for large parts of (mainly nonlinear) analysis such as fixed point theory, ergodic theory, abstract Cauchy problems and nonsmooth optimization. In more than 100 case studies carried out by many authors it has turned out that even proofs which prima facie use highly nonconstructive tools allow for the extraction of explicit effective bounds which not only are (in all cases so far) definable in Godel’s
T but usually even of very low complexity going down in important situations to polynomial and - most recently - even linear bounds. We will discuss this ‘proof-theoretic tameness’ of large parts of ordinary mathematics and provide a couple of examples which show the general spirit of proof mining as an applied form of Hilbert’s program.

### Dettagli sull'evento

#### Data e luogo

Inizio: 24/05/2023 alle ore 11:00 Fine: 24/05/2023 alle ore 13:00
Area Scientifico Didattica Paolo Volponi (Urbino, Via Saffi, 15) Aula D4

Online e in Presenza

#### Organizzato e promosso da:

Dipartimento di Scienze Pure e Applicate
Scuola di Scienze, Tecnologie e Filosofia dell'Informazione
LM-78 - Classe delle lauree magistrali in scienze filosofiche - Filosofia dell'informazione. Teoria e gestione della conoscenza
Synergia Research Group

### Modalità di partecipazione

#### Altre informazioni utili

Per ulteriori informazioni, contattare: pierluigi.graziani@uniurb.it

#### Il tuo 5x1000 per sostenere le attività di ricerca

L'Università di Urbino destina tutte le risorse che deriveranno da questa iniziativa alla ricerca scientifica ed al sostegno di giovani ricercatori.

15 22

#### Se sei vittima di violenza o stalking chiama il 1522, scarica l'app o chatta su www.1522.eu

Il numero, gratuito è attivo 24 h su 24, accoglie con operatrici specializzate le richieste di aiuto e sostegno delle vittime di violenza e stalking.

#### In contatto

Comunicati Stampa
Rassegna Stampa

#### Social

Università degli Studi di Urbino Carlo Bo
Via Aurelio Saffi, 2 – 61029 Urbino PU – IT
Partita IVA 00448830414 – Codice Fiscale 82002850418
2024 © Tutti i diritti sono riservati

Top