Еебрендизация

Доказательство теоремы Эрбрана

Herbrandization логической формулы ( названной в честь Жака Эрбрана ) — это конструкция, которая является двойственной к Skolemization формулы. Торальф Скулем рассматривал Skolemization формул в предваренной форме как часть своего доказательства теоремы Лёвенгейма–Скулема (Skolem 1920). Herbrand работал с этим двойственным понятием Herbrandization, обобщенным для применения также и к непредваренным формулам, чтобы доказать теорему Herbrand (Herbrand 1930).

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

Определение и примеры

Пусть будет формулой на языке логики первого порядка . Мы можем предположить, что не содержит переменных, связанных двумя различными вхождениями квантификатора, и что ни одна переменная не встречается одновременно связанной и свободной. (То есть может быть переименована для обеспечения этих условий таким образом, чтобы результатом была эквивалентная формула). ${\displaystyle F}$ ${\displaystyle F}$ ${\displaystyle F}$

Гербрендизация тогда получается следующим образом: ${\displaystyle F}$

• Сначала замените все свободные переменные константными символами. ${\displaystyle F}$
• Во-вторых, удалите все квантификаторы переменных, которые либо (1) имеют универсальную квантификацию и находятся в пределах четного числа знаков отрицания, либо (2) имеют экзистенциальную квантификацию и находятся в пределах нечетного числа знаков отрицания.
• Наконец, замените каждую такую ​​переменную символом функции , где — переменные, которые все еще квантифицируются и чьи квантификаторы управляют . ${\displaystyle v}$ ${\displaystyle f_{v}(x_{1},\dots ,x_{k})}$ ${\displaystyle x_{1},\dots ,x_{k}}$ ${\displaystyle v}$

Например, рассмотрим формулу . Нет свободных переменных для замены. Переменные — это тот тип, который мы рассматриваем для второго шага, поэтому мы удаляем квантификаторы и . Наконец, мы заменяем константой (поскольку не было других квантификаторов, управляющих ), и мы заменяем символом функции : ${\displaystyle F:=\forall y\exists x[R(y,x)\wedge \neg \exists zS(x,z)]}$ ${\displaystyle y,z}$ ${\displaystyle \forall y}$ ${\displaystyle \exists z}$ ${\displaystyle y}$ ${\displaystyle c_{y}}$ ${\displaystyle y}$ ${\displaystyle z}$ ${\displaystyle f_{z}(x)}$

${\displaystyle F^{H}=\exists x[R(c_{y},x)\wedge \neg S(x,f_{z}(x))].}$

Скулемизация формулы получается аналогично, за исключением того, что на втором шаге выше мы бы удалили квантификаторы по переменным, которые либо (1) квантифицированы экзистенциально и в пределах четного числа отрицаний, либо (2) квантифицированы универсально и в пределах нечетного числа отрицаний. Таким образом, рассматривая то же самое сверху , ее скулемизация будет: ${\displaystyle F}$

${\displaystyle F^{S}=\forall y[R(y,f_{x}(y))\wedge \neg \exists zS(f_{x}(y),z)].}$

Чтобы понять значение этих построений, см. теорему Эрбрана или теорему Лёвенгейма–Скулема .

Смотрите также

• Логика предикатного функтора

Ссылки

• Сколем, Т. «Логико-комбинаторные исследования выполнимости или доказуемости математических предложений: упрощенное доказательство теоремы Л. Лёвенгейма и обобщения теоремы». (В ван Хейеноорте 1967, 252-63.)
• Хербранд, Дж. «Исследования в теории доказательств: свойства истинных предложений». (В ван Хейеноорте 1967, 525-81.)
• ван Хейеноорт, Дж. От Фреге к Гёделю: Справочник по математической логике, 1879-1931 . Издательство Гарвардского университета, 1967.