System Hilberta

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.

Istnieje wiele Systemów Hilberta do różnych logik i dla jednej logiki.

Podstawową regułą dowodzenia w większości z nich jest modus ponens:

• jeśli ${\displaystyle x}$ i ${\displaystyle x\supset y,}$ to ${\displaystyle y.}$

Ponadto zwykle dodaje się regułę substytucji:

• jeśli dana jest pewna formuła, to wolno dopisać formułę powstałą przez podstawienie dowolnej formuły za wszystkie wystąpienia pewnej zmiennej.

Zamiast skończonej liczby aksjomatów dopuszcza się skończoną liczbę schematów aksjomatu, czyli w istocie nieskończenie wiele aksjomatów.

Załóżmy, że mamy regułę modus ponens i dwa schematy aksjomatu:

1. ${\displaystyle X\supset (Y\supset X)}$
2. ${\displaystyle (X\supset (Y\supset Z))\supset ((X\supset Y)\supset (X\supset Z)).}$

Udowodnijmy teraz, że ${\displaystyle P\supset P{:}}$
Z schematu 1 podstawiając ${\displaystyle X=P,}$ ${\displaystyle Y=P}$

${\displaystyle P\supset (P\supset P)}$

Z schematu 1 podstawiając ${\displaystyle X=P,}$ ${\displaystyle Y=(P\supset P)}$

${\displaystyle P\supset ((P\supset P)\supset P)}$

Z schematu 2 podstawiając ${\displaystyle X=Z=P,}$ ${\displaystyle Y=(P\supset P)}$

${\displaystyle (P\supset ((P\supset P)\supset P))\supset ((P\supset (P\supset P))\supset (P\supset P))}$

Z drugiej i trzeciej formuły i modus ponens:

${\displaystyle (P\supset (P\supset P))\supset (P\supset P)}$

Z pierwszej i czwartej formuły i modus ponens:

${\displaystyle (P\supset P)}$

Co miało zostać udowodnione.