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. π π ∗ π ∗
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.
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ô.
- (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.
- (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.ω
- (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.
- 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.
- (Teorema de Rabin) S2S é a teoria de segunda ordem de dois sucessores. O S2S pode ser decidido pelos autômatos de Rabin.
fonte