Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

§ 7. Правила перестановки кванторов Пусть А - произвольная формула логики предикатов. Рассмотрим для А произвольную, но фиксированную интерпретацию. Сразу же из определения кванторов получаем, что там, где истинно Vx VyA, истинно и Vy VxA, и наобо­ рот. В силу произвольности интерпретации следует, что VxVyA -VyVxA. (2.16) Точно так же получаем, что ЗсВуА ~ ЗсВуА. (2.17) Таким образом, при перемене мест стоящих рядом одноименных кванто­ ров получаем равносильные формулы. Итак, одноименные кванторы, стоящие рядом, можно переставлять местами. Известно, что формулы А и В равносильны тогда и только тогда, когда А=В является логически общезначимой формулой (теорема 2.2). Тогда из (2.16) и (2.17) получаем, что формулы \/х \/уА=\/у VxA и Зс^А=^ЗсА являются логически общезначимыми. Разноименные кванторы, оказывается, можно переставлять не в каждой формуле. Докажем теорему. Теорема 2.5. Для каждой формулы А и любых предметных переменных хиу формула ЗхУуА^УуЗхА (2.18) логически общезначима, а формула УуЗхА^ЗхУуА (2.19) не является логически общезначимой (при любой формуле/!). Доказательство. Для доказательства логической общезначимости форму­ лы (2.18) фиксируем произвольную интерпретацию формулы А, и из определе­ ний кванторов сразу получаем, что формула (2.18) истинна. Таким образом, в любой интерпретации формула (2.18) истинна, следовательно, она логически общезначима. Чтобы доказать, что формула (2.19) не является логически общезначимой, достаточно привести пример формулы А и интерпретации для нее, где формула (2.19) не истинна. Пусть область интерпретации М - множество действительных чисел и формула А означает предикат х>у, тогда высказывание Vy3x(x>y) (2.20) означает, что для любого числа у существует число х большее, чем у. Это вы­ сказывание истинно. Высказывание, полученное из (2.20) перестановкой кванто­ ров Зс \/у(х>у), означает, что существует число х больше любого другого числа и, очевидно, является ложным. Тогда ложна импликация: Vy3x(x>y)^3xVy(x>y). 43