Niesprzeczność w logice
Niesprzeczność to cecha teorii logicznej, definiowana zarówno semantycznie, jak i syntaktycznie. Z definicji semantycznej wynika, że teoria jest niesprzeczna, jeśli posiada model, co odpowiada pojęciu niesprzeczności w tradycyjnej logice Arystotelesa. Współczesna logika matematyczna używa pojęcia spełnialności. Z kolei definicja syntaktyczna stwierdza, że teoria jest niesprzeczna, jeśli nie można wyprowadzić zarówno formuły P, jak i jej zaprzeczenia z aksjomatów danej teorii. Równoważność tych definicji określa się jako zupełność logiki.
Zupełność rachunku zdań została udowodniona przez Paula Bernaysa (1918) i Emila Posta (1921), a rachunku kwantyfikatorów przez Kurta Gödla (1930). Niektóre silne logiki, jak rachunek predykatów drugiego rzędu, nie są jednak zupełne.
Teoria dowodu
Wczesny rozwój teorii dowodu miał na celu znalezienie skończonych dowodów niesprzeczności całej matematyki w ramach programu Hilberta. Jednak twierdzenie Gödla o niedowodliwości niesprzeczności pokazało, że bogate teorie dowodzenia nie mogą udowodnić niesprzeczności samych siebie, zakładając, że są rzeczywiście niesprzeczne.
Formuły w rachunku predykatów
Zbiór formuł Φ w rachunku predykatów pierwszego rzędu jest niesprzeczny (symbolicznie: Con Φ), gdy nie istnieje formuła φ, dla której zarówno Φ ⊢ φ, jak i Φ ⊢ ¬φ. W przeciwnym razie zbiór Φ jest sprzeczny (Inc Φ). Równoważność sprzeczności można wyrazić następująco:
- Inc Φ
- Dla każdego φ, Φ ⊢ φ.
Każdy spełnialny zbiór formuł jest niesprzeczny. Zbiór formuł Φ jest spełnialny wtedy, gdy istnieje model I, taki że I ⊨ Φ.
Niesprzeczność i zupełność arytmetyki
W teoriach arytmetyki, takich jak arytmetyka Peana, istnieje silna zależność pomiędzy niesprzecznością a zupełnością teorii. Teoria jest zupełna, gdy dla każdej formuły φ przynajmniej jedna z formuł φ lub ¬φ jest jej logiczną konsekwencją.
Arytmetyka Presburgera jest przykładem układu aksjomatycznego, który jest zarówno niesprzeczny, jak i zupełny. Twierdzenie Gödla o niezupełności wskazuje, że żadna dostatecznie silna efektywna teoria arytmetyki nie może być jednocześnie zupełna i niesprzeczna. Dotyczy to arytmetyki Peana i prostej arytmetyki rekurencyjnej, ale nie arytmetyki Presburgera.
Dodatkowo, drugie twierdzenie Gödla stwierdza, że dostatecznie silna efektywna teoria arytmetyki jest niesprzeczna tylko wtedy, gdy nie ma dowodu dla specyficznego zdania Gödla, które formalizuje niesprzeczność danej teorii. W efekcie, niesprzeczność bogatej, efektywnej teorii arytmetyki nie może być udowodniona w ramach tej samej teorii, co odnosi się również do teorii takich jak teoria mnogości Zermela-Fraenkla.
