Една формула се нарича безкванторна, ако може да се построи от атомарни формули и true чрез използване само на отрицание, конюнкция, дизюнкция, импликация и еквиваленция. За всяка безкванторна формула с n атомарни компоненти съществува двоична функция на n променливи, изразяваща верностната стойност на формулата в коя да е структура при дадена оценка на променливите чрез верностните стойности на атомарните компоненти на формулата в същата структура при същата оценка на променливите.
    Дизюнкция на списък от литерали се нарича елементарна дизюнкция, а конюнкция на списък от литерали се нарича елементарна конюнкция. Една елементарна дизюнкция се нарича хорнова, ако най-много един от членовете й е атомарна формула без отрицание. Всяка безкванторна формула е еквивалентна на някоя конюнкция от елементарни дизюнкции (конюнктивна нормална форма на дадената формула) и на някоя дизюнкция от елементарни конюнкции (дизюнктивна нормална форма на дадената формула).
    Формула, получена от безкванторна формула чрез поставяне на някакъв брой квантори за общност пред нея, се нарича универсална формула, а безкванторната формула, от която тя е получена, се нарича нейна безкванторна част. Една универсална формула се нарича хорнова, ако безкванторната й част е еквивалентна на някоя конюнкция от хорнови елементарни дизюнкции. Една затворена формула се нарича изпълнима, ако е вярна в поне една структура. Едно множество от затворени формули се нарича изпълнимо, ако съществува структура, в която са верни всички формули от това множество. Като се представи безкванторната част на една затворена универсална формула в конюнктивна нормална форма, въпросът за изпълнимостта на дадената формула може да се изследва чрез метода на резолюцията. В специалния случай, когато формулата е хорнова, изследването за изпълнимостта й може по този начин да се сведе и до изследване за изпълнимост на хорнови цели при хорнова програма.
    Дефинира се резултат от прилагане на субституция към безкванторна формула и това дава възможност да се говори за частни случаи на безкванторна формула. Ако една безкванторна формула е тъждествено вярна в дадена структура, частните случаи на тази формула също са тъждествено верни в тази структура. При предположението за наличието на константа в сигнатурата една затворена универсална формула е изпълнима точно тогава, когато е изпълнимо множеството на затворените частни случаи на безкванторната й част. При същото предположение е в сила теоремата на Ербран, че ако една затворена безкванторна формула е неизпълнима, то някое крайно множество от затворени частни случаи на безкванторната й част също е неизпълнимо. Този резултат има връзка с теоремата за компактност, според която всяко неизпълнимо множество от затворени формули притежава неизпълнимо крайно подмножество.