Todiste teoria , joka tunnetaan myös nimellä teorian todiste (ja Englanti todiste teoria ) on osa matemaattista logiikkaa . Sen perusti David Hilbert vuoden alussa XX : nnen vuosisadan .
Hilbert ehdotti tätä uutta matemaattinen kurinalaisuutta hänen kuuluisa lausahdus klo 2 : nnen kansainvälisen kongressin Matematiikan vuonna 1900, jonka tavoitteena on osoittaa johdonmukaisuutta matematiikka. Tämän tavoitteen mitätöi Gödelin vuonna 1931 tekemä yhtä kuuluisan epätäydellisyyden teoreema , joka ei kuitenkaan estänyt mielenosoituksen teoriaa kehittymästä, erityisesti Jacques Herbrandin ja Gerhard Gentzenin työn ansiosta . Jälkimmäinen osoitti yhden todistusteorian päätuloksista , joka tunnetaan nimellä Hauptsatz (päälause) tai leikkauksen eliminointilause . Gentzen käytti tämän lauseen avulla ensimmäisen puhtaasti syntaktisen todistuksen aritmeettisen johdonmukaisuudesta .
Rauhallisen jakson jälkeen, joka mahdollisti useiden muiden suhteellisen johdonmukaisuuden tulosten määrittämisen ja aksiomaattisten teorioiden luokittelun luonnehtimisen, todistusteoria koki suurenmoisen elpymisen 1960-luvulla. Curryn löytämisen jälkeen -Howardin kirjeenvaihto, jolla oli uusi ja syvä rakenteellinen yhteys logiikan ja tietojenkäsittelyn välillä: Gentzenin määrittelemä leikkauksen eliminointimenettely voidaan olennaisesti nähdä laskennallisena prosessina, joten muodollisista todisteista tulee ohjelmia, joiden tyyppi on osoitettava ehdotus. Sittemmin näyttöä teoria on kehitetty tiiviissä symbioosissa muiden alojen logiikan ja teoreettisen tietojenkäsittelyopin, erityisesti lambda-hammaskiveä , ja se on synnyttänyt uusia malleja hammaskiven, joista viimeisin on lineaarinen logiikka on Jean-Yves Girard vuonna 1986. Nykyään osa todisteiden teoriasta sulautuu ohjelmointikielten semantiikkaan ja on vuorovaikutuksessa monien muiden logiikan ja teoreettisen tieteenalojen kanssa: