Інтерпретація Ербрана

У математичній логіці, Ербранова інтерпретація — це інтерпретація, в якій константам і функціональним символам присвоєно дуже простий зміст.[1]. Конкретніше, кожна константа інтерпретується як вона сама, функціональний символ ж інтерпретується як функція, яка застосовується. Інтерпретація також визначає предикатні символи як задають підмножину відповідної Ербрановой бази, фактично задаючи, яким чином обчислюється значення замкнутих формул. Це дозволяє інтерпретувати символи в чисто синтаксичному вигляді, незалежно від будь-якої реальної конкретизації.

Важливість інтерпретації Ербрана в тому, що якщо якась інтерпретація задовольняє заданій множині умов S, то існує Ербранова інтерпретація, яка задовольнить ім. Більш того, теорема Ербрана стверджує, що якщо S суперечливо, то існує кінцеве суперечливе безліч формул з Ербранова універсуму, заданого S. Так як це безліч звичайно, то його суперечливість може бути перевірено в кінцевий час. Проте, може бути нескінченне число таких множин для перевірки.