W logice matematycznej , w koherencji lub spójności , o teorii aksjomatyczną można definiować na dwa sposoby, albo przez odniesienie do odliczenia : nie jest możliwe wykazanie wszystko od aksjomatów teorii, ani w odniesieniu do semantyki teorii : ten ma realizacje, które nadają mu znaczenie.
Pierwsza definicja jest syntaktyczna w tym sensie, że używa dedukcji lub demonstracji , które są obiektami skończonymi. O teorii mówi się w tym sensie, że jest spójna lub konsekwentna, gdy nie skutkuje wszystkimi stwierdzeniami języka, w którym jest ona wyrażona, lub w równoważny sposób (ponieważ ze sprzeczności możemy wydedukować wszystko ), gdy nie pozwala na zademonstrowanie zarówno wypowiedzi, jak i jej zaprzeczenia. Mówi się również, że taka teoria nie jest sprzeczna .
Druga definicja posługuje się teorią modeli : teoria jest spójna, gdy ma model , czyli strukturę matematyczną, w której interpretuje się terminy językowe i która spełnia wszystkie aksjomaty teorii, czyli taka struktura istnieje że wszystkie aksjomaty teorii są prawdziwe w tej strukturze.
Te dwie definicje są równoważne przez twierdzenie o poprawności i twierdzenie o kompletności . Pierwsza z nich powoduje, że wszystkie możliwe do udowodnienia twierdzenia teorii są spełnione przez strukturę, która spełnia aksjomaty, a zatem teoria spójna w sensie semantycznym jest spójna w sensie syntaktycznym, ponieważ struktura nie może spełnić zarówno twierdzenia, jak i jego negacji. . Twierdzenie kompletność wskazuje, że spójna teoria w sensie syntaktycznym ma model, to znaczy, że jest spójny w sensie semantycznym. Te dwa twierdzenia są zademonstrowane w logice klasycznej, przy obliczaniu predykatów pierwszego rzędu.
Do braku sprzeczności można podejść i zdefiniować na dwa sposoby:
Jeśli te definicje semantyczne i składniowe są równoważne dla danej logiki, mówi się, że ten system logiczny jest kompletny .
Dowód spójności to matematyczny dowód, że dana teoria jest spójna. Teoria dowodu zostało zainicjowane przez Davida Hilberta w celu dostarczenia dowodów finitary konsystencję do teorii matematycznych jako część swojego programu powiedział programu Hilberta . Dowody spójności badane w tym schemacie są syntaktyczne; semantyczny dowód spójności, gdy tylko wprowadza do gry nieskończony model, jest z natury nieskończony.
Program ten jest jednak kwestionowany przez twierdzenia o niekompletności , w szczególności drugie, zgodnie z którym rekurencyjnie aksjomatyzowalna spójna teoria, gdy tylko umożliwia wykonanie wystarczającej arytmetyki, nie pozwala wykazać własnej spójności. Tak jest w przypadku teorii takich jak prymitywna arytmetyka rekurencyjna (in) (kandydat na teorię rozwijającą dowody finitarne), arytmetyka Peano , teoria mnogości ZFC ... Istnieją jednak słabe spójne teorie arytmetyczne, jak arytmetyka Presburgera , aksjomatyczny system dla liczb całkowitych z dodawaniem, które są kompletne.
Pierwszego rzędu teoria jest widoczne w dalszej części jako zbiór zamkniętych wzorach logicznych z pewnym języka L z logiką pierwszego rzędu . Bardzo ogólna definicja koherencji (lub konsekwencji) w sensie dedukcji, tak zwana „syntaktyczna” definicja koherencji, jest następująca:
Jeśli język ma negację i jeśli logika przyjmuje jako zasadę, że ze sprzeczności (formuły i jej zaprzeczenia) można wydedukować jakąkolwiek formułę (tak jest w logice klasycznej , w logice intuicjonistycznej , ...), to definicja ta jest odpowiednik następujących:
O niespójnej teorii mówi się, że jest niespójna lub sprzeczna.
Z drugiej strony jest całkiem możliwe, biorąc pod uwagę spójną teorię T i formułę F w tym samym języku, że T nie ma konsekwencji ani formuły F, ani jej zaprzeczenia.
W kontekście dowodu twierdzenia o zupełności logiki pierwszego rzędu (klasycznej), to znaczy faktu, że teoria koherentna (w sensie dedukcji) ma model, wygodnie może być „wprowadzić następujące definicje.
Twierdzenie o kompletności można następnie zademonstrować w dwóch krokach:
W pierwszej części język L ' uzyskuje się przez dodanie do języka L „wystarczającej ilości” nowych stałych ( policzalny zbiór stałych, jeśli język oryginalny ma skończoną lub policzalną sygnaturę ), przy czym stałe są skojarzone bijektywnie z formułami. Do. Do. wolna zmienna języka docelowego L ' . Te stałe są świadkami Henkina o odpowiednich formułach, teoria jest najpierw wzmacniana przez odpowiednie aksjomaty, a następnie nasycana, aby dać maksymalnie spójne rozszerzenie (w najbardziej ogólnym przypadku lemat Zorna jest przydatny, w policzalnym przypadku możemy użyć definicja przez indukcję). Możliwe jest również, aby nasycić świadków Henkin jest w tym samym czasie jak skonstruować maksymalnie spójne rozszerzenie, ważne jest, że dla każdego widocznego rachunku ∃ x F , mamy świadka C i że F [ c / x ] albo konsekwencją otrzymana teoria (lub w równoważny sposób (jeśli teoria jest kompletna), dla każdego nie dającego się udowodnić uniwersalnego stwierdzenia ∀ x F mamy świadka c i że negacja ¬ F [ c / x ] jest konsekwencją uzyskanej teorii ).
Druga część jest zademonstrowana, w przypadku języka pierwszego rzędu bez równości, przyjmując jako podstawowy zestaw modelu terminy zamknięte języka (język, który został uzupełniony przez świadków Henkina w pierwszym kroku). W przypadku języka egalitarnego konieczne jest ilorazowanie zbioru terminów przez stosunki równości między terminami zamkniętymi, które są wyprowadzone z teorii.