Преобразование предикатов

[Joker_vD]

Есть предикаты $A(a,a')$, $B(b,b')$, $C(a,b,c)$, и построенный из них предикат $D(a,a')=A(a,a')\wedge \forall b \forall b' (B(b,b') \rightarrow \exists c\, AB(a,b,c))$. Нужно переписать его, избавившись от импликации и кванторов всеобщности: в конечном ответе разрешается использовать квантор существования, конъюнкцию и такую вот "полуразность": $P(x,y) \diagdown Q(y,z) \stackrel{def}{=} P(x,y) \wedge \overline{\exists z\, Q(y,z)}$. Последняя операция определена для предикатов любой арности, в ней буквами $x,y,z$ обозначены "составные переменные": $x$ — переменные, входящие в $P(x,y)$, но не в $Q(y,z)$; $y$ — переменные, входящие и в $P(x,y)$, и в $Q(y,z)$; $z$ — переменные, входящие только в $Q(y,z)$, но не в $P(x,y)$.

Так вот, я очевидным образом переписал это дело как

$$D(a,a') = A(a,a') \wedge \overline{\exists b \exists b'\, (B(b,b') \wedge \overline{\exists c\, AB(a,b,c))}},$$

но я не могу свернуть внутреннюю скобку в полуразность: $AB(a,b,c)$ содержит $a$, а $B(b,b')$ — нет. Была идея "расщепить" $A(a,a')$ в $A(a,a')\wedge A(a,a')$ и внести одну $A(a,a')$ внутрь внешнего отрицания, но там выскакивает какая-то дикая дизъюнкция.

В ответе вроде бы должно получаться

$$A(a,a') \diagdown \bigl((A(a,a') \wedge B(b,b')) \diagdown AB(a,b,c)\bigr),$$

но что-то не выходит...

[cyb12]

Joker_vD в сообщении #506348 писал(а):

Была идея "расщепить" $A(a,a')$ в $A(a,a')\wedge A(a,a')$ и внести одну $A(a,a')$ внутрь внешнего отрицания, но там выскакивает какая-то дикая дизъюнкция.

У меня вот вполне получилось. Если сделать как $x\wedge \overline{y} = x \wedge \overline{x\wedge y},$ то получится, что

$$D(a,a') = A(a,a') \wedge \overline{\exists b \exists b'\, (A(a,a') \wedge B(b,b') \wedge \overline{\exists c\, AB(a,b,c)})},$$

дальше пишем, что это есть

$$ A(a,a')\diagdown (A(a,a') \wedge B(b,b') \wedge \overline{\exists c\, AB(a,b,c)}), $$

а далее как раз и ответ получается....

[Joker_vD]

cyb12
$x\wedge \overline y = x \wedge \overline{x\wedge y}$. Блин, и правда. Спасибо!