Given : A finite set X and a collection $S_1,...,S_k$ of subsets of X. Question: Is there a set $C \subset X$ which is an exact cover for $S_1,...,S_K$. (So for each $S_i,\ C \cap S_i$ contains exactly one element.
I made a simple example set to have a better picture:
Let my $X$ be $= \{a,b,c,...z\}$,
$C = \{b,e,t\}$,
$S_1 = \{a,b,c\},\ S_2 = \{b,d,a\}, \dots, S_k = \{e,f,a\}$
So for each $S_i, C \cap S_i$ = 1.
So I need to say these in first order logic:
Every element of C is in X.
Every Si has an element in C.
No Si has two distinct elements in C.
This is what I have so far
$∀x(C(a) → X(a))$
$\underset{i∈[n]}{\forall} \ ∃a,∃b ((S_i(a) \wedge C(b))→ a=b)$
$\underset{i∈[n]}{\forall} \ ∃a,∃b ((S_i(a) \wedge S_i(b) \wedge C(a) \wedge C(b)) → a=b)$
If you can correct and guide me through this, it would be awesome. Thank you very much!
First, a little bit on your notation. If you want to express natural numbers, i.e. $\mathbb{N}$, use
\mathbb{N}in mathmode. But your indices only range from $1$ to $k$ anyway, so it'd be correct to use $1 \leq i \leq k$ or $i \in \{1,\dots , k\}$ in the universal quantifier.Your three statements in natural language capture what you want very well.
However, the translation into FOL is fault at some places.
The first one is correct.
For the second one you overcomplicate things. You want to talk about one element per set. So why are you introducing two existentially bound variables? There is also no need for implications and equality here. In general, you should be very careful to use implications only when you mean to. Remember an implication is trivially satisfied when the precondition is false. Here this would mean the formula is trivially satisfied if there is any element that is not in $C$, since the conjunciton on the left side of the implication could be easily made false by just picking that element.
It might be helpful to rephrase the statement in natural language such that it can be directly translated into FOL like this:
For the third the implication is true trivially since there is an elemnt not in $C$. The idea of the implication here is right tho. It's an important concept to keep in mind to express distinctness, even though I think the implication in there is not obvious. It's not much that has to be changed, so again, let me try to rephrase: