Dedukcja naturalna

Ten artykuł od 2012-09 wymaga zweryfikowania podanych informacji. Należy podać wiarygodne źródła, najlepiej w formie przypisów bibliograficznych. Część lub nawet wszystkie informacje w artykule mogą być nieprawdziwe. Jako pozbawione źródeł mogą zostać zakwestionowane i usunięte. Dokładniejsze informacje o tym, co należy poprawić, być może znajdują się w dyskusji tego artykułu. Po wyeliminowaniu niedoskonałości należy usunąć szablon {{Dopracować}} z tego artykułu.

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

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

5. ${\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

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.