На этом шаге мы рассмотрим кванторы.
Квантор - логическая операция, дающая количественную характеристику предметной области, к которой относится выражение, получаемое в результате использования квантора.
Квантор - это общее название для логических операций, которые по предикату P(x) строят высказывание, характеризующее область истинности предиката P(x). В логике предикатов первого порядка применяются квантор всеобщности " и квантор существования $.
Кванторы всеобщности " и существования $ используются для определения области действия переменных. Так, если x - переменная, то запись " x читается "для любого x ", "для каждого x " и т.п., а запись $ x - "существует x ", "хотя бы для одного x " и т.п.
Кванторы позволяют строить высказывания о множествах объектов и формулировать утверждения, истинные для этих множеств. Например, высказывание " xP(x) означает, что область истинности предиката P(x) совпадает с областью значений переменной x , а $ xP(x) - что область истинности предиката P(x) не пуста.
Часть формулы, на которую распространяется действие квантора, называется областью действия этого квантора.
Вхождение переменной в формулу непосредственно после знака квантора или в область действия квантора, после которого стоит эта переменная, называется связанным. Все остальные вхождения переменных называются свободными.
Например, вхождение переменной x в формулу F будет связанным, если x входит в часть формулы F вида " x F или $ x F; остальные вхождения x в формулу F будут свободными.
Формула, содержащая свободные вхождения переменных, зависит от них (является их функцией); связанные же вхождения переменных можно переименовывать, например, заменив переменные, попадающие под квантор существования, константами.
Переменная x называется параметром F, если найдено хотя бы одно свободное вхождение x в F. Переменная является связанной, если она попадает в поле действия квантора. В противном случае переменная является свободной.
В одной и той же формуле переменная может быть и свободной (до попадания в поле действия квантора), и связанной (после попадания в поле действия квантора).
На следующем шаге мы начнем рассматривать формулы логики предикатов первого порядка .