How do I read a ⊢ ab in mathematical logic? I'm beginning to read the interesting Introduction to Mathematical Logic, by Detlovs and Podnieks, but I'm having some troubles with a few simple concepts.
In an early paragraph, the following theory is described:

Our second example of a formal theory is only a bit more serious. It was
      proposed by Paul Lorenzen, so let us call this theory L. Propositions of L are
      all the possible "words" made of letters a, b, for example: a, b, aa, aba, baab.
      Thus, the set of all these "words" is the language of L. The only axiom of L is
      the word a, and L has two rules of inference: X |- Xb, and X |- aXa. This
      means that (in L) from a proposition X we can infer immediately the
      propositions Xb and aXa. For example, the proposition aababb is a theorem of
      L:
      a |- ab |- aaba |- aabab |- aababb
      rule1 rule2   rule1    rule1
      This fact is expressed usually as L |- aababb ( "L proves aababb", |- being a
      "fallen T").

How do I read a ⊢ ab? Surely not "a proves ab", I suppose.

$X \vdash \phi$ means that $\phi$ is derivable from the set [of expressions] $X$. 
If we are working in logic (propositional or other), this is exactly : 

the formula $\phi$ is provable from the set of axioms or assumptions $X$, by way of the inference rules of the system. 

But we can use this symbol in a more general context, like that of a formal system. 
In this case, we say that :

the expression $\phi$ is producible (or again : derivable) from the set of expressions $X$, according to the transformation rules of the system. 

