Исключение кванторов общности.

После исключения кванторов общности и стандартизации переменных формула содержит только кванторы общности, каждый из которых имеет свою переменную. Поэтому кванторы общности можно перенести в начало формулы (получаем предварённую формулу) и считать областью действия каждого квантора часть формулы, расположенную за ними. Например:

.

В связи с тем, что в импликации множество состоит из замкнутых формул, т.е. из формул, не содержащих свободных переменных, и формула F замкнута, все переменные в формуле из будут относиться к кванторам общности. А так как порядок расположения кванторов общности не имеет значения, то эти кванторы можно явно не исключать, условившись, что все переменные в формуле относятся к кванторам общности.

Таким образом, кванторы исключают, получив предваренную форму из одних кванторов общности.

Дата добавления: 2015-07-11