System Hilberta

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacja, szukaj

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 x \supset y, 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.

Przykład[edytuj | edytuj kod]

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

  1. X \supset (Y \supset X)
  2. (X \supset (Y \supset Z)) \supset ((X \supset Y) \supset (X \supset Z))

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

P \supset (P \supset P)

Z schematu 1 podstawiając X = P, Y = (P \supset P)

P \supset ((P \supset P) \supset P)

Z schematu 2 podstawiając X = Z = P, Y = (P \supset P)

(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:

(P \supset (P \supset P)) \supset (P \supset P)

Z pierwszej i czwartej formuły i modus ponens:

(P \supset P)

Co miało zostać udowodnione.