Dedukcja naturalna

Z Wikipedii, wolnej encyklopedii
Skocz do: nawigacji, wyszukiwania

Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazowany na systemach Hilberta.

Dowód to lista formuł objętych oknami.

Operacje w bardzo prostej wersji to:

  • dodanie założenia, otwiera to okno
  • przepisanie dowolnego aktywnego założenia
  • zamknięcie okna, dodaje się za oknem formułę "pierwsza formuła okna \supset ostatnia formuła okna", wszystkie formuły w oknie są dezaktywowane
  • użycie jednej z reguł dowodzenia (w szczególności modus ponens na dowolnych aktywnych) na dowolnych aktywnych formułach.

Każda formuła leżąca poza oknem, zwykle powstała w wyniku zamknięcia ostatniego okna, jest twierdzeniem.

Okna są wyłącznie graficzną reprezentacją tego co się dzieje.

Przykład[edytuj | edytuj kod]

Udowodnijmy, że P \supset (Q \supset P).


1. P (założenie)


2. Q (założenie)


3. P (przepisanie aktywnej formuły 1)


4. Q \supset P (eliminacja założenia 2, dezaktywacja 2 i 3)


5. P \supset (Q \supset P) (eliminacja założenia 1, dezaktywacja 1 i 4)

Dowód tego bardzo prostego twierdzenia jest - właśnie bardzo prosty. Co nie zawsze jest prawdą w przypadku innych systemów dowodzenia.

Bardziej rozbudowane wersje[edytuj | edytuj kod]

Przedstawiona tu wersja potrafi tylko dodawać i eliminować implikacje. Bardziej rozbudowane wersje zajmują się też innymi spójnikami dodając nowe reguły wyprowadzania formuł i zamykania okien.