Изменения

Дана некоторая формула <tex>s</tex>.Будем говорить, что подстрока <tex>s_1</tex> строки <tex>s</tex> является подформулой, если она в точности соответствует какому-то одному нетерминалув дереве разбора строки <tex>s</tex>.

Если в формулу входит подформула, полученная по правиламдля кванторов (то есть, <tex>\forall x \alpha</tex> или <tex>\exists x \alpha</tex>), то мы будем говорить, что формула <tex>\alpha</tex> находится в области действия данного квантора по переменной <tex>x</tex>. Также, будем говорить, что любая подформула формулы <tex>\alpha</tex> находится в области действия данного квантора.}} {{Определение |definition=Если некоторое вхождение переменной <tex>x</tex> находится в области действия квантора по переменной <tex>x</tex>, то такое вхождение мы назовем '''связанным'''. Вхождение переменной <tex>x</tex> непосредственно рядом с квантором (<tex>\forall x \dots</tex>) мы назовем '''связывающим'''. Те вхождения переменных, которые не являются связанными или связывающими, назовем '''свободными'''. Формула, не имеющая свободных вхождений переменных, называется '''замкнутой'''.