I have the following assertion:
∀x(E(x) ↔ ¬F (x)), ∀x(E(x) → G(x)) |= ∃x(F (x) ∧ ¬G(x))
Using the semantic tableaux method, I was able to get a counterexample in the form of G(a)=true, E(a)=true and F(a)=false.
My problem is that I'm having a hard time defining this counterexample as a structure. A structure consists of a domain, relations, functions and constants in the following format,
S = {domain; relations; functions; constants}
Now, I know that the relations are E, F and G, and the constant is {a}. I need some help defining the structure below,
S = {domain?; {E, F, G}, {functions?}, {a}}
Any help would be appreciated. Thanks!
For the domain you choose as individuals simply all the constant symbols that occur in any formula on the branch which you derive the countermodel from; in your case: {a}.
The interpretation of the predicates encompasses all tuples (and no others) for which there is a unnegated atomic formula on the branch: I(G) = {a}, I(E) = {a}, I(F) = ∅.
The set of function symbols in your example is empty, otherwise you would collect all equalities on the branch.
Individual constant interpretations are not needed as it is convention that you simply identify the constant name with the symbol you use to specify the corresponding individual in the structure, e.g. a.