A bizonyítás elmélet is ismert név alatt elmélet bizonyítása (angol bizonyítási elmélet ) egyik ága a matematikai logika . David Hilbert alapította a XX . Század elején .
Hilbert javasolt új matematikai alapokra ő híres nyilatkozata a 2 -én Nemzetközi Matematikai Kongresszus 1900-ban azzal a céllal, hogy igazolja az összhang a matematika. Ezt a célt érvénytelenítette Gödel 1931-es nemteljesítésének nem kevésbé híres tétele , amely azonban nem akadályozta meg a demonstráció elméletének fejlődését, különösen Jacques Herbrand és Gerhard Gentzen munkájának köszönhetően . Ez utóbbi a bizonyítási elmélet egyik fő eredményét mutatta be, Hauptsatz (fő tétel) vagy vágás eliminációs tétel néven . Ezután Gentzen ezt a tételt használta az első tisztán szintaktikai bizonyításra az aritmetika konzisztenciájáról .
A nyugodt időszak után, amely mindazonáltal lehetővé tette a relatív koherencia számos más eredményének megállapítását és az axiomatikus elméletek osztályozásának felvázolását, a bizonyítási elmélet látványos újjáéledésen ment keresztül az 1960-as években. A Curry felfedezésével. -Howard-megfelelés, amely új és mély strukturális kapcsolatot mutatott ki a logika és a számítástechnika között: lényegében a Gentzen által definiált cut eliminációs eljárás számítási folyamatnak tekinthető, így a formális bizonyítások aztán programokká válnak, amelyek típusa a bemutatandó javaslat. Azóta a bizonyítási elmélet szoros szimbiózisban alakult ki a logika és az elméleti számítástechnika más területeivel, nevezetesen a lambda-kalkulussal , és új számítási modelleket hozott létre, amelyek közül a legfrissebb Jean-Yves Girard 1986-os lineáris logikája volt . Ma a bizonyítási elmélet egy része összeolvad a programozási nyelvek szemantikájával , és kölcsönhatásba lép a logika és az elméleti számítógép számos más tudományágával: