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?


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.