Множество формул исчисления предикатов и теорий первого порядка определяется в два этапа: сначала описывается понятие терма (как нелогической функции от нелогических переменных), через которое затем определяется понятие логической формулы.
Терм (сигнатуры ) определяется индуктивно: термами полагаются сначала предметные переменные и предметные константы, а затем - все выражения вида , где - любой из функциональных символов, а - любые из уже имеющихся термов.
Формула (сигнатуры ) определяется также индуктивно: простейшими формулами (атомами) полагаются выражения вида , где - предикатный символ и - термы, а затем формулами считаются все выражения вида , где и - атомы или любые из уже построенных так формул, а - любая из предметных переменных.
В выражении формула называется областью действия квантора . Если формула не содержит переменной , считается, что смысл и одинаков. Чтобы уменьшить число используемых логических символов, выражение вида , использующее квантор существования , рассматривается как обозначение формулы , выражающей тот же смысл, что и формула .
Пара называется алгебраической системой сигнатуры при условии, что - непустое множество, а - отображение, ставящее в соответствие каждой предметной константе - элемент , каждому функциональному символу - некоторую n-местную операцию в , каждому предикатному символу - некоторое n-местное отношение в . Множество называется областью интерпретации, а отображение - интерпретацией сигнатуры в .
Алгебраическая система путем интерпретации опредмечивает абстрактные символы, придавая им конкретный смысл в предметной области, характеризуемой множеством . Задание алгебраической системы позволяет вычислять значения термов и определять выполнимость формул.
Например, формула в любой алгебраической системе либо тождественно истинна, либо тождественно ложна, так как каждая из входящих в нее переменных связана квантором. Пусть интерпретируется как число 1, - как умножение (*), - как сложение (+), - как неравенство (<). Тогда в привычной записи формула принимает вид . Эта формула истинна, если областью интерпретации (множеством констант и возможных значений переменных) является множество натуральных чисел (т.е. ={1,2,3,…}), и ложна, если областью интерпретации является множество всех целых (положительных и отрицательных) чисел (т.е. ={…,-3,-2,0,1,2,3,…}).
Формула исчисления предикатов может быть выполнимой и опровержимой в одной и той же или в разных алгебраических системах, истинной в одних и ложной в других алгебраических системах, логически общезначимой (истинной в любой алгебраической системе) или противоречием (ложной в любой алгебраической системе). Таким образом, истинность формулы в одной алгебраической системе еще не гарантирует ее истинности в других, а логически общезначимые формулы исчисления предикатов, тождественно истинные в любых алгебраических системах, являются аналогом и обобщением тавтологий исчисления высказываний..
Существуют и способы записи формул исчисления предикатов, подобные нормальным формам исчисления высказываний. Известна процедура преобразования формул исчисления предикатов к виду , в котором все кванторы предшествуют формуле , не содержащей кванторов. Причем здесь - означает квантор ( или ), и различны при , - бескванторная формула. Это так называемая префиксная (предваренная) нормальная форма записи формулы. Случай, когда все суть , подобен дизъюнкции по наборам значений предметных переменных, а случай, когда все суть , подобен конъюнкции по наборам значений предметных переменных. Когда же все суть , а все - суть , получаем нормальную форму Сколема, подобную дизъюнктивной нормальной форме исчисления высказываний. На этом мы завершаем рассмотрение языка теорий (и исчисления предикатов) первого порядка.
Do'stlaringiz bilan baham: |