FOL - Countermodel for argument without predicates

Question

Proof for: $∀x∀y(x=y)$

I have shown above the proof for $∀x∀y(x=y)$. However, I'm unsure how to build a counter-model for it.

Normally I would start building the domain, $D = \{\delta_{a},\delta_{b}\}$. Although there are no predicates in the argument, so does actually mean that there is to be no domain?

I mean, using the ∃ rule I still do substitute the 2 variables for the constants $a$ and $b$, but there are just no predicates to which to apply the interpretation function, $\nu$.

I would also expect to attain, $\nu(a)=\delta_{a}$ and $\nu(b)=\delta_{b}$, just no truth values.

Using a automated proof theorem software, the countermodel I get is: $D = \Phi$. So, I suppose my question consists of:

• When building the domain, do you only building from those terms attached to a predicate?
• If this is the case, are all arguments without a predicate going to end up $D = \Phi$?

N.B. if there are any glaring misconceptions it appears I may have, I'd greatly appreciate them being highlighted!

Answer 1

When building the domain, do you only building from those terms attached to a predicate?

A simple domain with two elements : $D = \{ a,b \}$ is enough.

Having found an interpretation with domain $D = \{ a,b \}$ (with a≠b) that satisfies the negation of the formula, i.e. falsifies it, is enough to conclude that the formula is not true in every interpretation, i.e. not valid.

---

The rules for managing quantifiers with Tableau method are simple :

The semantic tableau is a tree $\mathcal T$ that initally consists of a single node, the root, with the initial formula $\varphi$ and the set $\{ a_{0_1}, \ldots, a_{0_k} \}$ of constants that appear in $\varphi$. If $\varphi$ has no constants, take the first constant $a_0$ of the language.

Then, every time we found a node of a tree with a quantifier :

instantiate an universal quantifier with a constant $a$ whatever;

instantiate an existential quantifier with a constant $a'$ not already used.

The rules apply to quantified formulas $\forall x A(x)$ and $\exists x A(x)$, where the formula $A(x)$ may contain predicate symbols and equality : $=$.

Answer 2

Your 'proof' that $\forall x \forall y \ x=y$ is of course a disproof, because you ended up with an open but finished branch.

Moreover, from that very tree branch, you can immediately see the counterexample world: it is a world with $2$ distinct objects: $a$ and $b$

But, you ask, why are there no predicates? Well, actually, $=$ is a (2-place) predicate ... it's just that in logic this predicate is pre-defined to work like the identity predicate ... and so you don't get to interpret it.