It says in that post that it is impossible to translate SAT into HORNSAT. But it is known that HORNSAT is P-complete, so any language in P can be translated into HORNSAT. Then if it is impossible to translate SAT, which is in NP, into HORNSAT, then wouldn't this imply that P is not NP? What am I missing?
That question was about a translation from an arbitrary instance of SAT to a HORN-SAT instance with the exact same satisfying assignments. The translation property needed for P$\neq$NP is just equisatisfiability, not equality of assignments. That is, it simply requires them both to be satisfiable, or unsatisfiable. If satisfiable, they may be satisfied by different assignments.
For example: $a \wedge \neg b$ and $\neg a \wedge b$ are equisatisfiable (they are both satisfiable), but they have different satisfying assignments.
The answer was that there can not be a satisfying assignment preserving translation, but this doesn't tell us whether there is a polynomial time satisfiability preserving translation.