I'm trying to express this in FOL:
Every word has at least one concept associated w/ it, and every concept has at least one word associated w/ it. Would it be:
For all (x)(Cx<->Wx)
(for all x(w(x) -> there exists y(c(y) & r(x,y)))) & (for all y(c(y) -> there exists x(w(x) & r(x,y)))), where r(x,y) denotes the concept associate w/ the word x. Anyway to make that clearer? What would this actually look like on paper?
Why do you want to express this in FOL? BTW why not UML? Isn't the expression you want to arrive at an app?
In quantificational logic, (x) (Cx<->Wx) translates as; For any (x), C(x) if and only if W(x). Your elaboration paints a different picture.
You would need to assert something (i.e. universal or existential quantifier) to establish a categorical syntactical structure (unless you are assuming it).
Also, you would need to elaborate on the sentence constants (i.e. C and W) to show what exactly you are trying to prove.
Also, you may want to reconsider your notation with the bi-conditional and quantificational logic.
Oh. You don't need to go into quantificational logic for that. You can stay within the realm of propositional logic and still accomplish your goal without predicative inferences.
All you need is a standard bi-conditional and a truth table to prove it.