Гипердоктрины и монадическая логика второго порядка

Этот вопрос по сути является вопросом, который я задал на Mathoverflow.

Логика Монадического Второго Порядка (MSO) - это логика второго порядка с количественным определением по унарным предикатам. То есть количественное определение по множествам. Есть несколько логик MSO, которые являются фундаментальными для структур, изучаемых в информатике.

Вопрос 1. Существует ли категориальная семантика для монадической логики второго порядка?

Вопрос 2. Обращения к категориальной логике часто говорят о «интуиционистской логике высшего порядка». Правильно ли я предположить, что они имеют в виду функции более высокого порядка, а не количественную оценку по предикатам второго порядка?

Вопрос 3. (Добавлено 8 ноября 2013 г., после ответа Нила). Насколько я понимаю, количественная оценка первого порядка (с точки зрения представления Питта, упомянутого ниже) состоит в том, что она определяется в отношении отката.$\pi^*$ морфизма проекции $\pi$, В частности, универсальное количественное определение интерпретируется как правый сопряженный$\pi^*$ и экзистенциальная квантификация интерпретируется как левый сопряженный $\pi^*$, Эти примыкания должны удовлетворять некоторым условиям, которые я иногда видел, называемые условиями Бека-Шевалле и Фробениуса-Взаимности.

Теперь, если мы хотим дать количественную оценку предикатам, я предполагаю, что я нахожусь в декартовой закрытой категории, картина почти такая же, за исключением того, что $X$ ниже имеет другую структуру, чем раньше.

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

Это правильно?

Я полагаю, что моя психическая блокада была связана с тем, что я ранее имел дело с гипердоктринами первого порядка и не нуждался в закрытой декартовой категории и не рассматривал ее позже.

Фон и контекст. Я работал с презентацией категориальной логики Энди Питтсом в его статье « Справочник по логике в области компьютерных наук» , но я также знаком с трактовкой теории Трипоса в своей докторской диссертации, а также с примечаниями Аводея и Бауэра. Я начал изучать « Категории для типов» Крола и книгу Ламбека и Скотта, но прошло уже много времени с тех пор, как я ознакомился с последними двумя текстами.

Для мотивации меня интересует вид логики MSO, представленный в приведенных ниже теоремах. Я не хочу иметь дело с логикой, которая явно эквивалентна одной из них. То есть я не хочу кодировать монадические предикаты в терминах функций более высокого порядка, а затем иметь дело с другой логикой, но я рад изучить семантику, которая включает в себя такое кодирование.

1. (Теорема Буэчи и Элго) Когда универсум структур представляет собой конечные слова над конечным алфавитом, язык является регулярным в точности, если его можно определить в MSO с интерпретируемым предикатом для выражения последовательных позиций.
2. (Теорема Буэчи) Когда вселенная структур $\omega$слова над конечным алфавитом, язык $\omega$-регулярный точно, если это определимо в MSO с соответствующим интерпретируемым предикатом.
3. (Теорема Тэтчер и Райта) Множество конечных деревьев распознается автоматом конечного дерева снизу вверх точно, если оно определимо в MSO с интерпретированным предикатом.
4. WS1S - слабая монадическая теория второго порядка одного преемника. Формулы определяют наборы натуральных чисел, а переменные второго порядка могут интерпретироваться только как конечные наборы. WS1S может быть определено конечными автоматами путем кодирования кортежей натуральных чисел как конечных слов.
5. (Теорема Рабина) S2S - это теория второго порядка двух наследников. S2S может быть выбран автоматом Рабина.

1. Я не знаю!

2. Нет, ваше предположение неверно. Вы можете количественно определить функции и предикаты высшего порядка в IHOL (на самом деле предикаты - это просто функции в виде предложений). Настройка выглядит примерно так:

   $$\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$ с продуктами (используемыми для интерпретации терминов в контексте) и категорией множеств (решеток истинного значения), удовлетворяющих некоторым условиям для правильной работы замены.

Чтобы попасть в IHOL, вы дополнительно утверждаете, что

1. $C$ является декартово замкнутым (для моделирования способности количественно определять типы функций), и
2. $C$ имеет внутреннюю алгебру Хейтинга $H$ удовлетворяя свойство, которое для каждого $\Gamma \in C$, $\mathit{Obj}(P(\Gamma)) \simeq C(\Gamma, H)$, Ты используешь$H$ моделировать $\mathrm{prop}$и изоморфизм говорит вам, что условия типа $\mathrm{prop}$ действительно соответствуют ценностям правды.

Эта структура почти «элементарный топос». Если вам дополнительно требуется, чтобы$P(\Gamma)$ представляет собой набор предметов $\Gamma$тогда ты там. (По сути, это говорит о том, что вы можете добавить принцип понимания к своей логике.)