Dedukcja naturalna


Dedukcja naturalna w encyklopedii

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

Dedukcja naturalna – bardzo intuicyjny i generujący dowody system dowodzenia twierdzeń, bazujący 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 {\displaystyle \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 kod

Udowodnijmy, że P ( Q P ) . {\displaystyle P\supset (Q\supset P).}


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


5. P ( Q P ) {\displaystyle 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 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.

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