Translating statements into predicate logic? In the logical programming class I was given an example:
Everyone who is sane can learn. Insane people cannot study in university. Does this imply that everyone who cannot learn, cannot study in the university?
Define the following predicates
S(x) - x is sane
L(x) - x can learn
N(x) - x cannot study in university
Then the theory is:


*

*S(x) => L(x)  //Everyone who is sane can learn

*~S(x) => N(x) //Insane people cannot study in university

*~L(p)  // person p cannot learn


Implication: N(p) // person p cannot study in university ?
The answer is: true, p cannot study in university
The homework problem says: 
The king thinks that the queen thinks that she is insane. Is the king insane?
I defined the predicate T(x) - x thinks (x is sane), thinking = sanity


*

*T(k) => T(q) // the king thinks that the queen thinks

*T(q) => ~T(q) // the queen thinks she is insane


Implication: ~T(k) // the king is insane?
The answer is: true, the king is insane.
I'm sure this model is incorrect, and I would really appreciate if someone helped me with this.
Thank you!
 A: With your key for rendering the English into the language of first order logic, the two given premisses translate as

$$\forall x(S(x) \to L(x))$$
  $$\forall x(\neg S(x) \to N(x))$$

and you are asked whether these entail the following conclusion:

$$\forall x(\neg L(x) \to N(x)).$$

And that conclusion indeed follows. 
For take someone $a$ such that $\neg L(a)$. Then by the first premiss we know $S(a) \to L(a)$ whence $\neg S(a)$. By the second premiss $\neg S(a) \to N(a)$, whence $N(a)$.
So by conditional proof we have shown $\neg L(a) \to N(a)$. Since $a$ was arbitrary we can generalize to get the desired conclusion.
[One comment: in most modern dialects of the language of first-order logic, we would write e.g. $Sa, Nx, \neg Lx$ etc, without further brackets after the predicate letter.]
So far so good. But as to the second example, something hopelessly confusing is going on here. 'The King thinks that $p$' engenders an intentional context. Standard first-order logical syntax can't handle intentional contexts. [You can, as you do(?), have an extensional predicate $T$ meaning "thinks", without a content clause. But note that your $T(q) \to \neg T(q)$ renders "if the queen thinks, she doesn't think" which isn't what you want at all.]
