Гербирование

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

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

Определение и примеры [ править ]

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

Herbrandization из затем получают следующим образом :${\ 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 \ существует x [R (y, x) \ клин \ neg \ exists zS (x, z)]}$${\ displaystyle y, z}$${\ displaystyle \ forall y}$${\ Displaystyle \ существует z}$${\ displaystyle y}$${\ displaystyle c_ {y}}$${\ displaystyle y}$${\ displaystyle z}$${\ displaystyle f_ {z} (x)}$

${\ Displaystyle F ^ {H} = \ существует 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)].}$

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

См. Также [ править ]

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

Ссылки [ править ]

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