1
$\begingroup$

I have a formula in FOL: $\forall x \exists y: B(x) \implies C(y)$ and in SPASS: forall([X], exists[Y], implies(B(X),C(Y)))

I want to check the formula: $\exists x: B(X) \implies C(X)$ and in SPASS exists([X], implies(B(X), C(X)))

The problem is I want to determine that X and Y are different (like in my first formula) and I want to be the second formula false because of the fact, that B and C are for the same X: $B(X) => C(X)$ but my first formula said that it should be different.

Is there a way to tell SPASS that these arguments should be different?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.