Czy istnieje logiczna koncepcja „Turing Complete”?

Można wykazać, że dwa modele obliczeniowe są kompletne, jeśli każdy z nich może zakodować uniwersalny symulator dla drugiego. Można wykazać, że dwie logiki są kompletne, jeśli kodowanie reguł wnioskowania (i może aksjomatów, jeśli są obecne) każdego z nich jest twierdzeniem drugiej. W obliczeniach doprowadziło to do naturalnego pomysłu kompletności Turinga i tezy Kościoła Turinga. Nie widziałem jednak, gdzie logiczne dopełnienia doprowadziły do ​​jakiegokolwiek naturalnie wywołanego pomysłu całkowitej kompletności o podobnej jakości.

Ponieważ dostępność i obliczalność są tak ściśle ze sobą powiązane, myślę, że nie należy zbytnio myśleć, że może istnieć koncepcja logiczna, która jest naturalnym dublem w stosunku do kompletności Turinga. Spekulacyjnie coś w rodzaju: istnieje „prawdziwe” twierdzenie, które nie jest możliwe do udowodnienia w logice tylko wtedy, gdy istnieje funkcja obliczalna, której nie da się opisać modelem obliczeniowym. Moje pytanie brzmi, czy ktoś to studiował? Przydałoby się odniesienie lub niektóre słowa kluczowe.

Przez „prawdziwe” i „obliczalne” w poprzednim akapicie odnoszę się do intuicyjnych, ale ostatecznie niemożliwych do zdefiniowania pomysłów. Na przykład ktoś mógłby wykazać, że skończoność sekwencji Goodsteina jest „prawdziwa”, ale nie da się jej udowodnić w arytmetyki Peano bez pełnego zdefiniowania pojęcia „prawda”. Podobnie poprzez diagonalizację można wykazać, że istnieją funkcje obliczeniowe, które nie są prymitywnymi rekurencyjnymi, bez faktycznego pełnego zdefiniowania pojęcia obliczalności. Zastanawiałem się, mimo że ostatecznie są to pojęcia empiryczne, być może pojęcia te mogą być ze sobą powiązane wystarczająco dobrze, aby odnieść się do pojęcia kompletności.

Nie jestem pewien, dlaczego mówisz „prawda” jest ostatecznie nieokreślony, ponieważ istnieje precyzyjna definicja tego, co oznacza, że ​​formuła pierwszego rzędu jest prawdziwa .

Unikalne w przypadku obliczalności jest to, że dla dowolnej definicji (tak dzikiej jak twoje marzenia) dla „modelu obliczeniowego” można w końcu powiązać go z zestawem funkcji (funkcjami, które może obliczyć). W ten sposób można w naturalny sposób porównać różne modele, a po ustaleniu jednego (na podstawie pewnego empirycznego uzasadnienia, takiego jak „jest to dobra reprezentacja obliczeń w świecie rzeczywistym”), można nazwać dowolny inny model kompletny, jeśli oblicza dokładnie ten sam zestaw Funkcje.

Jak jednak porównać różne logiki? Wygląda na to, że nie ma naturalnej właściwości, którą można przypisać do dowolnej logiki i użyć jej do porównania z innymi systemami. Być może możesz naprawić logikę, np. Logikę predykatu pierwszego rzędu i zapytać o kompletność systemu aksjomatycznego. Załóżmy, że pracujesz w ZFC i uwierz, że składa się on z naturalnych aksjomatów reprezentujących świat. Teraz, gdy otrzymamy inny system aksjomatyczny, możesz zapytać, czy mają one tę samą teorię, i nazwij ten system kompletnym, jeśli odpowiedź brzmi „tak”. Myślę, że różnica w porównaniu z przypadkiem obliczalności polega na tym, że w przypadku obliczalności istnieje silniejszy konsensus co do tego, jaki powinien być „model podstawowy”. Powodem tego konsensusu jest to, że wiele niezależnych modeli obliczeń okazało się później równoważnych,