Czy w logice konstruktywistycznej istnieją niezdecydowane języki?

Logika konstruktywistyczna to system, który usuwa Prawo Akceptowanego Środka, a także Podwójną Negację, jako aksjomaty. Jest opisany na Wikipedii tutaj i tutaj . W szczególności system nie dopuszcza dowodu sprzeczności.

Zastanawiam się, czy ktoś wie, jak to wpływa na wyniki dotyczące maszyn Turinga i języków formalnych? Zauważam, że prawie każdy dowód, że język jest nierozstrzygalny, opiera się na dowodzie sprzeczności. Zarówno argument diagonalizacji, jak i koncepcja redukcji działają w ten sposób. Czy kiedykolwiek może istnieć „konstruktywny” dowód istnienia nierozstrzygalnego języka, a jeśli tak, to jak by to wyglądało?

EDYCJA: Żeby było jasne, moje rozumienie dowodu przez sprzeczność w logice konstruktywistycznej było błędne i odpowiedzi wyjaśniły to.

Tak. Nie potrzebujesz wykluczonego środka, aby uzyskać sprzeczność. W szczególności diagonalizacja nadal działa.

Oto typowy argument przekątnej Conora McBride'a. Ta szczególna diagonalizacja dotyczy niepełności, a nie nierozstrzygalności, ale idea jest taka sama. Ważnym punktem, na który należy zwrócić uwagę, jest to, że wywodząca się z niego sprzeczność nie ma formy „P, a nie P”, ale formy „x = x + 1”.

Oczywiście teraz możesz zastanawiać się, czy logika konstruktywna dopuszcza „x = x + 1” jako sprzeczność. To robi. Główną właściwością sprzeczności jest to, że cokolwiek wynika z sprzeczności i używając „x = x + 1”, rzeczywiście mogę konstruktywnie udowodnić „x = y” dla dowolnych dwóch liczb naturalnych.

Jedną rzeczą, która może się różnić w konstruktywnym dowodzie, jest sposób definiowania „nierozstrzygalnego”. W logice klasycznej każdy język musi być rozstrzygalny lub nierozstrzygalny; więc „nierozstrzygalne” oznacza po prostu „nierozstrzygalne”. Jednak w logice konstruktywnej „nie” nie jest prymitywną operacją logiczną, więc nie możemy w ten sposób wyrazić nierozstrzygalności. Zamiast tego mówimy, że język jest nierozstrzygalny, jeśli założenie, że jest rozstrzygalny, prowadzi do sprzeczności.

W rzeczywistości, chociaż „nie” nie jest prymitywne w konstruktywnej logice, zwykle definiujemy „nie P” jako cukier składniowy dla „P można wykorzystać do skonstruowania sprzeczności”, więc dowód sprzeczności jest w rzeczywistości jedynym sposobem na konstruktywnie udowodnij stwierdzenie w postaci „nie P”, takie jak „język L jest nierozstrzygalny”.

Mówiąc konstruktywnie o sprawdzalności klasycznych stwierdzeń, często ważne jest, jak je sformułujemy. Klasycznie równoważne preparaty nie muszą być konstruktywnie równoważne. Ważne jest również to, co dokładnie rozumiesz przez konstruktywny dowód, istnieją różne szkoły konstruktywizmu.

Na przykład stwierdzenie stwierdzające, że istnieje nieobliczalna funkcja całkowita, nie byłoby prawdziwe w tych odmianach konstruktywnej matematyki, które zakładają tezę Turinga Kościoła (tj. Każda funkcja jest obliczalna) jako aksjomat.

Z drugiej strony, jeśli jesteś ostrożny, możesz sformułować go w taki sposób, aby można go było udowodnić: dla każdego obliczalnego wyliczenia całkowitych funkcji obliczeniowych istnieje całkowita funkcja obliczeniowa, której nie ma w wyliczeniu.

Możesz znaleźć ten post interesujący.

ps: Możemy również spojrzeć na diagonalizację z perspektywy teoretycznej kategorii. Widzieć

• Francis William Lawvere , „ Diagonal Arguments and Cartesian Closed Categories ”, 1969

I pomyśleć że dowód na ważność nadal obowiązuje, co świadczy o istnieniu języków, które nie są językami obliczalnymi (więc zdecydowanie nierozstrzygalnymi).

Bezpośredni dowód jest dość prosty, po prostu zauważa, że ​​Maszyny Turinga są zakodowane w skończonym alfabecie (równie dobrze mogą być binarne), więc jest ich niezliczona liczba i zestaw wszystkich języków w ustalonym alfabecie (równie dobrze może być znowu binarny) ) jest zbiorem wszystkich podzbiorów zbioru ciągów w tym alfabecie - tj. zestawem mocy zbioru policzalnego i musi być niepoliczalny. Dlatego jest mniej maszyn Turinga niż języków, więc czegoś nie da się obliczyć.

Wydaje mi się, że jest to wystarczająco konstruktywne (chociaż nie byłoby możliwe kontynuowanie go fizycznie, daje to sposób wskazania na pewien zestaw języków i znajomość jednego z nich nie do obliczenia).

Możemy wtedy zapytać, czy można pokazać, że zbiory policzalne i niepoliczalne mają inną liczność, w szczególności unikają diagonalizacji. Myślę, że to wciąż możliwe. Oryginalny argument Cantora wydaje się również odpowiednio konstruktywny.

Oczywiście musi to sprawdzić ktoś, kto wie znacznie więcej o logice konstruktywistycznej.

Myślę, że zgadzam się z innymi, że argument diagonalizacji jest konstruktywny, chociaż z tego, co mogę powiedzieć, w niektórych kręgach istnieje pewna różnica zdań.

Załóżmy, że patrzymy na zestaw wszystkich rozstrzygalnych języków. Potrafię zbudować nierozstrzygalny język za pomocą diagonalizacji. Warto zauważyć, że nie uważam „konstruktywizmu” i „finityzmu” za to samo, chociaż historycznie uważam, że były to pokrewne łuki.

Po pierwsze, myślę, że wszyscy - nawet konstruktywiści - zgadzają się, że zbiór rozstrzygalnych języków jest policzalny. Ponieważ zestaw maszyn Turinga jest policzalny (możemy zakodować wszystkie poprawne bazy TM za pomocą skończonych ciągów), umowa ta następuje dość łatwo.

$L_1, L_2, ..., L_k, ...$

1. $0^i$
2. Jeśli $0^i \in L_i$$0^i$
3. $0^i \notin L_i$$0^i$

$n$$L_1, L_2, ..., L_n$ . Po arbitralnej (lub potencjalnie nieskończonej) liczbie kroków nie możemy znaleźć w zestawie języka pasującego do tego, który właśnie stworzyliśmy.

Tak więc technicznie stworzyliśmy język, który „nie jest rozstrzygalny”; to, czy konstruktywista argumentowałby, że „nierozstrzygalnego” nie należy mylić z „nierozstrzygalnym”, jest interesującym pytaniem, ale na które nie jestem w stanie odpowiedzieć.

Aby wyjaśnić, to, co moim zdaniem pokazuje, jest następujące: możemy konstruktywnie udowodnić, że istnieją języki, na które nie decydują maszyny Turinga. Jak wybrać interpretację tego w określonych ramach, jest trudniejsze pytanie.