Czy możliwe są rekurencyjne formy wypowiedzi Godela?


20

Samoreferencyjność problemu P / NP była czasem podkreślana jako bariera dla jego rozwiązania, patrz na przykład artykuł Scotta Aaronsona, czy P vs. NP jest formalnie niezależny ? Jednym z wielu możliwych rozwiązań P / NP byłby dowód, że problem jest formalnie niezależny od ZFC lub prawdziwy, ale niemożliwy do udowodnienia.

Można sobie wyobrazić, że samo-referencyjność problemu może stanowić głębsze wyzwanie w dowodach niezależności, na przykład, jeśli stwierdzenia o jego udowodnieniu są same w sobie nie do udowodnienia lub w inny sposób niemożliwe do uzasadnienia.

Załóżmy, że nazywamy twierdzenie T Godel_0, jeśli jest prawdziwe, ale nie do udowodnienia w sensie twierdzenia Godela. Zadzwoń do T Godel_1, jeśli wyrażenie „T to Godel_0” jest prawdziwe, ale nie do udowodnienia. Zadzwoń do T Godel_i, jeśli zdanie „T to Godel _ {(i-1)} jest prawdziwe.

Wiemy, że istnieją instrukcje Godel_0 i znaleziono kilka przykładów „na wolności”, które nie zostały skonstruowane wyraźnie w tym celu, jak w tym artykule .


Moje pytanie brzmi: czy istnieją jakieś oświadczenia Godel_1 lub wyższe? Czy takie stwierdzenia są naturalną konsekwencją twierdzenia Godela?

A co ze stwierdzeniem, o którym absolutnie nic nie możemy udowodnić: tj. Takim , dla którego dla każdego k > 0, T jest Godel_k?

Mogę zadać analogiczne pytanie o formalną niezależność, chociaż podejrzewam, że odpowiedź brzmi „nie”.

Aby powrócić do pytania P vs. NP, pozwól mi zapytać, czy istnieje jakaś wskazówka, że ​​twierdzenie Godela jest istotne w kwestiach dotyczących rozdzielności klas. Czy zidentyfikowano jakieś prawdziwe, ale nie dające się udowodnić stwierdzenia w odniesieniu do klas złożoności - poza oczywiście oczywistym związkiem między problemem zatrzymania a twierdzeniem Godela?


Może to być bardziej odpowiednie dla logików z MO - zachęcamy do wskazania, czy tak jest.
Anand Kulkarni,

Odpowiedzi:


14

Jak zauważyli inni, istnieją pewne trudności techniczne z odpowiedzią na twoje pytanie. Aby je wyprostować, zacznijmy od unikania używania terminu „nie do udowodnienia” bez kwalifikacji i wyraźnego określenia, z którego zestawu aksjomatów powinno być niemożliwe stwierdzenie T. Załóżmy na przykład, że interesują nas stwierdzenia T, których nie da się udowodnić z PA, aksjomaty arytmetyki Peano pierwszego rzędu.

Pierwszą irytacją jest to, że „T jest prawdą” nie wyraża się w języku arytmetyki pierwszego rzędu, według twierdzenia Tarskiego. Możemy to obejść, pracując w metateorii, która jest wystarczająco silna, aby zdefiniować prawdziwość arytmetycznego stwierdzenia, ale myślę, że dla twoich celów jest to niepotrzebnie skomplikowana droga. Myślę, że nie interesujesz się prawdą jako taką, ale sprawdzalnością. To znaczy, podejrzewam, że byłbyś zadowolony ze zdefiniowania T jako Godel_0, jeśli T jest prawdziwe, ale nie do udowodnienia w PA, i zdefiniowania T jako Godel_1, jeśli T jest nie do udowodnienia w PA, ale „T jest nie do udowodnienia w PA” jest nie do udowodnienia w PA, i zdefiniowanie T jako Godel_2, jeśli T jest nie do udowodnienia w PA i „T jest nie do udowodnienia w PA” jest nie do udowodnienia w PA, ale „„ T jest nie do udowodnienia w PA ”jest nie do udowodnienia w PA” itp. W ten sposób nie

To wystarczy, aby sprecyzować twoje pytanie, ale niestety istnieje wtedy dość trywialne rozwiązanie. Weź T = „PA jest spójny”. Zatem T jest prawdą, ponieważ PA jest spójne, a T jest niemożliwe do udowodnienia w PA przez twierdzenie Goedela o drugiej niekompletności. Ponadto, „T jest nie do udowodnienia w PA” jest również nie do udowodnienia w PA z nieco głupiego powodu: każde stwierdzenie w formie „X jest nie do udowodnienia w PA” jest nie do udowodnienia w PA, ponieważ „X jest nie do udowodnienia w PA” trywialnie oznacza, że ​​„PA jest spójne „(ponieważ niespójne systemy dowodzą wszystkiego ). Więc T jest Godel_n dla wszystkich n, ale tak naprawdę nie dostaję się do zamierzonego pytania.

Możemy spróbować „załatać” twoje pytanie, aby uniknąć takich błahości, ale zamiast tego pozwól mi spróbować odpowiedzieć na to, co moim zdaniem jest twoim zamierzonym pytaniem. Milcząco wierzę, że łączysz logiczną siłę potrzebną do udowodnienia twierdzenia z trudnością psychicznąudowodnienia tego. Oznacza to, że interpretujesz wynik formy „T jest nie do udowodnienia w X” jako stwierdzenie, że T jest w jakiś sposób poza naszą zdolnością do zrozumienia. Są tam te potworne domysły, a my, mizerni ludzie, trzaskamy biczami PA lub biczami ZFC lub czymś innym u tych dzikich bestii, próbując je oswoić. Ale nie sądzę, że „T jest nie do udowodnienia w X” należy interpretować w ten sposób, że „T jest niemożliwy do uzasadnienia”. Zamiast tego mierzy tylko określoną właściwość techniczną dotyczącą T, a mianowicie jego siłę logiczną. Więc jeśli próbujesz wymyślić über-potwora, nie sądzę, że znalezienie czegoś, co jest nie tylko niemożliwe do udowodnienia, ale którego nie można udowodnić itp., Jest właściwym kierunkiem.

Wreszcie, jeśli chodzi o twoje pytanie, czy niedopuszczalność wydaje się w ogóle związana z rozdzielnością klas złożoności, istnieją pewne powiązania między trudnością obliczeniową a niedopuszczalnością w niektórych systemach ograniczonej arytmetyki. Niektóre z nich wspomniane są w cytowanym przez Aaronsona artykule; patrz także książka Cooka i Nguyena Logiczne podstawy dowodu złożoności .


Rzeczywiście, twój trywialny przykład rozwiązuje pytanie i cieszę się, że miał tak proste rozwiązanie - podejrzewałem, że takie stwierdzenia były prawdopodobnie równoważne. Jednak interesuje mnie tylko siła logiczna, a nie psychologiczna trudność udowodnienia lub uzasadnienia rzeczy. Moim pytaniem było zadać pytanie: „czy formalnie trudniej jest udowodnić niedopuszczalność stwierdzenia niż udowodnić, że stwierdzenie jest niemożliwe do udowodnienia?” Twój przykład sugeruje, że odpowiedź brzmi „nie”.
Anand Kulkarni

Nie do końca rozumiem twoje przeformułowane pytanie, ponieważ nadal używasz słowa „nie do udowodnienia” bez kwalifikacji. Powiedz, że T1 jest nie do udowodnienia w X1. Wtedy „T1 jest nie do udowodnienia w X1” (nazwij to stwierdzenie T2) jest możliwe do udowodnienia w niektórych systemach, a nie w innych. Czy jesteś zainteresowany (nie) sprawdzalnością T2 w samym X1 lub w innym systemie X2? Jeśli to drugie, to na ogół będą istnieć systemy X3, które dowodzą T2, ale nie „T2 nie jest możliwe do udowodnienia w X2”.
Timothy Chow,

8

Nie jestem pewien co do definicji Godel_1. Czy możesz spróbować sformalizować to trochę bardziej?

Jak możesz zakodować formułę „T to Godel_0”? W tym celu trzeba w jakiś sposób zakodować, że „T jest semantycznie prawdziwe” bez odwoływania się do pojęcia dowodu. Jak możesz to robić?


1
Doskonały punkt Pojęcie Prawdy jest niemożliwe do zakodowania w spójnej logice „wystarczająco silnej”.
ripper234,

Jak sugerujesz, nie jestem pewien, czy to stwierdzenie może zostać sformalizowane bez jasno określonych pojęć prawdy i udowodnienia. Zakładam, że jest oczywiste, co mam na myśli w nieformalnym sensie: stwierdzenie T to Godel_1 iff oświadczenie „T jest prawdziwe, ale nie do udowodnienia” jest prawdziwe, ale nie do udowodnienia. Jeśli zdanie Godela jest luźno „Nie istnieje żaden dowód tego twierdzenia”, wówczas zdanie Godel_1 mogłoby brzmieć: „Nie istnieje żaden dowód twierdzenia„ nie istnieje żaden dowód tego twierdzenia ”. jednak wewnętrzne oświadczenie jest prawdziwe
Anand Kulkarni

6

Dla każdego n istnieją instrukcje Godel_n. Być może zainteresuje Cię książka The Unproviable of Consistency, autorstwa George'a Boolosa. Definiuje logikę modalną, w której Box oznacza „można udowodnić,„ Diament oznacza ”jest spójny”, a następnie przystępuje do badania zachowania zdań typu Godela. (Napisał także książkę uzupełniającą, The Logic of Provability).


Czy mógłbyś rozwinąć wyniki Boolos? Czy udowodni, że takie stwierdzenia istnieją?
Anand Kulkarni,

Argh. Przeczytałem pierwszą książkę, nie drugą, ale to było milion lat temu, kiedy myślałem, że będę logiką, kiedy dorosnę. Nawet sprzedałem swój egzemplarz książki do księgarni. Mogę sprawdzić, czy znajduje się tutaj w bibliotece. Gdybym spojrzał na to jeszcze raz, prawdopodobnie mógłbym szybko zapamiętać rzeczy. Żadnych obietnic i przepraszam, nie jestem więcej pomocą.
Aaron Sterling
Korzystając z naszej strony potwierdzasz, że przeczytałeś(-aś) i rozumiesz nasze zasady używania plików cookie i zasady ochrony prywatności.
Licensed under cc by-sa 3.0 with attribution required.