Względna spójność PA i niektórych teorii typów

Dla teorii typów przez spójność rozumiem, że ma typ, który nie jest zamieszkany. Z silnej normalizacji sześcianu lambda wynika, że ​​układ $F$ i układ $F_\omega$ są spójne. Typy indukcyjne MLTT + mają również dowód normalizacji. Jednak wszystkie powinny być wystarczająco mocne, aby zbudować model PA, co dowodzi, że PA jest spójny z tymi teoriami. System $F$ jest dość potężny , więc spodziewam się, że będzie w stanie udowodnić spójność PA poprzez zbudowanie modelu z wykorzystaniem cyfr Kościoła. MLTT + IT ma typ indukcyjny liczb naturalnych i powinien również wykazywać spójność.

To wszystko sugeruje, że dowodów normalizacyjnych dla tych teorii nie można internalizować w PA. Więc:

1. Czy system $F$ , system $F_\omega$ i MLTT + IT faktycznie mogą udowodnić spójność PA?
2. Jeśli mogą, to jaka metateoria jest potrzebna do udowodnienia normalizacji dla systemu $F$ , $F_\omega$ i MLTT + IT?
3. Czy istnieje dobre odniesienie do teorii teorii dowodu w ogóle, czy w szczególności do niektórych z tych teorii?

Krótka odpowiedź na twoje pytanie 1 brzmi „ nie” , ale może z subtelnych powodów.

Przede wszystkim system i F ω nie może wyrazić pierwszego rzędu teorię arytmetyka , a nawet mniej konsystencja P A .$F$$F_\omega$ $\mathrm{PA}$

Po drugie, i to jest naprawdę zaskakujące, może faktycznie udowodnić spójność obu tych systemów! Odbywa się to za pomocą tak zwanego modelu nieistotnego dowodu , który interpretuje typy jako zestawy ∈ { ∅ , { ∙ } } , gdzie ∙ jest jakimś elementem pozornym reprezentującym mieszkańca niepustego typu. Następnie można zapisać proste zasady funkcjonowania → i ∀ na tego typu dość łatwo dostać model systemu F , w którym typ ∀ X . X jest interpretowany przez $\mathrm{PA}$$\in\{\varnothing,\{\bullet\}\}$$\bullet$$\rightarrow$$\forall$$F$$\forall X.X$$\varnothing$. Podobnie można zrobić dla , stosując nieco większą ostrożność, aby interpretować wyższe rodzaje jako przestrzenie funkcji skończonych.$F_\omega$

Istnieje tutaj pozorny paradoks, w którym może udowodnić spójność tych z pozoru potężnych systemów, ale nie (jak pokażę za chwilę) normalizacji.$\mathrm{PA}$

$p$$\phi$$p\Vdash \phi$$\phi$$p$$p\not\Vdash\bot$

Twierdzenie: Jeśli jest twierdzeniem arytmetyki drugiego rzędu , to istnieje pewien zamknięty termin systemu taki, że$\phi$$\mathrm{PA}_2$$t$$F$

$$t\Vdash\phi$$

To twierdzenie można udowodnić w , a więc mamy i stosuje Argument Gödla (i nie może udowodnić normalizacji systemu ). Jest to przydatne, aby pamiętać, że odwrotna implikacja, tak więc mamy dokładną charakterystykę mocy dowód teoretycznie potrzebnej do udowodnienia normalizację systemu .$\mathrm{PA}$

$$\mathrm{PA}\vdash F\mbox{ is normalizing}\Rightarrow\mbox{$\mathrm{PA}_2$ is consistent}$$ $\mathrm{PA}$$F$$F$

Podobna historia dotyczy systemu , który moim zdaniem odpowiada wyższej arytmetyki .$F_\omega$$\mathrm{PA}_\omega$

---

Wreszcie mamy trudny przypadek MLTT z typami indukcyjnymi. Tutaj ponownie pojawia się nieco subtelna kwestia. Z pewnością tutaj możemy wyrazić spójność , więc to nie jest problem i nie ma modelu nieistotnego dla dowodów, ponieważ możemy udowodnić, że typ ma co najmniej 2 elementy ( nieskończona ilość różnych elementów).$\mathrm{PA}$$\mathrm{Nat}$

Jednak natrafiamy na zaskakujący fakt teorii intuicyjnych wyższego rzędu: , wersja Heyting Arithmetic wyższego rzędu jest konserwatywna w stosunku do ! W szczególności nie możemy udowodnić zgodności (co jest równoważne z ). Intuicyjnie wynika to z faktu, że intuicyjne przestrzenie funkcji nie pozwalają na kwantyfikację w oparciu o dowolny podzbiór , ponieważ wszystkie definiowalne funkcje muszą być obliczalne.$\mathrm{HA}_\omega$$\mathrm{HA}$$\mathrm{PA}$$\mathrm{HA}$N → $\mathbb{N}$$\mathbb{N}\rightarrow \mathbb{N}$

W szczególności nie sądzę, abyś mógł udowodnić spójność jeśli dodasz tylko liczby naturalne do MLTT bez wszechświatów. Wierzę, że dodanie wszechświatów lub „silniejszych” typów indukcyjnych (takich jak porządkowe) da ci wystarczającą moc, ale obawiam się, że nie mam na to odniesienia. W przypadku wszechświatów argument wydaje się dość prosty, ponieważ masz dość teorii mnogości, aby zbudować model .H $\mathrm{PA}$$\mathrm{HA}$

---

Wreszcie, odniesienia do teorii dowodów systemów typu: myślę, że tutaj naprawdę jest luka w literaturze i chciałbym czysto potraktować wszystkie te tematy (w rzeczywistości marzę o tym, aby napisać ją kiedyś!). W międzyczasie:

• Model nieistotny dla dowodu jest wyjaśniony tutaj przez Miquela i Wernera, choć robią to dla rachunku konstrukcji, co nieco komplikuje sprawy.

• Argument wykonalności został nakreślony w klasycznych dowodach i typach Girarda, Taylora i Lafonta. Myślę, że naszkicowali również model nieistotny dla dowodów oraz wiele innych przydatnych rzeczy. To prawdopodobnie pierwsze odniesienie do przeczytania.

• Argument konserwatywności arytmetyki Heytinga wyższego rzędu można znaleźć w nieuchwytnym drugim tomie Konstruktywizm w matematyce autorstwa Troelstra i van Dalen (patrz tutaj ). Oba tomy są niezwykle pouczające, ale dość trudne do odczytania dla nowicjusza, IMHO. W pewien sposób unika się również „współczesnych” tematów teorii typu, co nie jest zaskakujące, biorąc pod uwagę wiek książek.

---

Dodatkowe pytanie w komentarzach dotyczyło dokładnej wytrzymałości konsystencji / wytrzymałości normalizacyjnej MLTT + Induktywne. Nie mam tutaj dokładnej odpowiedzi, ale z pewnością odpowiedź zależy od liczby wszechświatów i dozwolonej natury rodzin indukcyjnych. Rathjen bada to pytanie we wspaniałym artykule Siła niektórych teorii Martina-Lofa .

Normalizacja Wrt, podstawową ideą jest to, że jeśli dla 2 teorii i mamy U P A ⊢ C o n ( T ) ⇒ C o n ( U$\cal{T}$$\cal{U}$

$$\mathrm{PA}\vdash\mathrm{Con}(\cal{T})\Rightarrow\mathrm{Con}(\cal{U})$$

wtedy ogólnie

$$\mathrm{PA}\vdash \mbox{1-$\mathrm{Con}$}(\cal{T})\Rightarrow\mathrm{Norm}(\cal{U})$$

gdzie 1- to spójność 1, a to (słaba) normalizacja.N o r $\mathrm{Con}$$\mathrm{Norm}$

MLTT + rodzaj liczb naturalnych (i rekurencja) jest konserwatywnym rozszerzeniem , co zostało udowodnione w Besson Recursive Models for Constructive Set Theories .$\mathrm{HA}_\omega$

Jeśli chodzi o MLTT z indukcją-rekurencją lub indukcją-indukcją, nie wiem, jaka jest sytuacja, a AFAIK problem dokładnej konsystencji jest nadal otwarty.