For example, given Theory T with predicates $$A(x), B(x), C(x,y), D(x,y), x=y$$ axioms $$\exists x.A(x) \land \exists x.B(x) \land \exists xy.C(x,y)\\ \forall x(A(x) \leftrightarrow \neg B(x)),$$ produce interpretation where formula $$\forall x\forall y(C(x, y) \to A(x))$$ is false.

How-do you solve problems like this? I have a suspicion that one should introduce objects into interpretation domain D and define their truth values (of course, following axioms) in a such way that there is object x that can produce true from predicate C while producing at the same time false from predicate A (the idea is that implication is false only in one case - when premise is true but consequence - false). Am I right?

Also I'm interested how does one prove that formula is satisfiable or not satisfiable in some interpretation and how does one produce interpretation that shows it.

  • $\begingroup$ Well, this is rather trivial where there are no axioms governing $C(x,y)$; given a model of your axioms, make a new model with $A,B$ interpreted the same way, and define $C$ to be the binary relation $\{\langle x,y\rangle: B(x)\}$. $\endgroup$ – Malice Vidrine Jan 19 '14 at 20:04
  • $\begingroup$ Your question is more complicated than it needs to be: all you're really asking is "how do you find a model of a theory?" and in particular have asked about the theory $$T + \neg \forall x\forall y(C(x, y) \to A(x))$$ $\endgroup$ – user14972 Jan 19 '14 at 21:35
  • 1
    $\begingroup$ Regarding your question : "how does one prove that formula is satisfiable or not satisfiable in some interpretation and how does one produce interpretation that shows it", you can refer to tableaux method. It is quite simple (for propositional and first-order logic) and can solve this kind of problems, i.e. verify if a (finite) set of formulae is satisfiable and, if so, build up a model showing it. $\endgroup$ – Mauro ALLEGRANZA Jan 20 '14 at 12:37

In general, finding an interpretation in which some sentence fails can be rather hard. But in this case, we have a very weak theory, and one of the predicates has no conditions on it.

We know that there are at least two things in any intepretation of this theory; there's a $B$ thing and an $A$ thing and nothing can be both. In fact ignoring the predicate $C$ entirely, we can make a model of the other axioms with exactly two elements. Then we figure out what we want $C$ to be. One can go even simpler than I did above and define $C:=\{\langle x,y\rangle: A(x)\vee\neg A(x).\wedge.A(y)\vee\neg A(y)\}$. Point is, we need $C(x,y)$ to be true when $A(x)$ is false; in this case, $C(x,y)$ is true of everything and we know one thing $A(x)$ is false of.

My inspiration for this intepretation was an intepretation in a natural language sense: a bag of Go stones with $A$ being "is a white stone", $B$ being "is a black stone" and $C(x,y)$ being defined as above. Trying to think of your predicates as predicates in some similar language is a good way to start getting ideas.

  • $\begingroup$ But the 2nd axiom [i.e., $\forall x ( A(x) \leftrightarrow B(x) )$ ] says that the (at least one) "$A$s" and the (at least one) "$B$s" must coincide ! $\endgroup$ – Mauro ALLEGRANZA Jan 19 '14 at 20:51
  • $\begingroup$ @Mauro: I could swear when I read it it said $A(x)\leftrightarrow\neg B(x)$! Let me check the edit history and adjust appropriately. $\endgroup$ – Malice Vidrine Jan 19 '14 at 21:00
  • $\begingroup$ Before the revision it was written "Ax(A(x) <-> ~B(x))", and I think the "~" got lost in the Tex. I believe my reading was the intended one. $\endgroup$ – Malice Vidrine Jan 19 '14 at 21:05
  • 1
    $\begingroup$ Assuming the revised reading of the 2nd axiom [i.e., $\forall x (A(x) \leftrightarrow \lnot B(x))$ we can build a model with two elements $0$ and $1$. Let the predicates $A(x)$ and $B(x)$ interpreted as $x = 1$ and $x = 0$, respectively. And let $C(x,y)$ interpreted as "$ x < y$". The axioms are satisfied, but $(0 < 1) \land \lnot (0 = 1)$ This last formula is an instance of $\exists x \exists y (C(x,y) \land \lnot A(x))$ which is the negation of $\forall x \forall y (C(x,y) \rightarrow A(x))$. Note The predicate $D$ is not used at all ... $\endgroup$ – Mauro ALLEGRANZA Jan 19 '14 at 21:21
  • $\begingroup$ Yep, that also works. In fact I think if you use $\leq$ instead then your answer interprets my brief answer in the comments. $\endgroup$ – Malice Vidrine Jan 19 '14 at 21:31

You are looking for a countermodel

A countermodel is a model (interpretation) where all axioms are true and the statement you are investigating is false.

So in your case: when is $\forall x\forall y(C(x, y) \to A(x) )$ false?

It is false when $ \lnot \forall x\forall y(C(x, y) \to A(x) )$ is true.

When $\exists x \exists y( \lnot(C(x, y) \to A(x) ))$ is true.

when $\exists x \exists y( C(x, y) \land \lnot A(x) )$ is true.

And this is true when for some x and y (let change them to a and b, dont use variables that are not bounded)

C(a, b) is true A(a) is false

Now you only have to check if this combination is invalidated by the axioms.


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.