Niesprzeczność
Z Wikipedii, wolnej encyclopedia
Niesprzeczność – brak sprzeczności teorii logicznej. Można go zdefiniować semantycznie albo syntaktycznie. Definicja semantyczna postuluje, że teoria jest niesprzeczna, jeśli posiada model. Odpowiada to pojęciu niesprzeczności w tradycyjnej logice Arystotelesa, aczkolwiek w dzisiejszej logice matematycznej używa się w zamian określenia spełnialności. Definicja syntaktyczna mówi, że teoria jest niesprzeczna, jeśli nie ma takiej formuły że zarówno jak i jej zaprzeczenie można wyprowadzić z aksjomatów danej teorii za pomocą powiązanego z nią systemu dedukcji.
Jeśli dane definicje semantyczne i syntaktyczne są równoważne, to mówi się, że dana logika jest zupełna. Zupełność rachunku zdań została wykazana przez Paula Bernaysa w 1918 roku i Emila Posta w 1921 roku, podczas gdy zupełność rachunku kwantyfikatorów została udowodniona przez Kurta Gödla w 1930 r. Silne logiki, takie jak rachunek predykatów drugiego rzędu, nie są zupełne.
Wczesny rozwój teorii dowodu był napędzany chęcią podania skończonych dowodów niesprzeczności dla całej matematyki w ramach programu Hilberta. Postulatami programu Hilberta wstrząsnęło twierdzenie Gödla o niedowodliwości niesprzeczności, które uzmysłowiło matematykom, że dostatecznie bogate teorie dowodzenia nie pozwalają na wykazanie niesprzeczności samych siebie (przy założeniu, że są one rzeczywiście niesprzeczne).
Pomimo iż niesprzeczność można wykazać za pomocą teorii modeli, to często robi się to, opierając się wyłącznie na syntaktyce, bez odnoszenia się do modeli.