Rachunek dowodowy
W logice matematycznej rachunek dowodowy lub system dowodowy buduje się w celu udowodnienia twierdzeń.
Przegląd
System dowodowy składa się z elementów:
- Język: Zbiór L formuł dopuszczonych przez system, na przykład logika zdań lub logika pierwszego rzędu .
- Reguły wnioskowania : Lista reguł, które można zastosować do udowodnienia twierdzeń na podstawie aksjomatów i twierdzeń.
- Aksjomaty : Przyjmuje się, że formuły w L są ważne. Wszystkie twierdzenia wywodzą się z aksjomatów.
Zwykle dany rachunek dowodowy obejmuje więcej niż jeden konkretny system formalny, ponieważ wiele rachunków dowodowych jest niedostatecznie określonych i można je zastosować w przypadku radykalnie odmiennych logik. Na przykład przypadkiem paradygmatycznym jest rachunek sekwencyjny , którego można użyć do wyrażenia relacji konsekwencji zarówno logiki intuicjonistycznej , jak i logiki relewancji . Zatem, mówiąc luźno, rachunek dowodowy to szablon lub wzorzec projektowy , charakteryzujący się pewnym stylem wnioskowania formalnego, który może specjalizować się w tworzeniu określonych systemów formalnych, a mianowicie poprzez określenie rzeczywistych reguł wnioskowania dla takiego systemu. Wśród logików nie ma zgody co do tego, jak najlepiej zdefiniować ten termin.
Przykłady rachunku dowodowego
Najbardziej znane rachunki dowodowe to te klasyczne rachunki, które są nadal w powszechnym użyciu:
- Klasa systemów Hilberta , której najsłynniejszym przykładem jest system logiki pierwszego rzędu Hilberta-Ackermanna z 1928 r .;
- Rachunek dedukcji naturalnej Gerharda Gentzena , który jest pierwszym formalizmem teorii dowodu strukturalnego i który jest kamieniem węgielnym korespondencji formuł jako typów wiążącej logikę z programowaniem funkcjonalnym ;
- Rachunek sekwencyjny Gentzena , będący najlepiej zbadanym formalizmem teorii dowodu strukturalnego.
Wiele innych rachunków dowodowych było lub mogło być przełomowych, ale obecnie nie są powszechnie stosowane.
- Rachunek sylogistyczny Arystotelesa , przedstawiony w Organonie , łatwo dopuszcza formalizm. Nadal istnieje pewne współczesne zainteresowanie sylogizmami, realizowanymi pod egidą logiki terminów .
- , że dwuwymiarowy zapis Begriffsschrift ( 1879) Gottloba Fregego wprowadza do logiki nowoczesną koncepcję kwantyfikatora .
- Wykres egzystencjalny CS Peirce’a z łatwością mógłby okazać się przełomowy, gdyby historia potoczyła się inaczej.
Współczesne badania w dziedzinie logiki obfitują w konkurencyjne rachunki dowodowe:
- Zaproponowano kilka systemów, które zastępują zwykłą składnię tekstową pewną składnią graficzną. sieci dowodowe i rachunek różniczkowy należą do takich systemów.
- Ostatnio wielu logików zainteresowanych teorią dowodu strukturalnego zaproponowało rachunki z głębokim wnioskiem , na przykład logikę wyświetlania , hipersekwencje , rachunek struktur i implikacje grupowe .
Zobacz też
- System dowodu zdań
- Siatki dowód
- Rachunek cyrkulacyjny
- Rachunek konstrukcji
- Formalny dowód
- Metoda obrazów analitycznych
- Rozdzielczość (logika)