System Hilberta
Z Wikipedii
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 x i , to 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.
[edytuj] Przykład
Załóżmy że mamy regułę modus ponens i dwa schematy aksjomatu:
Udowodnijmy teraz że :
Z schematu 1 podstawiając X = P, Y = P
Z schematu 1 podstawiając X = P,
Z schematu 2 podstawiając X = Z = P,
Z drugiej i trzeciej formuły i modus ponens:
Z pierwszej i czwartej formuły i modus ponens:
Co miało zostać udowodnione.