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 i to 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.