Структура Эрбранда

Структура словаря, определяемая исключительно синтаксическими свойствами

В логике первого порядка структура Эрбрана S — это структура над словарем σ , которая определяется исключительно синтаксическими свойствами σ . Идея состоит в том, чтобы брать строки символов терминов в качестве их значений, например, обозначение постоянного символа c — это просто « c » (символ). Она названа в честь Жака Эрбрана .

Структуры Эрбрана играют важную роль в основах логического программирования . ^[1]

Вселенная Эрбранда

Определение

Вселенная Эрбрана служит вселенной в структуре Эрбрана .

1. Вселенная Эрбрана языка первого порядка L ^σ — это множество всех основных терминов L σ ^. Если язык не имеет констант, то он расширяется путем добавления произвольной новой константы.

   • Вселенная Эрбрана счетно бесконечна, если σ счетно и существует функциональный символ арности больше 0.
   • В контексте языков первого порядка мы также говорим просто о эрбрановом универсуме словаря σ .
2. Вселенная Эрбрана замкнутой формулы в нормальной форме Скулема F — это множество всех членов без переменных, которые могут быть построены с использованием функциональных символов и констант F. Если F не имеет констант, то F расширяется путем добавления произвольной новой константы.

   • Это второе определение важно в контексте вычислительного разрешения .

Пример

Пусть L ^σ — язык первого порядка со словарным запасом

• постоянные символы: c
• функциональные символы: f (·), g (·)

тогда универсум Эрбрана L ^σ (или σ ) равен { c , f ( c ), g ( c ), f ( f ( c )), f ( g ( c )), g ( f ( c )), g ( g ( c )), ...}.

Обратите внимание, что символы отношений не имеют значения для вселенной Эрбрана.

Структура Эрбранда

Структура Эрбрана интерпретирует термины на основе вселенной Эрбрана .

Определение

Пусть S — структура со словарем σ и универсумом U. Пусть W — множество всех терминов над σ, а W ₀ — подмножество всех терминов, свободных от переменных. S называется структурой Эрбрана тогда и только тогда, когда

1. У = В ₀
2. f ^S ( t ₁ , ..., t _n ) = f ( t ₁ , ..., t _n ) для каждого n -арного функционального символа f ∈ σ и t ₁ , ..., t _n ∈ W ₀
3. c ^S = c для каждой константы c в σ

Замечания

1. U — это вселенная Эрбрана σ .
2. Структура Эрбрана, являющаяся моделью теории T , называется моделью Эрбрана теории T.

Примеры

Для постоянного символа c и унарного функционального символа f (.) мы имеем следующую интерпретацию:

• U = { c , fc , ffc , fffc , ...}
• фк → фк , фк → фк , ...
• с → с

база Herbrand

В дополнение к универсуму, определенному в § Вселенная Эрбрана, и термину обозначения, определенному в § Структура Эрбрана, база Эрбрана завершает интерпретацию, обозначая символы отношений.

Определение

База Эрбрана — это множество всех основных атомов, аргументы которых являются элементами вселенной Эрбрана.

Примеры

Для символа бинарного отношения R получаем с учетом приведенных выше терминов:

{ р ( c , c ), р ( fc , c ), р ( c , fc ), р ( fc , fc ), р ( fc , c ), ...}

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

• Теорема Эрбрана
• Еебрендизация
• интерпретация Эрбрана

Примечания

1. «Семантика Эрбрана».

Ссылки

• Эббингауз, Хайнц-Дитер ; Флум, Йорг; Томас, Вольфганг (1996). Математическая логика . Спрингер . ISBN 978-0387942582.