Hyperdoktryny i monadyczna logika drugiego rzędu

To pytanie jest zasadniczo pytaniem, które zadałem na Mathoverflow.

Monadyczna logika drugiego rzędu (MSO) to logika drugiego rzędu z kwantyfikacją w stosunku do pojedynczych predykatów. Oznacza to kwantyfikację zbiorów. Istnieje kilka logiki MSO, które są fundamentalne dla struktur badanych w informatyce.

Pytanie 1. Czy istnieje kategoryczna semantyka dla logiki Monadic drugiego rzędu?

Pytanie 2. Traktowanie logiki kategorycznej często mówi o „logice intuicyjnej wyższego rzędu”. Czy mam rację, zakładając, że dotyczą one funkcji wyższego rzędu, a nie kwantyfikacji w oparciu o predykaty drugiego rzędu?

Pytanie 3. (Dodano, 8 listopada 2013 r., Po odpowiedzi Neela) Moje rozumienie kwantyfikacji pierwszego rzędu (w odniesieniu do prezentacji Pittsa wspomnianego poniżej) jest takie, że jest ono zdefiniowane w odniesieniu do wycofania morfizmu projekcji . W szczególności, kwantyfikacja uniwersalna jest interpretowana jako prawy przydział a kwantyfikacja egzystencjalna jest interpretowana jako lewy przecinek . Te połączenia muszą spełniać pewne warunki, które czasem widziałem jako warunki Beck-Chevalley i Frobenius-Wzajemność.$\pi^*$$\pi$$\pi^*$$\pi^*$

Teraz, jeśli chcemy skwantyfikować predykaty, zakładam, że jestem w kartezjańskiej zamkniętej kategorii, obraz jest prawie taki sam, z tym wyjątkiem, że poniżej ma inną strukturę niż wcześniej.$X$

$$\exists_{I,X}, \forall_{I,X}: P_C(I\times X) \to P_C(I)$$

Czy to prawda?

Wydaje mi się, że mój umysł był zablokowany, ponieważ wcześniej miałem do czynienia z hiperdoktrynami pierwszego rzędu i nie potrzebowałem tej kategorii, by być kartezjańską zamkniętą i nie rozważałem tego później.

Tło i kontekst. Pracowałem nad prezentacją logiki kategorycznej przez Andy'ego Pittsa w jego artykule z Handbook of Logic in Computer Science , ale znam też traktowanie teorii Triposa w jego rozprawie doktorskiej, a także notatki Awodeya i Bauera. Zacząłem studiować kategorie Crole'a dla typów i książkę Lambka i Scotta, ale minęło trochę czasu, odkąd zajrzałem do dwóch ostatnich tekstów.

Jeśli chodzi o motywację, interesuje mnie rodzaj logiki MSO pojawiającej się w poniższych twierdzeniach. Nie chcę zajmować się logiką, która jest jednoznacznie równoważna z jedną z nich. Oznacza to, że nie chcę kodować predykatów monadycznych pod względem funkcji wyższego rzędu, a następnie zajmować się inną logiką, ale z przyjemnością studiuję semantykę, która obejmuje takie kodowanie pod maską.

1. (Twierdzenie Buechi i Elgot) Gdy wszechświat struktur jest skończonymi słowami nad skończonym alfabetem, język jest regularny dokładnie, jeśli można go zdefiniować w MSO z interpretowanym predykatem do wyrażania kolejnych pozycji.
2. (Twierdzenie Buechiego) Gdy wszechświat struktur ma słowa nad skończonym alfabetem, język jest nieregularny dokładnie, jeśli można go zdefiniować w MSO z odpowiednio zinterpretowanym predykatem.$\omega$$\omega$
3. (Twierdzenie Thatcher i Wright) Zbiór drzew skończonych jest rozpoznawany przez oddolny automat skończonych drzew dokładnie wtedy, gdy można go zdefiniować w MSO z interpretowanym predykatem.
4. WS1S to słaba monadyczna teoria drugiego rzędu jednego następcy. Formuły definiują zbiory liczb naturalnych, a zmienne drugiego rzędu mogą być interpretowane tylko jako zbiory skończone. O WS1S decydują automaty skończone, kodując krotki liczb naturalnych jako skończone słowa.
5. (Twierdzenie Rabina) S2S jest teorią drugiego rzędu dwóch następców. O S2S mogą decydować automaty Rabina.

1. Nie wiem!

2. Nie, twoje założenie jest nieprawidłowe. Możesz kwantyfikować funkcje wyższego rzędu i predykaty w IHOL (w rzeczywistości predykaty są po prostu funkcjami dla pewnego rodzaju zdań). Konfiguracja wygląda trochę tak:

   $$\begin{array}{llcl} \mbox{Sort} & \omega & ::= & \omega \to \omega \;\; | \;\; \omega \times \omega \;\; | \;\; 1 \;\;|\;\; \mathrm{prop} \;\;|\;\; \iota\\ \mbox{Term} & t & ::= & x \;\;|\;\; \lambda x.t \;\;|\;\; t\;t' \;\;|\;\; (t,t) \;\; | \;\; \pi_1(t) \;\;|\;\; \pi_2(t) \;\;|\;\; () \\ & & | & p \Rightarrow q \;\;|\;\; \top \;\;|\;\; p \wedge q \;\;|\;\; \bot \;\;|\;\; p \vee q \\ & & | & \forall x:\omega.p \;\;|\;\; \exists x:\omega.p \;\;|\;\; t =_\omega t' \\ & & | & f(\vec{t}) \end{array}$$

Podajesz zwykłe reguły pisania, aby ocenić poprawność terminu. Pierwszy wiersz pojęć to zwykły rachunek lambda po prostu, drugi dwa wiersze są propozycjami logiki wyższego rzędu (wpisany jako elementy ), a trzeci wiersz to dowolne stałe używane do tworzenia jednostek (elementy ).$\mathrm{prop}$$\iota$

Następnie chodzi o to, że chcesz rozszerzyć semantykę Kripke dla logiki intuicyjnej pierwszego rzędu na logikę wyższego rzędu, poprzez rozszerzenie semantyki hiperdoktryny o dodatkową strukturę. Hiperdoktryna pierwszego rzędu to funktor między kategorią z produktami (używanymi do interpretacji terminów w kontekście), a kategorią posetów (sieci wartości prawda ), spełniając niektóre warunki, aby zastąpienie działało prawidłowo.$P : C^\mathrm{op} \to \mathrm{Poset}$$C$

Aby dostać się do IHOL, dodatkowo to potwierdzasz

1. $C$ jest kartezjańsko zamknięty (aby modelować zdolność do kwantyfikacji według typów funkcji), oraz
2. $C$ ma wewnętrzną algebrę Heytinga spełniającą właściwość, która dla każdego , . Używasz do modelowania , a izomorfizm mówi ci, że terminy typu naprawdę odpowiadają wartościom prawdy. $H$$\Gamma \in C$$\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$$H$$\mathrm{prop}$$\mathrm{prop}$

Ta struktura jest prawie „elementarnym toposem”. Jeśli dodatkowo wymagasz, aby był zbiorem podobiektów , to jesteś na miejscu. (Zasadniczo mówi to, że możesz dodać zasadę zrozumienia do swojej logiki). $P(\Gamma)$$\Gamma$