Teoria dowodu - Polski Serwis Naukowy

Teoria dowodu to dział logiki matematycznej zajmujący się analizą pojęcia dowodu oraz możliwych sposobów używania go w rozważaniach matematycznych. Za ojca tej dziedziny uważa się Davida Hilberta, jednego z najwybitniejszych matematyków przełomu dziewiętnastego i dwudziestego wieku.

System Hilberta – dowolny system automatycznego dowodzenia twierdzeń, w którym występuje pewien zbiór aksjomatów i reguł dowodzenia, a dowód składa się z ciągu formuł będących albo aksjomatami, albo formułami wyprowadzonymi z poprzednich formuł na podstawie reguł dowodzenia, z których ostatnia jest właśnie formułą którą chcemy dowieść. Jest to wnioskowanie w przód w przeciwieństwie do wnioskowania w tył znanego z innych systemów dowodzenia.

Twierdzenie to sformalizowana wypowiedź sądu, stosowana we wszystkich naukach ścisłych, składająca się z dwóch zbiorów zdań, które łączy relacja implikacji. Pierwszy zbiór zdań określa ściśle warunki dla których dane twierdzenie jest spełnione i nazywa się założeniem twierdzenia, a drugi zbiór zdań jest właściwym sądem, będącym istotną treścią wypowiadanego twierdzenia i zwany jest tezą twierdzenia.

Do głównych zadań teorii dowodu należy kształtowanie takich systemów logicznych wraz z odpowiednimi zestawami aksjomatów, które nadawałyby się do formalizowania dowodów matematycznych, następnie zaś badanie siły tych systemów (im silniejszy system, tym więcej twierdzeń można udowodnić na jego gruncie wychodząc z danego zbioru aksjomatów). Bada się też szczegółowo strukturę dowodów formalnych, co czyni teorię dowodu odpowiednikiem syntaktyki logicznej (czasem obu tych terminów używa się zamiennie).

Dowód – w matematyce wykazanie, że pewne zdanie jest prawdziwe. Dowód należy odróżnić od empirycznego lub heurystycznego rozumowania. Każdy krok dowodu musi jasno wynikać z poprzednich lub być przyjętym aksjomatem; rozumowanie nie spełniające tego warunku nie jest dowodem. Ostatni krok dowodu to udowodnione zdanie, które w ten sposób staje się twierdzeniem danej teorii. Zwyczajowo koniec dowodu oznacza się skrótem q.e.d (quod erat demonstrandum), c.n.d. (co należało dowieść) lub podobnym.

Rachunek predykatów pierwszego rzędu – (ang. first order predicate calculus) to system logiczny, w którym zmienna, na której oparty jest kwantyfikator, może być elementem pewnej wybranej dziedziny (zbioru), nie może natomiast być zbiorem takich elementów. Tak więc nie mogą występować kwantyfikatory typu "dla każdej funkcji z X na Y ..." (gdyż funkcja jest podzbiorem X × Y), "istnieje własność p, taka że ..." czy "dla każdego podzbioru X zbioru Z ...". Rachunek ten nazywa się też krótko rachunkiem kwantyfikatorów, ale często używa się też nazwy logika pierwszego rzędu (szczególnie wśród matematyków zajmujących się logiką matematyczną).

Zobacz też

automatyczne dowodzenie twierdzeń

dedukcja naturalna

klasyczny rachunek logiczny

system Hilberta