(1): Эх1 ... Эxn, ..., Vy1 ... Vyi ... Эz1 ... Vu1 ... Эv1 ... b(бета)(x1 ..., y1 ..., v1 ...). b' - инд. предикат, определенный на _O_. Предположим, что в b(бета)=Эt(b^I(t)) где I(t)=1 на _О_, а t не входит свободно в b(бета).
Каждой переменной, связанной с факт. сущ-ия, сопоставим к.-л. функцию, опред. на _О_, приним. знач-ие из _O_ и зависящую только от переменных, связанных квантором всеобщности и предшеств. квантору существования. Если же квантору существования не предшеств. ни один квантор всеобщности, то мы ему поставим в соотв-ие к.-н. индивид. прдемет. обл.: х1, ..., xn1 ->(заменяем на опред.) x[0/1], ..., x[0/n1], где x[0/1] - x с индексами: верхний 0, нижний 1. zi->шi(y1, ..., yn2), где ш - "фи". vi->щi(y1,...,yn2; u1,...,un2), где щ - "пси" а un2 - u с нижним индексом n2. Все эти предметы и функции таковы, что в результате замены ими соотв. переменными в предикаты b(бета), получаемый предикат окажется истинным для всех значений входимых в него перменных, то будем указанные выше предметы и функции называть разрешающими функциями или ФУНКЦИЯМИ СКОЛЕМА: x[0/1], ..., x[0/n1]; шi(y1, ..., yn2), где ш - "фи"; щi(y1,...,yn2; u1,...,un2), где щ - "пси".
Говорят, что формула имеет сколемовскую нормальную форму, если ее за-пись не содержит кванторов существования, а все кванторы всеобщности следуют за всеми операциями алгебры высказываний, а формула Н не содержит кванторов и имеет КНФ. Для построения сколемовской нормальной формы (СНФ), формулу сначала необходимо привести к нормальной форме, затем бесквантовую ее часть привести к КНФ. После этого делаются следующие преобразования.
ЛЕММА: чтобы (1) была тождественна истиннана _О_необходимо и достаточно, чтобы для этой формулы существовали разрешающие функции.
ТЕОРЕМА ЛЁВИНГЕЙМА: если формула не содержит свободных переменных (но быть может содержит символы индивид. предметов), выполнима на некторой области, то она выполнима на полной (счетной) области.
