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

Правила вынесения кванторов за скобки, когда задана имплика­ ция некоторых формул, следуют из теоремы. Теорема 2.7. Пусть А — произвольная формула, не содержа­ щая свободных вхождений переменой х, а В{х) - произвольная фор­ мула, возможно, и содержащая свободные вхождениях. Тогда ЗхВ(х)=>А ~ Vx(i?(x)=>^); (2,33) А=>\/хВ(х) ~ \/х(А=>В{х)), (2.34) УхВ(х)=>А ~ 3x(i?(x)=^^), (2.35) А=>ЗхВ(х) ~ Зх(Л=>1?(х)). (2.36) Доказательство. Докажем соотношение (2.33). Рассмотрим формулу: Vx(i?(x)=>^). (2,37) Вместо формулы (2.37) введем равносильную формулу Vx(1 Bix)vA), которая по (2.24) равносильна формуле (Vx1 i?(x))v^, которая равносильна формуле 1V X 1B ( X )=:^ A Используя соотношение (2.15) между кванторами, получим формулу (ЗхВ{х))=>А. Таким обра­ зом, формула Vx(i?(x)=>^) равносильна формуле (3xi?(x)) =>А, что и требовалось доказать. Доказательство равносильностей (2.34)-(2.36) можно провести примерно таюке, как доказывалось соотношение (2.33). Из излолсенного видно, что при вынесении кванторов за скобки для указанных формул кванторы могут выноситься без изменения, либо меняться на двойственные. В общем случае, одазывается, нужно проводить еще и переименование переменных, прежде чем вынести квантор за скобки. 73