Why do they use |- instead of ->? Contrary to what others have said, I've only ever seen -> (implication) in my logic courses.
-> is material implication, so it is an operator of the object language. |- is part of the metalanguage that you use to reason about the object language. I am not that knowledgeable in logic, however.