Hyperdoktrinen und monadische Logik zweiter Ordnung

Diese Frage ist im Wesentlichen die Frage, die ich bei Mathoverflow gestellt habe.

Die MSO-Logik (Monadic Second Order) ist eine Logik zweiter Ordnung mit Quantifizierung über unäre Prädikate. Das heißt, Quantifizierung über Mengen. Es gibt mehrere MSO-Logiken, die für in der Informatik untersuchte Strukturen von grundlegender Bedeutung sind.

Frage 1. Gibt es eine kategoriale Semantik für monadische Logik zweiter Ordnung?

Frage 2. Behandlungen der kategorialen Logik sprechen oft von "intuitionistischer Logik höherer Ordnung". Kann ich zu Recht davon ausgehen, dass sie sich auf Funktionen höherer Ordnung beziehen und nicht auf die Quantifizierung über Prädikate zweiter Ordnung?

Frage 3. (Hinzugefügt am 08. November 2013 nach Neels Antwort) Mein Verständnis der Quantifizierung erster Ordnung (in Bezug auf die unten erwähnte Darstellung von Pitts) ist, dass sie in Bezug auf den Pullback eines Projektionsmorphismus definiert ist . Insbesondere wird die universelle Quantifizierung als der rechte Zusatz von und die existenzielle Quantifizierung als der linke Zusatz von interpretiert . Diese Punkte müssen einige Bedingungen erfüllen, die ich manchmal als Beck-Chevalley- und Frobenius-Reziprozitätsbedingungen bezeichnet habe.$\pi^*$$\pi$$\pi^*$$\pi^*$

Wenn wir nun über Prädikate quantifizieren wollen, gehe ich davon aus, dass ich in einer geschlossenen kartesischen Kategorie bin, ist das Bild fast das gleiche, außer dass unten eine andere Struktur als zuvor hat.$X$

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

Ist das richtig?

Ich glaube, meine mentale Blockade war, weil ich mich zuvor mit Hyperdoktrinen erster Ordnung befasst hatte und die Kategorie nicht kartesisch geschlossen haben musste und sie später nicht berücksichtigte.

Hintergrund und Kontext. Ich habe mit der Präsentation der kategorialen Logik von Andy Pitts in seinem Artikel Handbook of Logic in Computer Science gearbeitet , aber ich bin auch mit der Behandlung der Tripos-Theorie in seiner Doktorarbeit sowie den Notizen von Awodey und Bauer vertraut. Ich habe angefangen, Croles Kategorien für Typen und das Buch von Lambek und Scott zu studieren, aber es ist schon eine Weile her, seit ich die letzten beiden Texte konsultiert habe.

Aus Gründen der Motivation interessiere ich mich für die Art der MSO-Logik, die in den folgenden Theoremen aufgeführt ist. Ich möchte mich nicht mit einer Logik befassen, die einer dieser Logik ausdrücklich entspricht. Das heißt, ich möchte keine monadischen Prädikate in Form von Funktionen höherer Ordnung codieren und mich dann mit einer anderen Logik befassen, aber ich bin glücklich, eine Semantik zu studieren, die eine solche Codierung unter der Haube beinhaltet.

1. (Satz von Buechi und Elgot) Wenn das Universum der Strukturen endliche Wörter über einem endlichen Alphabet sind, ist eine Sprache genau dann regulär, wenn sie in MSO mit einem interpretierten Prädikat zum Ausdrücken aufeinanderfolgender Positionen definierbar ist.
2. (Satz von Buechi) Wenn das Universum der Strukturen Wörter über einem endlichen Alphabet ist, ist eine Sprache regelmäßig, genau wenn sie in MSO mit einem entsprechend interpretierten Prädikat definierbar ist.$\omega$$\omega$
3. (Thatcher- und Wright-Theorem) Eine Menge endlicher Bäume ist an einem Bottom-up-Automaten für endliche Bäume genau dann erkennbar, wenn sie in MSO mit einem interpretierten Prädikat definierbar ist.
4. WS1S ist die schwache monadische Theorie zweiter Ordnung eines Nachfolgers. Formeln definieren Mengen natürlicher Zahlen und Variablen zweiter Ordnung können nur als endliche Mengen interpretiert werden. WS1S kann durch endliche Automaten entschieden werden, indem Tupel natürlicher Zahlen als endliche Wörter codiert werden.
5. (Rabins Satz) S2S ist die Theorie zweiter Ordnung zweier Nachfolger. S2S kann von Rabin-Automaten entschieden werden.

1. Ich weiß es nicht!

2. Nein, Ihre Annahme ist nicht richtig. Sie können Funktionen und Prädikate höherer Ordnung in IHOL quantifizieren (Prädikate sind in der Tat nur Funktionen in einer Art von Aussagen). Das Setup sieht ungefähr so ​​aus:

   $$\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}$$

Sie geben die üblichen Schreibregeln an, um die Form eines Begriffs zu beurteilen. Die erste Zeile der Begriffe ist der übliche einfach typisierte Lambda-Kalkül, die zweiten beiden Zeilen sind die Sätze der Logik höherer Ordnung (typisiert als Elemente von ), und die dritte Zeile sind alle Konstanten, die Sie zur Bildung von Individuen verwenden (Elemente von ).$\mathrm{prop}$$\iota$

Die Idee ist dann, dass Sie die Kripke-Semantik für intuitionistische Logik erster Ordnung auf Logik höherer Ordnung erweitern möchten, indem Sie die hyperdoktrine Semantik um zusätzliche Struktur erweitern. Eine Hyperdoktrin erster Ordnung ist ein Funktor zwischen einer Kategorie mit Produkten (zur Interpretation der Begriffe im Kontext) und einer Kategorie von Posets (den Wahrheitswertgittern) ), die einige Bedingungen erfüllen, damit die Substitution richtig funktioniert.$P : C^\mathrm{op} \to \mathrm{Poset}$$C$

Um zu IHOL zu gelangen, behaupten Sie dies zusätzlich

1. $C$ ist kartesisch geschlossen (um die Fähigkeit zur Quantifizierung über Funktionstypen zu modellieren) und
2. $C$ hat eine interne Heyting Algebra die Eigenschaft , dass für jeden erfüllen , . Sie verwenden , um zu modellieren , und der Isomorphismus sagt Ihnen, dass Begriffe vom Typ tatsächlich Wahrheitswerten entsprechen. $H$$\Gamma \in C$$\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$$H$$\mathrm{prop}$$\mathrm{prop}$

Diese Struktur ist fast ein "elementarer Topos". Wenn Sie zusätzlich benötigen, dass eine Menge von Unterobjekten von , dann sind Sie da. (Dies bedeutet im Wesentlichen, dass Sie Ihrer Logik ein Verständnisprinzip hinzufügen können.) $P(\Gamma)$$\Gamma$