Нахождение конечной модели

Я знаю, что вопрос «имеет ли формула первого порядка модель» вообще неразрешим.$\phi$

Может ли кто-нибудь дать мне ссылку или книгу, которая даст ответ для конечных моделей. Если у меня есть формула первого порядка , можно ли имеет ли конечную модель? Я почти уверен, что вопрос хорошо известен, но я даже не знаю, с чего начать поиск ответа. (Например, я ожидал, что это будет в «Элементах теории конечных моделей» Либкина, но, похоже, я не могу его найти.)$\phi$$\phi$

Вторая часть моего вопроса: есть ли известные ограничения, так что проблема разрешима?

Например, проблема может стать разрешимой для формулы первого порядка только с монадическими предикатами. Или когда у нас есть монадический предикат плюс отношение-преемник. Но я не могу представить алгоритм, чтобы решить, существует ли (конечная) модель над этими ограничениями.

На первую часть вашего вопроса отвечает теорема Трахтенброта . Вторая часть действительно довольно большой вопрос. В зависимости от реляционной структуры, над которой вы работаете, может быть дано несколько решений. Например, если вы заинтересованы в формальных языках, MSO над структурами слов соответствует обычным языкам, а логика сопоставления ( см. Это ) соответствует CFL, и, следовательно, проблема их выполнимости разрешима.

Вы должны взглянуть на главу 14 Libkin, где доказано, что хорошие сегменты FO имеют разрешимую проблему выполнимости в соответствии с количеством разрешенных чередований кванторов.

Я не знаю ответа для произвольных фрагментов FO. Классическая модальная логика и ее расширения имеют несколько свойств разрешимости. При стандартных переводах вы получаете фрагменты классической логики, которые разделяют эти свойства.

1. Модальная логика и бизимуляционный инвариантный фрагмент FOL с двумя переменными.
2. CTL * и фрагмент инварианта бисимуляции в монадической логике пути.
3. Му-исчисление и фрагмент инварианта бисимуляции в монадической логике второго порядка.

Все модальные логики выше разрешимы и имеют свойство конечной модели. Другие логики с устойчивыми свойствами разрешимости - это защищенный фрагмент FO, слабо защищенный фрагмент и защищенная логика с фиксированной точкой. Эти логики были разработаны для того, чтобы перенести суть качественных свойств модальных логик в классическую логическую систему. Защищенная логика с фиксированной точкой разрешима, но не обладает свойством конечной модели.

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

Во-первых, ваш вопрос, по-видимому, представляет интерес для сообщества Automated Deduction. У Уильяма Маккуна есть программа под названием Mace4, которая ищет конечные модели. Возможно, вы захотите прочитать документацию, которая описывает, как это делается.

Что касается конкретных разрешаемых ограничений, вы можете посмотреть на следующее:

1. Случаи, когда Вселенная Гербранда конечна. Одним из механических способов проверки подмножества этих случаев является проверка наличия в формуле функциональных символов. Если это не так, Вселенная Гербранда конечна.

2. Случаи, когда исключение квантификатора возможно: теория.stanford.edu/~tingz/talks/qe.ps

В дополнение к ответам, которые уже были даны: очень хорошая ссылка о (не) разрешимости фрагментов логики первого порядка - это книга «Классическая задача решения » Боргера, Гределя и Гуревича.