Hiperdoctrinas y lógica monádica de segundo orden

Esta pregunta es esencialmente la pregunta que hice en Mathoverflow.

La lógica monádica de segundo orden (MSO) es lógica de segundo orden con cuantificación sobre predicados unarios. Es decir, cuantificación sobre conjuntos. Hay varias lógicas de MSO que son fundamentales para las estructuras estudiadas en informática.

Pregunta 1. ¿Existe una semántica categórica para las lógicas monádicas de segundo orden?

Pregunta 2. Los tratamientos de lógica categórica a menudo hablan de "lógica intuicionista de orden superior". ¿Estoy en lo cierto al suponer que se refieren a funciones de orden superior, en lugar de cuantificar sobre predicados de segundo orden?

Pregunta 3. (Agregado, 8 de noviembre de 2013, después de la respuesta de Neel) Mi comprensión de la cuantificación de primer orden (en términos de la presentación de Pitts mencionada a continuación) es que se define con respecto al retroceso de un morfismo de proyección π . Específicamente, la cuantificación universal se interpreta como el adjunto derecho de π * y cuantificación existencial se interpreta como el adjunto izquierdo de π * . Estos adjuntos tienen que satisfacer algunas condiciones, que a veces he visto referidas como condiciones de Beck-Chevalley y Frobenius-Reciprocity.$\pi^*$$\pi$$\pi^*$$\pi^*$

Ahora, si queremos cuantificar sobre predicados, supongo que estoy en una categoría cerrada cartesiana, la imagen es casi la misma, excepto que continuación tiene una estructura diferente a la anterior.$X$

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

¿Está bien?

Creo que mi bloqueo mental se debió a que anteriormente estaba lidiando con hiperdoctrinas de primer orden y no necesitaba que la categoría fuera cerrada cartesiana y no la consideré más tarde.

Antecedentes y contexto. He estado trabajando con la presentación de la lógica categórica por Andy Pitts en su artículo Manual de lógica en informática , pero también estoy familiarizado con el tratamiento de la teoría de Tripos en su tesis doctoral, así como las notas de Awodey y Bauer. Comencé a estudiar las Categorías de tipos de Crole y el libro de Lambek y Scott, pero ha pasado un tiempo desde que consulté los últimos dos textos.

Para motivarme, estoy interesado en el tipo de lógica de MSO que aparece en los teoremas a continuación. No quiero tratar con una lógica que sea expresamente equivalente a una de estas. Es decir, no quiero codificar predicados monádicos en términos de funciones de orden superior y luego tratar con otra lógica, pero me complace estudiar una semántica que incluye dicha codificación bajo el capó.

1. (Teorema de Buechi y Elgot) Cuando el universo de estructuras es palabras finitas sobre un alfabeto finito, un lenguaje es regular exactamente si es definible en MSO con un predicado interpretado para expresar posiciones consecutivas.
2. (Teorema de Buechi) Cuando el universo de estructuras es -palabras sobre un alfabeto finito, un lenguaje es ω -regular exactamente si es definible en MSO con un predicado interpretado apropiado.$\omega$$\omega$
3. (Teorema de Thatcher y Wright) Un conjunto de árboles finitos es reconocible por un autómata de árbol finito de abajo hacia arriba exactamente si es definible en MSO con un predicado interpretado.
4. WS1S es la teoría de segundo orden débil monádico de un sucesor. Las fórmulas definen conjuntos de números naturales y las variables de segundo orden solo pueden interpretarse como conjuntos finitos. WS1S puede decidirse por autómatas finitos codificando tuplas de números naturales como palabras finitas.
5. (Teorema de Rabin) S2S es la teoría de segundo orden de dos sucesores. S2S puede ser decidido por los autómatas de Rabin.

1. ¡No lo sé!

2. No, su suposición no es correcta. Puede cuantificar sobre funciones y predicados de orden superior en IHOL (de hecho, los predicados son solo funciones en un tipo de proposiciones). La configuración se parece un poco a esto:

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

$\mathrm{prop}$$\iota$

$P : C^\mathrm{op} \to \mathrm{Poset}$$C$

Para llegar a IHOL, usted también afirma que

1. $C$
2. $C$$H$$\Gamma \in C$$\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$$H$$\mathrm{prop}$$\mathrm{prop}$

$P(\Gamma)$$\Gamma$