Вопрос по математической логике

[Evgeni2011]

Здравствуйте, уважаемые участники форума, прошу помочь мне в решении следующего вопроса. Даны две формулы языка первого порядка: $A=\exists x_1...\exists x_{r-1}\forall x_r Q_{r+1}x_{r+1}...Q_nx_n M(x_1,...,x_n) $ и $ A'=\exists x_1...\exists x_{r-1}Q_{r+1}x_{r+1}...Q_nx_n M(x_1,,...,x_n)[x_r:=f(x_1,...,x_{r-1})] $, здесь $Q_{r+1},...,Q_n$ - какие-то кванторы, $M(x_1,...,x_n)$ не содержит кванторов, $M(x_1,,...,x_n)[x_r:=f(x_1,...,x_{r-1})]$ означает предложение получающееся из $M(x_1,...,x_n)$ заменой $x_r$ на $f(x_1,...,x_{r-1})$, причем символ $f$ не встречается в $M(x_1,,...,x_n)$. Собственно вопрос: верно ли что $ \models A' $ тогда и только тогда, когда $ \models A $? И как это доказать? У меня получилось доказать, что $ \models A $ влечет $ \models A' $, а вот обратно пока никак.

[Geen]

$\exists x:\; x^2=f(x)$
$\exists x\forall y:\; x^2=y$
?

[Evgeni2011]

Geen в сообщении #971159 писал(а):

$\exists x:\; x^2=f(x)$
$\exists x\forall y:\; x^2=y$
?

Не совсем понял, напишите поподробней, что Вы имели в виду? Здесь вроде нет тавтологий.

[Geen]

Если я правильно понимаю, из первого, второе не следует?

[Evgeni2011]

Еще раз повторю, тут нет общезначимых формул. Утверждение, которое я пытаюсь доказать звучит так: общезначимость $A'$ влечет общезначимость $A$.