Dlaczego rozsądek oznacza spójność?

Czytałem pytanie Spójność i kompletność oznaczają solidność? a pierwsze oświadczenie zawiera:

Rozumiem, że solidność oznacza konsekwencję.

Byłem dość zdziwiony, ponieważ uważałem, że dźwięk jest słabszym stwierdzeniem niż spójność (tj. Myślałem, że spójne systemy muszą być zdrowe, ale wydaje mi się, że to nieprawda). Używałem nieformalnej definicji, której Scott Aaronson używał w swoim kursie 6.045 / 18.400 na MIT dla spójności i solidności:

1. Soundness = System dowodowy jest zdrowy, jeśli wszystkie stwierdzenia, które udowodni, są rzeczywiście prawdziwe (wszystko, co można udowodnić, to prawda). tj. JEŻELI ( jest możliwe do udowodnienia) ( jest Prawdą). Więc JEŻELI (istnieje ścieżka do formuły) NASTĘPNIE (ta formuła ma wartość True)$\phi$$\implies$$\phi$
2. Spójność = spójny system nigdy nie dowodzi A i NIE (A). Tak więc tylko jedno A lub jego negacja może być Prawdą.

Korzystając z tych (być może nieformalnych) definicji, skonstruowałem następujący przykład, aby wykazać, że istnieje system, który jest solidny, ale niespójny:

Powodem, dla którego myślałem, że to był system dźwiękowy, jest to, że z założenia aksjomaty są prawdziwe. Tak więc A i nie A są prawdziwe (tak, wiem, że prawo wykluczonego środka nie jest uwzględnione). Ponieważ jedyną regułą wnioskowania jest negacja, otrzymujemy, że możemy osiągnąć zarówno A, jak i A z aksjomatów i dotrzeć do siebie. Zatem dochodzimy do prawdziwych stwierdzeń tylko w odniesieniu do tego systemu. Oczywiście system nie jest spójny, ponieważ możemy udowodnić negację jedynej instrukcji w systemie. Dlatego wykazałem, że system dźwiękowy może być niespójny. Dlaczego ten przykład jest niepoprawny? Co zrobiłem źle?

W mojej głowie ma to sens intuicyjnie, ponieważ bezbłędność mówi tylko, że kiedy zaczynamy od aksjomatu i przekręcamy reguły wnioskowania, docieramy tylko do miejsc docelowych (tj. Stwierdzeń), które są Prawdą. Jednak tak naprawdę nie mówi, do którego celu dotrzemy. Jednak spójność mówi, że możemy dotrzeć do miejsca docelowego, które osiąga albo albo (oba nie oba). Zatem każdy spójny system musi zawierać prawo wykluczonego środka jako aksjomat, którego oczywiście nie zrobiłem, a następnie po prostu uwzględniłem negację jedynego aksjomatu jako jedynego innego aksjomatu. Więc nie wydaje mi się, że zrobiłem coś zbyt sprytnego, ale jakoś coś jest nie tak?¬ $A$$\neg A$

Po prostu zdaję sobie sprawę, że to może być problem, ponieważ używam nieformalnej definicji Scotta. Jeszcze zanim napisałem pytanie, sprawdziłem wikipedię, ale ich definicja nie miała dla mnie sensu. W szczególności część, którą mówią:

w odniesieniu do semantyki systemu

ich pełny cytat to:

każda formuła, którą można udowodnić w systemie, jest logicznie poprawna w odniesieniu do semantyki systemu.

Polecam przyjrzenie się logice formalnej poza niejasnymi, falistymi opisami. Jest interesujący i bardzo istotny dla informatyki. Niestety terminologia i wąskie ukierunkowanie nawet podręczników dotyczących logiki formalnej może przedstawiać wypaczony obraz tego, czym jest logika. Problem polega na tym, że przez większość czasu, gdy matematyki mówią o „logice”, mają (często domyślnie) na myśli klasyczną logikę zdań lub klasyczną logikę pierwszego rzędu. Chociaż są to niezwykle ważne systemy logiczne, nie są one bliskie szerokości logiki. W każdym razie to, co powiem, w dużej mierze odbywa się w tym wąskim kontekście, ale chcę wyjaśnić, że dzieje się to w określonym kontekście i nie musi być prawdą poza nim.

Po pierwsze, jeśli spójność jest zdefiniowana jako nie udowadniająca zarówno jak i , co się stanie, jeśli nasza logika nie ma nawet negacji lub jeśli¬ A $A$$\neg A$$\neg$znaczy coś jeszcze? Oczywiście to pojęcie spójności przyjmuje pewne założenia dotyczące logicznego kontekstu, w którym działa. Zazwyczaj pracujemy nad klasyczną logiką zdań lub jakimś jej rozszerzeniem, takim jak klasyczna logika pierwszego rzędu. Istnieje wiele prezentacji, tj. List aksjomatów i reguł, które można nazwać klasyczną logiką zdań / logiki pierwszego rzędu, ale dla naszych celów nie ma to większego znaczenia. Są równoważne w pewnym sensie. Zazwyczaj, gdy mówimy o systemie logicznym, mamy na myśli (klasyczną) teorię pierwszego rzędu. Zaczyna się to od reguł i (logicznych) aksjomatów klasycznej logiki pierwszego rzędu, do których dodaje się podane symbole funkcji, symbole predykatów i aksjomaty (zwane aksjomatami nielogicznymi). Teorie pierwszego rzędu są zwykle tym, co my ”

Następnie, solidność zwykle oznacza solidność w odniesieniu do semantyki. Spójność jest właściwością składniową związaną z tym, jakie formalne dowody możemy wykonać. Soundness to właściwość semantyczna, która ma związek z tym, jak interpretujemy formuły, symbole funkcji i predykujemy symbole na obiekty matematyczne i wyrażenia. Aby nawet zacząć mówić o solidności, musisz podać semantykę, tj. Interpretację wyżej wymienionych rzeczy. Ponownie mamy separację między logicznymi łącznikami i logicznymi aksjomatami oraz symbolami funkcji, symbolami predykatów i nielogicznymi aksjomatami. To, co czyni łączniki łącznikami i logicznymi aksjomatami logicznymi aksjomatami z semantycznego punktu widzenia, polega na tym, że są one traktowane specjalnie przez semantykę, podczas gdy symbole funkcji, symbole predykatów i nielogiczne aksjomaty tego nie robią.$[\![\varphi\land\psi]\!]=[\![\varphi]\!]\cap[\![\psi]\!]$ gdzie używam jako interpretacja wzoru . W szczególności Gdzie jest zestawem domen. Pomysł polega na tym, że formuła jest interpretowana jako zbiór elementów (krotek) spełniających formułę. Formuła zamknięta (tj. Bez wolnych zmiennych) jest interpretowana jako relacja zerowa, czyli podzbiór zbioru singletonów, który może być tylko tym singletonem lub pustym zbiorem. Formuła zamknięta jest „prawdziwa”, jeśli nie jest interpretowana jako pusty zestaw. Zdrowość jest zatem stwierdzeniem, że każda sprawdzalna (zamknięta) formuła jest „prawdziwa” w powyższym znaczeniu.φ $[\![\varphi]\!]$$\varphi$$[\![\neg\varphi]\!]=D\setminus[\![\varphi]\!]$$D$

Łatwo stąd, nawet ze szkicu, który podałem, udowodnić, że solidność oznacza konsekwencję (w kontekście klasycznej logiki pierwszego rzędu i naszkicowanej przez nas semantyki). Jeśli Twoja logika jest zdrowy, wówczas każda formuła, którą można udowodnić, interpretuje jako niepusty zbiór, ale jest zawsze interpretowany jako pusty zbiór bez względu na to, jaka jest formuła , i dlatego nie da się udowodnić, tzn. twoja logika jest spójna.

Solidność i spójność są właściwościami systemów dedukcyjnych. Siła głosu może być zdefiniowana tylko w odniesieniu do pewnej semantyki, która zakłada się, że jest podawana niezależnie od systemu dedukcyjnego.

W dziedzinie semantyki obie właściwości są powiązane

Definicja 1 ( Soundness [Semantics] - zapożyczony z Wikipedii ) Soundness systemu dedukcyjnego jest właściwością, że każde zdanie, które można udowodnić w tym systemie dedukcyjnym, jest również prawdziwe we wszystkich interpretacjach lub strukturach teorii semantycznej dla języka, na którym ta teoria jest oparty.

Definicja 2 ( konsystencję semantyka [] ) Zestaw zdań w języku są zgodne, wtedy i tylko wtedy, gdy istnieją strukturę języka , które spełnia wszystkie zdania w . System dedukcyjny jest spójny, jeśli istnieje struktura spełniająca wszystkie możliwe do udowodnienia w nim formuły.L L$A$$\mathfrak{L}$$\mathfrak{L}$$A$

Dzięki dwóm powyższym definicjom wyraźnie widać, że solidność oznacza spójność. Tzn. Jeśli zbiór wszystkich zdań, które można udowodnić, mieści się we wszystkich strukturach języka, istnieje co najmniej jedna struktura, która je spełnia.

Twój system dowodowy nie jest ani solidny, ani spójny, ponieważ nie jest prawdziwą propozycją, chyba że , w którym to przypadku nie jest prawdziwą propozycją. Ten argument pokazuje, że każdy system dźwiękoszczelny jest również spójny.A ≡ ⊤ ¬ A ≡ $A$$A \equiv \top$$\lnot A \equiv \bot$

Często, gdy wymyślamy systemy logiczne, motywuje je próba opisania istniejącego wcześniej zjawiska. Na przykład arytmetyka Peano jest próbą aksjatyzacji liczb naturalnych wraz z operacjami dodawania i mnożenia.

Siła głosu może być zdefiniowana tylko w odniesieniu do zjawiska, które próbujesz opisać, i zasadniczo oznacza, że ​​twoje aksjomaty i reguły wnioskowania naprawdę opisują daną rzecz. Tak więc, na przykład, arytmetyka Peano jest zdrowa, ponieważ jej aksjomaty i reguły wnioskowania są prawdziwe w odniesieniu do liczb naturalnych.

To oczywiście oznacza, że ​​masz pojęcie „liczb naturalnych” wykraczające poza ich definicję Peano i pewne pojęcie o tym, co jest prawdziwe lub fałszywe dla liczb naturalnych bez wyprowadzenia tych prawd z jakiegokolwiek określonego zestawu aksjomatów. Próba wyjaśnienia, skąd pochodzą te prawdy lub jak można je zweryfikować, może doprowadzić cię do filozoficznej gorącej wody. Ale jeśli weźmiesz to za pewnik, że istnieją liczby naturalne i istnieje zbiór prawdziwych faktów na ich temat, możesz postrzegać projekt aksjatyzacji jako próbę wymyślenia zwięzłej specyfikacji formalnej, z której wiele najważniejszych prawdy można wyprowadzić. Zatem aksjatyzacja jest słuszna, jeśli wszystko, co może faktycznie udowodnić, znajduje się we wcześniej określonym zbiorze prawd, to znaczy

(Zwróć uwagę w szczególności, że twoja formalna specyfikacja nie udowodni wszystkiego , co jest prawdą w liczbach naturalnych, a ponadto nie będzie jednoznacznie opisywać liczb naturalnych, ponieważ istnieją inne struktury, inne niż liczby naturalne, w których aksjomaty Peano są też prawda.)

Przynajmniej w logice pierwszego rzędu teoria jest spójna, jeśli ma jakieś modele. Solidność oznacza, że ​​ma określony model, który chciałeś: konkretna struktura, którą próbujesz opisać swoją teorią, naprawdę jest modelem twojej teorii. Z tej perspektywy jasne jest, dlaczego solidność oznacza spójność.

$\neg$

$\neg$$\mathbb N$

$\neg$

Jeszcze jedno: nie zakładamy, że aksjomaty są z definicji prawdziwe. Wszystkie aksjomaty są z definicji tylko podstawowymi elementami składowymi dowodów. Są tylko twierdzeniami: są prawdziwe lub fałszywe, gdy odnoszą się do konkretnych obiektów matematycznych. Możesz mieć fałszywe aksjomaty, to po prostu dość głupie, ponieważ twój system będzie wtedy koniecznie i natychmiast nie zabrzmiał.

Aby uzyskać zwięzłą (i intuicyjną) odpowiedź, sparafrazuję to, co powiedział Scott Aaronson w swoim wykładzie 6.045 / 18.400 MIT. Powiedział coś takiego:

Zdrowość oznacza, że ​​wszystko, co można udowodnić, jest prawdą. Ponieważ spójność oznacza, że ​​nie ma już sprzeczności, a prawość już dotyczy pojęcia prawdy, a prawda musi być spójna (tj. Prawda! = Fałsz), to musi oznaczać, że systemy dźwiękowe są również spójne. Więc Zdrowość oznacza konsekwencję, ponieważ (prawdziwie) prawdziwe rzeczy nie mają sprzeczności.

Teraz, gdy się zastanawiam, zdaję sobie sprawę, że miałem kilka błędnych założeń / pomysłów:

1. Nie zdawałem sobie sprawy, że solidność dotyczy semantyki. Dlatego nie zdawałem sobie sprawy, że samo użycie reguł wnioskowania z aksjomatów nie wystarcza, aby doprowadzić do prawdziwych konsekwencji (i że nie gwarantuje tego, co moim zdaniem nie było możliwe do osiągnięcia sprzecznych rzeczy, dopóki zaczynaliśmy od aksjomatów i zastosowane prawidłowe reguły wnioskowania).
2. Pomyślałem, że dopóki aksjomaty są prawdziwe, a reguły wnioskowania mają sens, wszystko, co nastąpi, będzie prawdą. To, co teraz zdaję sobie sprawę, może nie być prawdą, ponieważ jeśli mamy gigantyczną listę aksjomatów i wnioskowania, trudno jest uzasadnić, czy wszystko, co następuje, będzie prawdą. tzn. samo rozpoczęcie od aksjomatu i użycie prawidłowej reguły wnioskowania nie wystarczy, aby zagwarantować, że następny krok będzie prawdziwy.
3. Poprzedni jest zasadniczo połączony z faktem, że nie zdawałem sobie sprawy, że istnieją dwa poziomy złożoności, 1) semantyka 2) składnia. Rozkręcanie gry w chrupanie symboli może prowadzić do sprzeczności.
4. Nie zdawałem sobie sprawy, że nie znam właściwej charakterystyki prawdy, którą Derek wykonał świetną robotę w charakteryzowaniu.