I am working with automated prover. I am creating a theory, where an unary predicate PR should be true just for several constants, false otherwise. I made following axioms:
PR(const1).
PR(const2).
...
PR(constK).
I want to define it such that I can prove not(PR(T)) for every term T different from const1 ... constK. It can not be proven from the axioms above. How should I define PR?
I also tried to add the axiom below, still does not help.
forall x ( PR(x) -> x = const1 V ... V x = constK ).
To make it more clear, I need to define PR in a way, such that adding a new axiom PR(C) with a new constant would make my theory inconsistent. Adding PR(C) now just adds a new consistent axiom. I know I can add an axiom not(PR(C)) for each constant C, but there are too many constants in my theory.
There's no way to do this without all other constants appearing in some axiom. For a constant that doesn't appear in an axiom, there's nothing to keep it from being equal to one of the constants for which $PR$ is true. So you'll need something like $\neg PR(c)$ or $c\ne\text{const1}\land c\ne\text{const2}\land\ldots$ for every other constant $c$. Even if you come up with something that you prefer to $\neg PR(c)$, it'll have to mention each other constant at least once.