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

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

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

Вселенная

Определение

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

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. ж ^С ( t ₁ , ..., t _n ) знак равно f ( t ₁ , ..., t _n ) для каждого n -арного функционального символа f ∈ σ и t ₁ , ..., t _n ∈ W ₀
3. с ^С = c для каждой константы c в σ

Замечания

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

Примеры

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

• U знак равно { c , FC , ffc , ffc , ...}
• ФК → ФК , ФК → ФК , ...
• с → с

База

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

Определение

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

Примеры

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

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

См. также

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

Ссылки

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