Gentzen

Gentzen

Gentzen Gerhard Karl Erich (Greifswald, Meclemburgo-Pomerania Occidentale, 1909 - Praga 1945) logico tedesco. Diede importanti contributi alla teoria della dimostrazione e al problema della coerenza dei sistemi formali dell’aritmetica. Dopo aver studiato in diverse università tedesche conseguì il dottorato a Göttingen, sotto la guida di H. Weyl, con una tesi sui fondamenti della matematica. Nel 1933 divenne assistente di D. Hilbert e fu quindi revisore della rivista «Zentralblatt für Mathematik». Riprese le tematiche della teoria della dimostrazione hilbertiana, inquadrandole in una nuova prospettiva e caratterizzando la struttura delle dimostrazioni nei termini di una serie di passi deduttivi atomici il più possibile aderenti all’effettivo procedimento argomentativo matematico; in tal modo la dimostrazione assume una caratteristica forma ramificata “ad albero”, che consente di evidenziare le assunzioni implicate. Sfruttando questi calcoli di deduzione naturale e una loro successiva generalizzazione in cui al posto di singoli enunciati vengono esaminati i rapporti tra successioni di formule, Gentzen riuscì a ottenere alcuni importanti risultati. Il primo (noto come Hauptsatz o eliminazione del → taglio) afferma che è possibile convertire ogni dimostrazione in un’altra in cui non si faccia uso dell’unica regola che consente di eliminare completamente alcune espressioni che compaiono nelle sue premesse; ne segue che per ogni proposizione formale dimostrabile esiste una dimostrazione composta unicamente da sue sottoespressioni. Il secondo risultato di Gentzen riguarda la coerenza dei sistemi formali dell’aritmetica, che egli riuscì a dimostrare descrivendo delle trasformazioni che a ogni derivazione del calcolo ne associano un’altra eventualmente più lunga, ma concettualmente più semplice. L’induzione transfinita che Gentzen utilizza in questo frangente eccede però i metodi finitisti ammessi da Hilbert, pur restando all’interno di una più vasta classe di metodi che possono essere considerati «costruttivi». I suoi studi furono interrotti dallo scoppio della seconda guerra mondiale: nel 1939 fu infatti arruolato e si occupò di telecomunicazioni. Congedato nel 1942 per motivi di salute, fu quindi chiamato a insegnare all’università tedesca di Praga, allora sotto occupazione tedesca. Quando nel maggio 1945 la popolazione di Praga insorse contro gli occupanti, Gentzen fu arrestato insieme a tutto lo staff dei docenti dell’università tedesca e, a causa della sua adesione al partito nazionalsocialista, fu poi internato dalle truppe sovietiche in un campo di prigionia, dove, tre mesi dopo, morì.