Teoria dovada , de asemenea , cunoscut sub numele de teoria probei (din limba engleză teoriei probei ) este o ramură a logicii matematice . A fost fondat de David Hilbert la începutul XX - lea secol .
Hilbert a propus această nouă disciplină matematică în celebra sa declarație la al 2- lea Congres Internațional al Matematicienilor din 1900, cu scopul de a demonstra consistența matematicii. Acest obiectiv a fost invalidat de nu mai puțin celebra teoremă a incompletitudinii lui Gödel în 1931, care însă nu a împiedicat dezvoltarea demonstrației, în special datorită muncii lui Jacques Herbrand și Gerhard Gentzen . Acesta din urmă a demonstrat unul dintre principalele rezultate ale teoriei dovezilor, cunoscut sub numele de Hauptsatz (teorema principală) sau teorema eliminării tăieturilor . Gentzen a folosit apoi această teoremă pentru a oferi prima dovadă pur sintactică a consistenței aritmeticii .
După o perioadă de calm, care a făcut tot posibilul să se stabilească o serie de alte rezultate de consistență relativă și să schițeze o clasificare a teoriilor axiomatice, teoria demonstrației a suferit o revigorare spectaculoasă în anii 1960. odată cu descoperirea Curry-ului. -Corespondența Howard care a prezentat o nouă și profundă legătură structurală între logică și calcul: în esență, procedura de eliminare a tăierii definită de Gentzen poate fi privită ca un proces de calcul, astfel încât dovezile formale devin apoi programe al căror tip este propunerea care trebuie demonstrată . De atunci, teoria dovezilor s-a dezvoltat în strânsă simbioză cu alte domenii ale logicii și informaticii teoretice, în special lambda-calcul și a dat naștere la noi modele de calcul, cea mai recentă fiind logica liniară a lui Jean-Yves Girard în 1986. Astăzi, o parte a teoriei dovezilor fuzionează cu semantica limbajelor de programare și interacționează cu multe alte discipline ale logicii și computerului teoretic: