Czy możemy udowodnić słabą normalizację dla Systemu F poprzez indukcję na transfinite porządkowej

Słabą normalizację dla prostego rachunku lambda o typie można udowodnić (Turinga) przez indukcję na . Rozszerzony rachunek lambda z rekursorami na liczbach naturalnych (Gentzen) ma słabą strategię normalizacji przez indukcję na ϵ 0 .$\omega^2$$\epsilon_0$

Co z systemem F (lub słabszym)? Czy w tym stylu jest słaby dowód normalizacji? Jeśli nie, czy w ogóle można to zrobić?

Najbardziej wszechstronnym badaniem związku między konstruktywną teorią dowodu (ściśle związaną z teorią porządków konstruktywnych) a arytmetyką impredykatywną drugiego rzędu (która, jak wskazuje Ulrik, jest równoważna sile z Systemem F), jest Girard (1989). Tam opiera się na swojej teorii rozszerzaczy (1981), której tak naprawdę nie przestrzegam, ale myślę, że zasadniczo zapewnia niekonstruktywną teorię skolemizacji wyższego rzędu.

Rozumiem, że nie można konstruktywnie wyrazić formuł w sensie biskupa - Martina-Löfa, ponieważ są one impredykatywne w sposób, którego nie można wyeliminować przez dodanie jakiegokolwiek schematu indukcji pierwszego rzędu.$\Sigma^1_2$

Pamiętam, jak zasugerowałem teoretykowi porządkowemu, że można po prostu zastrzec , że można oprzeć impredykatywny konstruktywizm na teorii typów opartej na rachunku polimorficznym lambda i zastosować technikę kandydata do redukcji z dowodu SN Girarda dla Systemu F, aby narzucić rozsądny całkowity porządek na wszechświat konstrukcji, nazywając otrzymane z tego klasy równoważności porządkami; powiedział coś inteligentnego, co zabrałem, mówiąc, że możesz sprawić, że zadziała, ale miałoby to wszystkie zalety kradzieży nad uczciwym trudem. Aby to zadziałało, nie wystarczy, że możesz udowodnić w teorii teorii istnienie takich porządków, potrzebujesz konstruktywnego dowodu trychotomii dla porządku.

Reasumując, przy zwykłym pojęciu intuicyjnej konstrukcji Biskupa - Martina-Löfa, znana mi literatura zdecydowanie sugeruje, że nie. Jeśli jesteś przeciwny uczciwemu trudowi i przyjmiesz impredykatywny konstruktywizm, zgaduję, że prawdopodobnie da się to zrobić. Potrzebowałbyś oczywiście silniejszej teorii, że System F do konstruktywnego udowodnienia wymaganej trikotomii, ale Rachunek Konstrukcji Indukcyjnych zapewnia oczywistego kandydata.

Bibliografia

1. Girard Jean-Yves (1981), -logic. I. Dylatatory, annały logiki matematycznej 21 (2): 75–219.$\Pi^1_2$
2. Girard (1989) Proof Theory and Logical Complexity, vol. I , Napoli: Bibliopolis. Nie ma tomu II.

$\Pi^0_2$$\omega^2$

$\varepsilon_0$$\Gamma_0$

Mam nadzieję, że pewnego dnia ktoś wymyśli zwykłą notację dla arytmetyki drugiego rzędu, którą wszyscy zgodzą się, jest naturalna, a następnie może być wykorzystana w uczciwy sposób, aby udowodnić słabą normalizację dla Systemu F.

$\mathbb{N} \to \mathbb{N}$

Co więcej, myślę, że arytmetyka drugiego rzędu jest dość silna i że nie jest jeszcze znana żadna konstruktywna górna granica ze względu na jej „dowód teoretyczny porządkowy” ( Sztuka analizy porządkowej, część 3 ).

Myślę, że ta konstruktywna granica porządkowa jest potrzebna do wykonania indukcji, o którą prosisz.