2015-03-27
520
После исключения кванторов общности и стандартизации переменных формула содержит только кванторы общности, каждый из которых имеет свою переменную. Поэтому кванторы общности можно перенести в начало формулы (получаем предварённую формулу) и считать областью действия каждого квантора часть формулы, расположенную за ними. Например:
.
В связи с тем, что в импликации 
множество состоит из замкнутых формул, т.е. из формул, не содержащих свободных переменных, и формула F замкнута, все переменные в формуле из 
будут относиться к кванторам общности. А так как порядок расположения кванторов общности не имеет значения, то эти кванторы можно явно не исключать, условившись, что все переменные в формуле относятся к кванторам общности.
Таким образом, кванторы исключают, получив предваренную форму из одних кванторов общности.
