Czy możliwe są rekurencyjne formy wypowiedzi Godela?

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?

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 .

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ć?

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).