System Hilberta


System Hilberta w encyklopedii

Z Wikipedii, wolnej encyklopedii Przejdź do nawigacji Przejdź do wyszukiwania

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 {\displaystyle x} i x y , {\displaystyle x\supset y,} to y . {\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.

Przykład | edytuj kod

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

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

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

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

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

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

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

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

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

Z pierwszej i czwartej formuły i modus ponens:

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

Co miało zostać udowodnione.

Na podstawie artykułu: "System Hilberta" pochodzącego z Wikipedii
OryginałEdytujHistoria i autorzy