Predicate Logic - Is my answer correct? Construct a predicate logic proof equivalent to the following natural language
argument.
“No athletes are bookworms. Carol is a bookworm. Therefore Carol is not an athlete.”
Could someone please help with my symbols? 
Ans. 
Let $A(x)$ mean that $x$ is an athlete.
Let $B(x)$ mean that $x$ is a bookworm.
Let Constant $C$ denote Carol
$\forall x, A(x) \implies \neg B(x), B(C), \neg A(C)$.
Is this correct? I know we will have to apply rules down after this—but is my beginning even correct?
I sometimes feel that my starting statement should be
$\forall x, A(x) \implies \neg B(x), B(C), \iff \neg A(C)$.
Is this correct?
Thanks so much!!!
 A: The task here, it seems to me, is to construct a proof, that validates the argument you are given in natural language. So you need premises, and you need a desired conclusion. So your premises are $$\begin{align} & (1)\quad\forall x, A(x) \Rightarrow \lnot B(x) \\ \\ & (2) \quad B(C)\end{align}$$
Then, from these premises, you need to construct a proof which leads you to the conclusion:
$$\therefore \lnot A(C)$$
For example, you'd need to use universal instantiation on premise $(1)$ to infer $$(3) \quad A(C) \Rightarrow \lnot B(C)$$
Now you can simply use $(3)$ and premise $(2)$ to conclude, by modus tollens, that therefore, $(4)\quad \lnot A(C)$, though you might want to add a fourth step, double negation on premise $(2)$ to get $\lnot \lnot B(C)$, and then employ modus tollens to arrive at the conclusion.
This argument form, as given in natural language, is called a syllogism, which has the form:$$\begin{align} \quad & \text{No A is a B}\\ \\  \quad & \text{C is a B}\\  & \hline \\ \\  \therefore & \text{C is not an A}\end{align}$$
A: Your answer is not quite correct, but you're close. Let's take your answer apart:
$\forall x, A(x) \implies \neg B(x),A(C),\neg B(x)$ collects three statements. The first is "any $x$ that is an athlete is not a bookworm", the second means "C is a bookworm" and the third means "C is not an athlete. These parts are correct.
What is missing is that you need to match the original form of the argument. In particular, the statement is "therefore, Carol is not an athlete", whereas the "therefore" does not appear in your formalization. However, this points directly to the right solution: You need to tie the three statements together with logical connectives.
As a pointer on how to solve this, consider the following example: When I formalize "All cats are animals. Therefore, the cat Delila is an animal", a possible formalization would be $(\forall x, \mathsf{Cat}(x) \implies \mathsf{Animal}(x)) \implies (\mathsf{Cat}(\mathsf{Delila}) \implies \mathsf{Animal}(\mathsf{Delila}))$. Can you figure out the solution from here?
EDIT: The question was modified after this answer was posed. The expression $\forall x, A(x) \implies \neg \neg B(x), B(C), \iff \neg A(C)$ is not well-defined: writing $\iff P$ is like writing $= 0$, so it's not clear what you second attempt is supposed to mean.
