Введение

В математической логике теорема интерполяции Крейга — это результат, устанавливающий связь между различными логическими теориями. Если говорить упрощенно, теорема утверждает, что если формула φ влечет формулу ψ и у них есть хотя бы один общий атомарный символ переменной, то существует формула ρ, называемая интерполянтом, такая, что каждый нелогический символ в ρ встречается как в φ, так и в ψ, φ влечет ρ, а ρ влечет ψ. Теорема была впервые доказана Уильямом Крейгом в 1957 году для логики первого порядка. Варианты теоремы справедливы и для других логик, таких как пропозициональная логика. Более сильная форма теоремы интерполяции Крейга для логики первого порядка была доказана Роджером Линдоном в 1959 году; общий результат иногда называют теоремой Крейга — Линдона.

Теорема интерполяции Линдона

Предположим, что S и T – две теории первого порядка. Для обозначения пусть S ∪ T обозначает наименьшую теорию, включающую как S, так и T; сигнатура S ∪ T – наименьшая сигнатура, содержащая сигнатуры S и T. Также пусть S ∩ T обозначает пересечение языков этих двух теорий; сигнатура S ∩ T – пересечение сигнатур этих двух языков. Теорема Линдона утверждает, что если S ∪ T невыполнима, то существует интерполирующая формула ρ в языке S ∩ T, которая истинна во всех моделях S и ложна во всех моделях T. Более того, ρ обладает более сильным свойством: для каждого символа отношения, который встречается с положительным знаком в ρ, существует формула в S, в которой он также встречается с положительным знаком, и формула в T, в которой он встречается с отрицательным знаком. И для каждого символа отношения, который встречается с отрицательным знаком в ρ, существует формула в S, в которой он встречается с отрицательным знаком, и формула в T, в которой он встречается с положительным знаком.

Приложения

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