jeśli (λ x. xx) ma typ, to czy system typów jest niespójny?

Jeśli system typów może przypisać typ do λ x . x xlub do nieterminującego (λx . x x) (λ x . x x), to czy w konsekwencji ten system jest niespójny? Czy każdy typ w tym systemie jest zamieszkały? Czy możesz okazać się fałszywy?

Z pewnością przypisanie typu do to za mało na niespójność: w systemie możemy wyprowadzić $\lambda x. x\ x$$F$

w dość prosty sposób (to dobre ćwiczenie!). Jednak nie można dobrze wpisać w tym systemie, zakładając -konsekwencję arytmetyki drugiego rzędu, ponieważ oznacza to, że wszystkie takie dobrze wpisane terminy są normalizowane.$(\lambda x.x\ x)(\lambda x.x\ x)$ $\omega$

Ponadto system jest spójny. Wynika to z jednej z normalizacji, ponieważ można wykazać, że dowolny termin typu nie może mieć normalnej postaci lub znacznie prostszego argumentu, w którym każdemu typowi jest przypisany zestaw, albo albo i można wykazać, że wszystkie typy pochodnych są przypisane , a ma przypisany (i dlatego nie jest pochodna).$F$$\forall X.X$$\varnothing$$\{\varnothing\}$$\{\varnothing\}$$\forall X.X$$\varnothing$

Ten ostatni argument można przeprowadzić w arytmetyce pierwszego rzędu. Fakt, że może być dobrze wpisany w spójny system, może być postrzegany jako nieco niepokojący i jest konsekwencją impredykatywności tych systemów . Nie powinno dziwić, że niektórzy kwestionują wiarygodność impredykacyjnych systemów logiki. Jak dotąd nie stwierdzono jednak niespójności w takich systemach.$\lambda x.x\ x$

Z drugiej strony, aby móc sformułować bardziej ogólne stwierdzenie, że nie można poprawnie wpisać w spójny system, musisz mieć wystarczającą „logiczną strukturę” w swoim system typów, aby móc jasno zdefiniować spójność. Następnie musisz pokazać, że termin bez głowy w normalnej formie (jak ten powyżej) może mieć dowolny typ, co również nie jest oczywiste!$(\lambda x.x\ x)(\lambda x.x\ x)$

Więcej szczegółów można znaleźć w mojej odpowiedzi na powiązane pytanie: /cstheory//a/31321/3984