I think the pedagogical ambiguity here is best resolved exactly by not introducing a new term: instead use the totally unambiguous phrases "syntactic entailment" and "semantic entailment" (until fluency is achieved of course).
This is especially true since logic already suffers from an abundance of terminology (signature/vocabulary/type/alphabet; countable/denumerable/enumerable; recursively enumerable/computably enumerable/recognizable/semidecidable/; etc.).
That said, suppose one is absolutely dead-set on introducing a new notation; what's a least-bad choice?
"Allows" is in my opinion a poor choice here: there's no sense in which "$\vdash$" is less compulsory than "$\models$," so I don't see what difference is being emphasized. It's also highly misleading in that it would lead to the conclusion that more restrictive axiom sets allow more things. Adding axioms in the hope of removing inconsistencies is a common mistake students make ("Let's get rid of Russell's paradox by forbidding self-containing sets"), and this wouldn't help.
"Deduces" has the advantage of being fairly unambiguous and connecting with existing terminology ("natural deduction"). However, the grammar is horrible: "$\Gamma$ deduces $\varphi$" isn't right at all. What we should say is "From $\Gamma$ we can deduce $\varphi$" or similar, but that's a mouthful. I personally do think grammar matters in this case: using a strange grammar makes the terminology feel more alien.
The best one I can think of is "justifies." The idea here is that we think of statements involving $\vdash$ as taking place in some dialogical process, with our goal being to construct an argument.
But again, I really think that no new terminology should be introduced; rather, the existing terms "syntactic entailment" and "semantic entailment" should be used until comfort is achieved. Besides the reasons mentioned above, this terminology has one very useful advantage: it emphasizes the similarity between $\vdash$ and $\models$, which is really the surprising feature (ultimately justified by the completeness theorem).
- Of course, in more advanced topics in logic we'll sometimes want to go the other way and emphasize the difference between the two notions, or work in a context where one or the other doesn't even exist, but those situations won't arise until well after we've achieved a basic level of competence - at which point this won't be an issue anymore.
Best Answer
I think the first one is right and the second is wrong. When the limit existis it is surely a number, and a number doesn't tend to anything.
Maybe he meant something like $$f(x)\overset{x\to \infty}{\to} 0$$ But I would prefer always $$\lim_{x\to \infty} f(x)=0$$ because the limit IS something and not tends to something.
When you use the arrows you say something like it tends to so essentially you say in $f(x)\to 0$ as $x\to \infty$ that when $x$ goes to $\infty$ your function tends to zero.
The second notation would be, as the limit is a fixed $c$, $$\text{c}\to 0$$ which I think is nonsense.
The notation to use depends on wheter you are in a text or you are in display mode. In a display mode I would use $$\lim_{x\to \infty} f(x)=0$$ In inline there are three options, the first is
Personally I prefer the third, because in the first the index will be hardly legible, in the second there are to many mathematical symbols in a sentence and the third will be the easiest to read.