In questo intervento, che ripercorre alcuni contenuti della mia tesi di dottorato, saranno esaminate alcune forme di « circolarità » che appaiono nella teoria della dimostrazione della logica del secondo ordine e della sua controparte costruttiva, il Sistema F.
Queste circolarità, o « circoli viziosi » (Poincaré 1906), saranno analizzate sulla base della distinzione tra due punti di vista corrispondenti a metodologie distinte e irriducibili (a causa dei teoremi di incompletezza): il primo (« le pourquoi », Girard 2000) é focalizzato sulla questione della coerenza e dell’Hauptsatz e richiede dei metodi di dimostrazione infinitari (ovvero non elementari). Il secondo (« le comment », Girard 2000) é focalizzato sul contenuto computazionale e combinatorio delle dimostrazioni, dato dalla corrispondenza tra prove e programmi, e non richiede che metodi elementari di dimostrazione.
Questa distinzione metodologica permette di mettere in luce nel dettaglio le limitazioni epistemologiche a cui va incontro la logica del secondo ordine (cosa può essere deciso in modo elementare, ovvero con certezza? Cosa invece non può mai essere stabilito al di là di ogni ragionevole dubbio?)