Gerhard Gentzen

Gerhard Gentzen, 1909-1945, tysk logiker. Efter studier i matematik i Greifswald, Göttingen, München og Berlin var han fra 1934 assistent for David Hilbert og blev i 1943 docent ved det tyske universitet i Prag. I august 1945 døde han i allieret internering.

Gentzen udviklede to nye former for aksiomatisering af logikken, kaldet naturlig deduktion og sekventkalkyle; formelle beviser i disse systemer svarer ret nøje til uformelle, intuitive argumentformer. Hans navn er knyttet til to vigtige resultater. Han viste, at det er muligt at finde en normalform for beviser i prædikatslogikken, som har minimal kompleksitet (Gentzens Hauptsatz). Endvidere viste han, at det er muligt at bevise aritmetikkens konsistens, dvs. at der ikke findes logiske modsigelser i aritmetikken. Begge resultater spiller en afgørende rolle i moderne bevisteori.

Gentzens bevis for aritmetikkens konsistens hviler på antagelser vedrørende induktionsbeviser over visse uendelig store tal. Hans resultat viser, at det på trods af Kurt Gödels ufuldstændighedssætninger giver mening at føre konsistensbeviser, hvilket har ført til nye, svagere formuleringer af Hilberts program om at bevise matematiske teoriers konsistens.