What are the meanings of the various turnstiles It is easy to find the meanings of $\vdash$ and $\models$ (see this question and Wikipedia) but what of the (triple?) turnstile $\Vvdash$ and the (vertical double?) turnstile $\Vdash$? Do they have a standard accepted meaning and usage?
(It seems implausible that no exhaustive index of all these symbols already exists but I couldn't find one)
 A: According to Change/Keisler, "Model theory", 3rd edition, page 209, the double vertical bar turnstile means the "finite forcing relation". The detailed explanation is somewhat technical.
PS. Much the same definition for the double vertical turnstile is given by Smullyan/Fitting, "Set theory and the continuum problem", page 210. They say that $p\Vdash X$ means "$p$ forces $X$".
PPS. Jech, "The axiom of choice", page 202, says $p\Vdash\phi$ means "$p$ forces $\phi$".
PPPS. Huth/Ryan, "Logic in computer science", page 310, says $x\Vdash\phi$ means "$x$ satisfies $\phi$" or "$\phi$ is true in world $x$". So far I haven't found any triple vertical bars.
PPPPS. Curry, "Foundations of mathematical logic", pages 185–186, uses the double vertical turnstile, but his explanation of its meaning is totally incomprehensible.
PPPPPS. My other 40 books on mathematical logic and model theory don't use the double vertical turnstile, and none of them use the triple vertical turnstile. So I imagine it's not in common use.
