Hiperdoctrinas e lógica monádica de segunda ordem

Esta questão é essencialmente a pergunta que fiz no Mathoverflow.

A lógica monádica de segunda ordem (MSO) é uma lógica de segunda ordem com quantificação sobre predicados unários. Ou seja, quantificação sobre conjuntos. Existem várias lógicas MSO que são fundamentais para estruturas estudadas em ciência da computação.

Pergunta 1. Existe uma semântica categórica para a lógica monádica de segunda ordem?

Questão 2. Os tratamentos da lógica categórica costumam falar sobre "lógica intuicionista de ordem superior". Estou certo em assumir que eles estão se referindo a funções de ordem superior, em vez de quantificação sobre predicados de segunda ordem?

Pergunta 3. (Adicionado em 08/11/2013, após a resposta de Neel) Meu entendimento da quantificação de primeira ordem (em termos da apresentação de Pitts mencionada abaixo) é que ela é definida com relação à retração de um morfismo de projeção . Especificamente, a quantificação universal é interpretada como o adjunto certo de e a quantificação existencial é interpretada como o adjunto esquerdo de . Esses adjuntos precisam satisfazer algumas condições, que às vezes já vi referidas como condições de Beck-Chevalley e Frobenius-Reciprocity. π π ∗ π $\pi^*$$\pi$$\pi^*$$\pi^*$

Agora, se queremos quantificar sobre predicados, presumo que estou em uma categoria fechada cartesiana, a imagem é quase a mesma, exceto que abaixo tem uma estrutura diferente de antes.$X$

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

Isso está certo?

Acredito que meu bloqueio mental foi porque eu estava lidando com hiperdoctrinas de primeira ordem e não precisava que a categoria fosse fechada cartesiana e não a considerou mais tarde.

Antecedentes e Contexto. Eu tenho trabalhado com a apresentação da lógica categórica por Andy Pitts em seu artigo Handbook of Logic in Computer Science , mas também estou familiarizado com o tratamento da teoria de Tripos em sua tese de doutorado, bem como nas notas de Awodey e Bauer. Comecei a estudar Categorias de tipos de Crole e o livro de Lambek e Scott, mas já faz um tempo desde que consultei os dois últimos textos.

Por motivação, estou interessado no tipo de lógica do MSO que aparece nos teoremas abaixo. Não quero lidar com uma lógica que seja expressivamente equivalente a uma delas. Ou seja, não quero codificar predicados monádicos em termos de funções de ordem superior e depois lidar com outra lógica, mas estou feliz em estudar uma semântica que inclua essa codificação sob o capô.

1. (Teorema de Buechi e Elgot) Quando o universo de estruturas é composto por palavras finitas sobre um alfabeto finito, uma linguagem é regular exatamente se for definível no MSO com um predicado interpretado para expressar posições consecutivas.
2. (Teorema de Buechi) Quando o universo de estruturas é -words sobre um alfabeto finito, uma linguagem é -regular exatamente se for definível no MSO com um predicado interpretado apropriado.$\omega$$\omega$
3. (Teorema de Thatcher e Wright) Um conjunto de árvores finitas é reconhecível por um autômato de árvore finita de baixo para cima exatamente se é definível no MSO com um predicado interpretado.
4. WS1S é a teoria Monádica Fraca de Segunda Ordem de Um Sucessor. As fórmulas definem conjuntos de números naturais e variáveis ​​de segunda ordem só podem ser interpretadas como conjuntos finitos. O WS1S pode ser decidido por autômatos finitos, codificando tuplas de números naturais como palavras finitas.
5. (Teorema de Rabin) S2S é a teoria de segunda ordem de dois sucessores. O S2S pode ser decidido pelos autômatos de Rabin.

1. Eu não sei!

2. Não, sua suposição não está certa. Você pode quantificar funções e predicados de ordem superior no IHOL (de fato, predicados são apenas funções em um tipo de proposições). A configuração é parecida com esta:

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

Você fornece as regras de digitação usuais para julgar a boa formação de um termo. A primeira linha de termos é o cálculo lambda usual de tipo simples, as segunda duas linhas são as proposições da lógica de ordem superior (digitadas como elementos de ) e a terceira linha são as constantes que você usa para formar indivíduos (elementos de ).$\mathrm{prop}$$\iota$

Então, a idéia é que você deseja estender a semântica de Kripke para a lógica intuicionista de primeira ordem para a lógica de ordem superior, estendendo a semântica da hiperdótrina com estrutura adicional. Uma primeira ordem é um functor entre uma categoria com produtos (usados ​​para interpretar os termos no contexto) e uma categoria de posets (as redes de valor verdade ), satisfazendo algumas condições para fazer a substituição funcionar corretamente.$P : C^\mathrm{op} \to \mathrm{Poset}$$C$

Para chegar ao IHOL, você também afirma que

1. $C$ é fechado cartesiano (para modelar a capacidade de quantificar tipos de função) e
2. $C$ tem uma álgebra interna Heyting satisfazendo a propriedade que para cada , . Você usa para modelar , e o isomorfismo diz que os termos do tipo realmente correspondem aos valores de verdade. $H$$\Gamma \in C$$\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$$H$$\mathrm{prop}$$\mathrm{prop}$

Essa estrutura é quase um "topos elementar". Se você adicionalmente exigir que seja um poset de subojetos de , você estará lá. (Isso basicamente diz que você pode adicionar um princípio de compreensão à sua lógica.) $P(\Gamma)$$\Gamma$