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

Herbrandization

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

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

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

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

В Гербирование из тогда получается следующим образом:

  • Сначала замените все свободные переменные в постоянными символами.
  • Во-вторых, удалите все кванторы для переменных, которые либо (1) количественно определены универсально и в пределах четного числа знаков отрицания, либо (2) определены количественно экзистенциально и в пределах нечетного числа знаков отрицания.
  • Наконец, замените каждую такую ​​переменную с символом функции , где являются переменными, которые все еще оцениваются количественно, и чьи кванторы определяют .

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

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

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

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

использованная литература

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