The right tack, ⊢, is typically read as “entails”, which is ambiguous due to the difference between syntactic entailment and semantic entailment. It is sometime read as “yields”, but although I agree with this word in the way it suggests something is produced, I feel it too much suggests something imperative, I mean “will produce” where I would expect “may produce”. So I was wondering if it could be read and written in natural language as “allows”. I mean to read or write A ⊢ b as, “given what is written in A, one can write b” (ex. like when ⊢ is used to express a typing judgement).
Then, there is the semantic entailment, ⊨. To help distinguish it from the syntactic entailment which allows (and not requires) to produce something, I was thinking about a word with no production connotation, like “means” or “says”. Ex. A ⊨ B would be read as “A means B” or “A also says B” (I feel to prefer the former).
I feel to not have that much doubt ⊨ can be read as “means” (I still may be wrong), I am more unsure about reading ⊢ as “allows”. What is your feeling about it?
— Edit —
After some comments, I believe I have to clarify. I was unclear in the way I had two point of view in mind with this question. To a target language, there may be two different point of view: the one from someone whose write in the language, to which syntactic derivations, allows sentences to be written, and the one from someone who proves or is interested in properties of the language, to which syntactic derivations yields cases to be covered.
The question is not in the contexte of teaching, I’m not a teacher (nor a student), it’s in the context of how to explain some things and provide material for people to be confident of some things about it.
Best Answer
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).