Математическая логика и теория алгоритмов

занные в начале § 4 данной главы, ни задавали, мы всегда будем полу­ чать истинные отиощения или высказывания. Примером логически общезначимых формул, очевидно, являются следующие формулы: А=>А, \/хЛ^ЗхЛ, Л=Л. Если формула А является логически общезначимой, то будем записывать иногда в сокращенном виде: « |=Л» и эта запись читается: (<Л является логически общезначимой формулой (логики предикатов)». Формула логики предикатов А называется выполнимой, если существует интерпретация, в которой выполнима Л. Примером выполнимой формулы является формула VxA(x,y,bi). Действительно, если взять i ¥=[0,co), A{x,y,b\) поставить в соответствие предикат (отношение) х + у >z,b\ поставить в соответствие число 2, то наша формула в этой интерпретации означает, что \fx(x + у > 2). Последнее будет истинно, например, при любых значениях у> 2. Сле­ довательно, заданная формула выполнима в этой интерпретации. Таким образом, для нашей формулы существует интерпретация, в которой она выполнима, поэтому эта формула выполнима. Имеют место следующие очевидные утверждения. Формула А логически общезначима тогда и только тогда, когда формула "U не является выполнимой. Формула/4 выполнима тогда и только тогда, ког'да формула ~\А не является логически общезначимой. Будем называть формулу логики предикатов А противоречием, если формула "U является логически общезначимой или, что то же, если формулаложна во всякой интерпретации. Говорят, что формула логики предикатов А логически влечет формулу логики предикатов В, если в любой интерпретации формула В принимает значение И при каасдой совокупности значений свобод­ ных переменных (входящих в ^4 и JB), при которых формула А приняла значение И. Иначе говорят, что В является логическим следствием формулы А. В этом случае записываем Л }= S и читаем; «из А логиче­ ски следует JS » или «В является логическим следствием из А». Отме­ тим, что «А [= ВУ> не является формулой, а является мегаутверисдением относительно формул/4 и В (логики предикатов). 61

RkJQdWJsaXNoZXIy MTY0OTYy