Czy dowód sprzeczności może działać bez prawa wykluczonego środka?

Niedawno myślałem o ważności dowodu sprzeczności. Przez kilka ostatnich dni czytałem o intuicyjnej logice i twierdzeniach Godela, aby sprawdzić, czy dostarczyłyby mi odpowiedzi na moje pytania. W tej chwili wciąż mam pytania (być może związane z nowym materiałem, który czytam) i liczyłem na kilka odpowiedzi

( OSTRZEŻENIE : masz zamiar czytać treść z bardzo zagmatwanymi podstawami w logice, wziąć wszystko z odrobiną soli, przypuszczalnie jest to pytanie, a nie odpowiedź, jest w tym wiele nieporozumień).

Wydaje mi się, że moim głównym pytaniem jest to, że kiedy pokazaliśmy, że nie A prowadzi do sprzeczności, więc A nie musi być fałszywe, wtedy dochodzimy do wniosku, że A musi być prawdą. Ta część ma sens (zwłaszcza jeśli akceptuję prawo wykluczonego środka jako coś, co ma sens), ale niepokoi mnie to, w jaki sposób faktycznie pojawia się dowód sprzeczności. Najpierw zaczynamy od A, a następnie po prostu stosujemy aksjomaty i reguły wnioskowania (powiedzmy mechanicznie) i sprawdzamy, dokąd nas to zaprowadzi. Zwykle dochodzi do sprzeczności (powiedz, że A jest prawdą lub $\neg \varphi$ i $\phi$ jest prawdą). Stwierdzamy, że nie A musi być fałszywe, więc A jest prawdziwe. W porządku. Ale moje pytanie brzmi: jakie gwarancje mają takie formalne systemyjeśli zastosowałbym ten sam proces, ale zacząłem od A, że nie dostałbym tam również sprzeczności ? Wydaje mi się, że istnieją pewne ukryte przypuszczenia potwierdzone sprzecznościami, że gdyby podobnie ten sam proces w A nie osiągnąłby sprzeczności , jakie mamy gwarancje, które by się nie wydarzyły? Czy istnieje dowód, który jest niemożliwy? Innymi słowy, gdybym miał Tokarkę (TM) (lub super TM), która poszła na zawsze, która wypróbowała wszystkie logiczne kroki z każdego aksjomatu, poczynając od rzekomo prawdziwego stwierdzenia $A$ , co gwarantuje, że NIE ZATRZYMUJE się z powodu znalezienia sprzeczności ?

Później nawiązałem pewne powiązania z moim przeszłym pytaniem z twierdzeniem Godela o niekompletności, które brzmi mniej więcej tak:

System formalny F, który wyraża arytmetykę, nie może udowodnić swojej spójności (w obrębie F).

To w zasadzie wyjaśniło mi, że jeśli to prawda, to konsekwencja, tj. Zagwarantowanie, że A, a nie A się nie wydarzy, jest niemożliwa. Dlatego wydaje się, że wydaje się, że dowód sprzeczności po prostu domyślnie zakłada, że ​​spójność jest w jakiś sposób gwarantowana (w przeciwnym razie dlaczego miałby po prostu iść dalej i stwierdzić, że A jest prawdą, wykazując, że A nie jest możliwe, gdyby nie wiedział już o tej spójności i sprzeczność, gdzie w porządku, dla dowolnej pary stwierdzeń A, a nie A)? Czy to jest nieprawidłowe, czy coś przeoczyłem?

Pomyślałem wtedy: ok, po prostu uwzględnijmy w naszych aksjomatach zasadę wykluczonego środka, a wtedy wszystkie problemy zostaną rozwiązane. Ale potem zdałem sobie sprawę, poczekaj, jeśli to zrobimy, po prostu definiujemy problem, zamiast go rozwiązać. Jeśli po prostu zmuszę mój system do zachowania spójności z definicji, niekoniecznie oznacza to, że faktycznie jest spójny… prawda? Próbuję po prostu zrozumieć te pomysły i nie jestem do końca pewien, co robić, ale właśnie to realizuję po kilku dniach czytania rzeczy i oglądania filmów w prawie każdym aspekcie tych koncepcji, sprzeczności, wyjątkowego środka, logika intuicyjna, twierdzenia o kompletności i niekompletności Godela…

W związku z tym wydaje się, że w zasadzie niemożliwe jest bezpośrednie udowodnienie, że coś jest fałszywe bez reguły wykluczonego środka (lub sprzeczności). Wydaje się, że systemy dowodowe dobrze sprawdzają się w prawdziwych stwierdzeniach, ale moim zdaniem nie są w stanie bezpośrednio wykazać, że wszystko jest fałszywe. Być może sposób, w jaki to robią, jest bardziej pośredni ze sprzecznością (gdzie pokazują, że coś musi być fałszywe lub coś złego się dzieje), lub wykluczony środek (gdzie znajomość wartości prawdy tylko jednego A lub nie A daje nam prawdę drugiego) lub dostarczanie przeciwnych przykładów (co w zasadzie pokazuje, że jest odwrotnie, więc pośrednio stosuje prawo wykluczonego środka). Chyba naprawdę chcę konstruktywnego dowodu, że coś jest fałszywe?

Myślę, że gdybym wiedział, że jeśli nie udowodnię, że A jest fałszywe (powiedzmy, że akceptuję sprzeczność), to naprawdę jest w porządku i nie muszę stosować wszystkich reguł wnioskowania i aksjomatów w nieskończoność do A i mam gwarancję, że A wygrał osiągnąć sprzeczność. Gdyby to była prawda, myślę, że łatwiej byłoby zaakceptować dowód sprzeczności. Czy to prawda, czy też druga niekompletność Godela gwarantuje, że nie mogę tego mieć? Jeśli nie mogę tego mieć, to co mnie zastanawia, jak to możliwe, że tylu lat matematyków robi matematykę, że nie znaleźliśmy niespójności? Czy muszę polegać na empirycznych dowodach spójności? Lub na przykład, czy prof F jest konsekwentny, pokazując, że superF dowodzi, że F, ale skoro tak naprawdę nigdy nie będę potrzebować superF i tylko F, ​​to nie mogę być treścią, która naprawdę działa?

Właśnie zauważyłem, że moja skarga obejmuje również bezpośrednie dowody. Ok, więc jeśli zrobiłem bezpośredni dowód A, to wiem, że A jest prawdą ... ale skąd mam wiedzieć, że jeśli zrobiłem bezpośredni dowód nie A, to nie dostałbym również prawidłowego dowodu? Wydaje się, że to samo pytanie tylko nieco inny nacisk ...

Pytałeś (Robię swoje pytanie nieco wyraźniejszy): „Co formalny jest gwarancja, że nie może się zdarzyć, że zarówno i p prowadzić do sprzeczności?” Wydaje się, że martwisz się, że jeśli logika jest niespójna, wówczas dowodzenie przez sprzeczność jest problematyczne. Ale wcale tak nie jest.$\lnot p$$p$

Jeśli logika jest niespójna, dowodem sprzeczności jest nadal bardzo ważna reguła rozumowania, ale także jej negacja i reguła, która mówi, że z możemy wnioskować, że jesteś następnym papieżem. Niespójność w logice niczego nie unieważnia: wręcz przeciwnie, potwierdzawszystko!$1 + 1 = 2$

Istnieje inne możliwe źródło nieporozumień: tytuł pytania można odczytać jako sugerujący, że prawo wykluczonego środka mówi, że logika jest spójna. To jest niepoprawne. Spójność logiki sprowadza się do „nie jest tak, że zarówno stwierdzenie, jak i jego negacja mają dowody”, podczas gdy wykluczony środek jest regułą, która pozwala nam udowodnić twierdzenia w formie .$p \lor \lnot p$

Uzupełnienie: Nie rozumiem, dlaczego to pytanie powoduje tyle dyskusji. Mam problem ze zrozumieniem, czym tak naprawdę jest dylemat, i o ile mogę stwierdzić, pytanie wynika z pewnego rodzaju nieporozumień. Jeśli ktoś może wyjaśnić pytanie, będę wdzięczny. Chciałbym również zwrócić uwagę na następujące kwestie:

1. Dowód sprzeczności i wykluczony środek są sobie równe, a zatem tytuł, jak napisano, nie ma sensu. Oczywiście nie możemy mieć jednego bez drugiego, są one równoważne.

2. Z tego, co rozumiem z długiej dyskusji w tym pytaniu, OP wydaje się mówić lub martwić, że niespójność logiczna unieważnia dowód. To nieprawda, jak wskazałem powyżej. Byłbym wdzięczny za jakąś odpowiedź PO: czy PO może zobaczyć, w jaki sposób niespójność w logice (tj. Możliwość udowodnienia wszystkiego) nie unieważnia żadnych dowodów?

3. Wydaje mi się prawdopodobne, ale nie mogę powiedzieć na pewno, że OP uważa, że ​​prawo wykluczonych środków środkowych stwierdza, że ​​niemożliwe jest utrzymanie zarówno jak i ¬ p (ze wzorem: ¬ ( p $p$$\lnot p$ ). Nie jest to wykluczone w środku. Czasami nazywa się to prawem braku sprzeczności i można to udowodnić (bez wykluczonego środka).$\lnot (p \land \lnot p)$

4. OP uważa, że ​​„niemożliwe jest bezpośrednie udowodnienie, że coś jest fałszywe bez wykluczonego środka”. Jest mylącym dowodem negacji i dowodem sprzeczności, które nie są tym samym . Powiązany post zawiera wiele przykładów konstruktywnych dowodów na to, że coś jest fałszywe. W rzeczywistości większość dowodów na to, że coś jest fałszywe w podręcznikach, jest już konstruktywna.

5. Niepełność Gödela została wciągnięta z powodu, który mogę dostrzec. Niekompletność Gödla przewiduje karę taki, że ani G ani ¬ G jest udowodnić. Nie oznacza to , że G ∨ ¬ G jest nie do udowodnienia (przez proste zastosowanie wykluczonego środka)! Nie oznacza to również, że ¬ G ∧ ¬ $G$$G$$\lnot G$$G \lor \lnot G$ posiada, lub niektóre podobne. Więc w jaki sposób niekompletność Gödela jest tutaj istotna?$\lnot G \land \lnot\lnot G$

PS Przepraszam za poprzednią wersję suplementu, która była niegrzeczna.

Myślę, że twoje pytanie sprowadza się do „podczas formalnej weryfikacji za pomocą jakiejś formalnej logiki, jaką mam gwarancję, że logika jest spójna?”. Odpowiedź brzmi: brak. To coś, co musisz założyć. Formalna weryfikacja nie eliminuje wszystkich założeń; po prostu pomaga ci wyjaśnić, co zakładasz, a może pomaga ci zacząć od założeń, które wydają się rozsądne.

Jeśli pracujesz w ramach standardowej logiki, generalnie większość ludzi chętnie przyjmuje, że logika jest spójna, nawet jeśli nie mają na to dowodów. To prawda, że ​​pewnego dnia możemy odkryć, że logika jest niespójna ... ale większość ludzi uważa, że ​​jest to mało prawdopodobne.

W niektórych przypadkach można udowodnić, że logika jest spójny, ale wymaga użycia innego mocniejszy logiki, gdzie musimy założyć, że druga logika jest spójny, więc nadal pozostają konieczności dokonać pewnych założeń (zakładamy, że niektóre logika jest zgodny ). Można to uznać za dowód na to, że pierwsza logika jest prawdopodobnie spójna, jeśli uważasz, że druga logika jest prawdopodobnie spójna, ale rozumowanie musi gdzieś być na dole - są pewne rzeczy, które musimy po prostu założyć i których nie możemy udowodnić.

Zobacz np . Drugi problem Hilberta i ta dyskusja na temat spójności ZFC (i to i to i to i prawdopodobnie wiele innych).

Istnieje wiele interesujących filozoficznych punktów, które poruszają twój post.

Spójność logiki boolowskiej

Kwestia spójności teorii dowodów w logice klasycznej nie jest tak straszna, jak się wydaje. Zasadniczo sprowadza się do:

Możemy zdefiniować logikę logiczną jako zbiór funkcji operacji logicznych na wartościach prawdy 1i 0. Ale skąd to wiemy 0≠1?

(zauważ, że po prostu używam 0i 1jako abstrakcyjne symbole dwóch wartości prawdy; w szczególności nie zakładam tutaj pojęcia liczby całkowitej)

My, oczywiście, nie wiem, że 0i 1są różne. Ale logika boolowska jest tak absurdalnie prosta, że ​​odrzucenie tej możliwości jest skrajnym poziomem sceptycyzmu.

Ale klasyczna logika zdań ogranicza się do tego. Przypomnijmy, że możemy przypisywać wartości boolowskie do zdań atomowych w dowolny sposób, a to rozciąga się na przypisywanie wartości do wszystkich zdań, które można zbudować z tych atomowych.

Stwierdzenie „od Pciebie można wywnioskować Q” jest dosłownie tylko relacją porządkową; oznacza to to samo, co twierdzenie, że „obowiązuje v(P) ≤ v(Q)dla każdej funkcji vprzypisującej wartości prawdy do zdań atomowych”.

Reguły wnioskowania dla logiki zdań są właśnie właściwościami do pracy z porządkowaniem ≤. W szczególności dowodem sprzeczności jest spostrzeżenie, że jeśli P ≤ 0, to wtedy P = 0.

Wracając do waszego problemu ... gdybyśmy wiedzieli jedno P ≤ 0i drugie, a ¬P ≤ 0po wprowadzeniu wartości prawdy ostatecznie do tego dojdziemy 0=1; prawda i fałsz oznaczają to samo.

Jeśli więc masz pewność, że „prawda” i „fałsz” oznaczają różne rzeczy, powinieneś mieć podobne zaufanie do spójności logiki logicznej.

Dowód sprzeczności w logice intuicyjnej

Należy uważnie zauważyć, że dowód sprzeczności lepiej sformułować jako:

• Jeśli możesz wywodzić sprzeczność P, to wyciągnij wniosek¬P

W rzeczywistości można wprost zdefiniować negację jako łącznik z tą właściwością. Np. W algebrze Heytinga zwykle widzisz ¬P zdefiniowane jako P → 0.

Zwróć uwagę w szczególności na przypadek szczególny

• Jeśli możesz wywodzić sprzeczność ¬P, to wyciągnij wniosek¬¬P

To, co opisałeś jako „dowód sprzeczności”, pochodzi z utożsamiania się ¬¬Pz P. Logika intuicyjna nie zakłada, że ​​są one równoważne.

Spójność jako formalna umowa

Istnieje więcej formalizmów obliczeniowych do kodowania logiki; patrz po prostu typowany rachunek lambda, typy zależne, a w szczególności paradygmat „zdań jako typów”.

Bez wchodzenia w szczegóły sprzeczność jest zasadniczo traktowana jako formalna umowa. Istnieje typ, który wywołam 0, i istnieje umowa „tych funkcji nie można użyć do zbudowania elementu typu 0”.

Jeśli taki system jest tak odważny, że pozwala ci zbudować funkcję T → 0, to jeśli tak naprawdę trzyma się kontraktu, oznacza to, że podobnie niemożliwe jest zbudowanie jakichkolwiek obiektów typu T. Jest to obliczeniowy punkt widzenia na to, co oznacza dowód sprzeczności.

Ostatecznie nie różni się to tak bardzo, jak na przykład funkcja C, która zwraca wskaźnik obiecujący, że nie zwróci wskaźnika zerowego, lub funkcja C ++, która obiecuje, że nie zgłosi wyjątku.

I zataczając koło, wracając do klasycznej logiki, właśnie to robimy.

Proponowane są nam formalne umowy, takie jak „z aksjomatów Peano, reguły wnioskowania nie pozwalają na wyciągnięcie sprzeczności”. Jeśli ta umowa jest rzeczywiście przestrzegana, to jeśli byłeś w stanie wykazać, że ¬Poznacza to sprzeczność, Pnie możesz również sugerować sprzeczności.

Gdyby można było złamać umowę, powiedzielibyśmy po prostu: „Aksjomaty Peano są niespójne”.

W przypadku zagwarantowania prawdziwości formalnego oświadczenia wszystkie dowody domyślnie zakładają spójność systemu, w którym są oparte. Dzieje się tak, ponieważ jeśli system jest niespójny, cały system jest zepsuty, a cała praca, którą wykonaliśmy w tym systemie jest w zasadzie śmieci.

Ponieważ nie możemy udowodnić, że jakikolwiek system (lub przynajmniej jakikolwiek złożony system) jest spójny w ramach tego systemu, musimy traktować go jako prawdę empiryczną, a nie prawdę formalnie możliwą do udowodnienia. Zasadniczo, jeśli matematycy spędzają dużo czasu pracując z systemem formalnym i nigdy nie zostanie odkryta sprzeczność, to są to dowody empiryczne na korzyść spójności systemu. Ponadto możemy użyć mocniejszego systemu, aby udowodnić spójność systemu, z którym pracujemy (chociaż spójność tego mocniejszego systemu byłaby nadal empiryczna - gdzieś buck się zatrzymuje).

U podstaw sytuacja w matematyce jest identyczna jak w nauce. Budujemy matematykę na podstawie teorii, które wydają się poprawne, na podstawie wszystkich dostępnych informacji na temat tych teorii i podobnie jak w nauce nie można udowodnić, że teoria jest poprawna; możesz tylko udowodnić, że jest niepoprawny.

$S$ będzie zbiorem wszystkich zbiorów, które się nie zawierają”. Musieliśmy wyrzucić te formuły.

Bez względu na to, na którym systemie aksjomatów wybieramy matematykę, zawsze istnieje niebezpieczeństwo, że odkryjemy sprzeczność w tym systemie. Właśnie dlatego matematycy nie wprowadzają do matematyki nowych aksjomatów: każdy nowy aksjomat ma szansę być niezgodny z już używanymi aksjomatami, a wszelkie prace, które wykorzystują nowy aksjomat, powinny zostać całkowicie ponownie ocenione.

Dodatek: Kiedy mówię o stwierdzeniu, które jest prawdziwe dla danego systemu, mam na myśli, że nie można go obalić w tym systemie, jeśli ten system jest spójny.