# First Order Logic knowledge base problem

I would like to present in the predicate logic the knowledge base and then check if the one provided formula is satisfied using the defined knowledgebase. I am trying to do this using SPASS prover, but I don't know why I get results I don't want to have. For example, I have a knowledge base:

$$\forall x: A \implies B \\ \forall x : B \implies \neg{A} \\ \forall x : B \implies C \\ \forall x : C \implies \neg{B} \\$$ And then I want to prove that formula $\exists x : B \implies A$ is false. With the last formula it is false, but without is true. I want to be it false, because of the second formula in knowledgebase.

Here is the SPASS prover input: https://pastebin.com/4PEV0JGr you can try it by pasting into WebSPASS: https://webspass.spass-prover.org/

My aim is to represent the sequence of events (sth. like state machine, automata) $A \rightarrow B \rightarrow C$ in FOL and then ask if something can happend. For example in the mentioned sequence it is possible to go from $A$ to $B$ but it is impossible to go from $B$ to $A$ and it should be false for these sequence. But if the sequence would be $A \leftrightarrow B \rightarrow C$ then the both formulas $A \implies B$ and $B \implies A$ should be true. I use implication $A \implies B$ as a possibility to change the state from $A$ to $B$.

Could anyone help me with understading this problem and give me some tip or solution?

$\forall x : A \implies B \land B \implies \lnot A$
can be combined to say
$\forall x : A \implies \lnot A$

$\therefore \forall x :\lnot A$

similarly, $\forall x :\lnot B$

now, $\exists x : B \implies A$ is always the same as $\exists x : False \implies False$.

"if False, then False" is vacuously true. In this case not just for some x but for all x.

You are trying to prove that something is false when in fact it is true. This will be impossible.

• So why SPASS prover indicate formula $\exists x: B \implies A$ as false with database $\forall x: A \implies B$, $\forall x: B \implies \neg{A}$ ? – michalk93 Jun 12 '18 at 16:53