Meaning of symbols $\vdash$ and $ \models$

You are right in your definitions, but both symbols can be used in the metatheory, meaning that they are used to describe properties and relations between objects of the theory : axioms, theorems, and between the theory and its models.

With a formal theory, like $\mathsf {ZFC}$ or $\mathsf {PA}$, based on first-order logic, it is useful to separate symbols of the language, like :

• $\lnot, \rightarrow, \land, \lor$, all belonging to the common first-order language

• $\in$, specific of set theory

• $+$, specific of arithmetic,

and symbols used in the meta-language, like :

• $\vdash$, for the relation of derivability in a theory, meaning there is a formal derivation of a theorem from the axioms of the theory

• $\vDash$, for the relation of logical consequence, meaning that a sentence in the language of the theory is true in all models of the theory, i.e. in all interpretations satisfying the axioms.

The two relations are linked through Gödel's completeness theorem.

Expanded edition

The above is a précis of the "standard view", dating back to the '50s and '60s of last century; see :

• Stephen Cole Kleene, Introduction to metamathematics (1952), page 87 :

We introduce, by a metamathematical definition, the notion of "formal deducibility under assumptions". Given a list $D_1, \ldots, D_l$ of (occurrences of) formulas, a finite sequence of one or more (occurrences of) formulas is called a (formal) deduction from the assumptions formulas $D_1, \ldots, D_l$, if each formula of the sequence is either one of the formulas $D_1, \ldots, D_l$, or an axiom, or an immediate consequence of preceding formulas of the sequence. A deduction is said to be a deduction of its last formula $E$; and this formula is said to be deducible from the assumption formulas (in symbols, $D_1, \ldots, D_l \vdash E$), and is called the conclusion of the deduction. (The symbol "$\vdash$" may be read "yields".)

See also :

• Stephen Cole Kleene, Mathematical logic (1967), page 26 :

we define : $B$ is a valid consequence of $A_1, \ldots, A_m$, or in symbols $A_1, \ldots, A_m \vDash B$, if, [...] the formula $B$ is true in all those [structures] in which $A_1, \ldots, A_m$ are simultaneously true. The symbol $\vDash$ may be read "entails".

And see footnote, page 36 :

The symbol "$\vdash$" goes back to Frege (Begriffsschrift, 1879); the present use of it to Rosser (1935) and Kleene (1934). [...] The parallel use of "$\vDash$" is perhaps original with Kleene (1956).

See Rob's comment below ; the sequent calculus (Gentzen, 1934) is a formalization of the derivability relation. The original Gentzen's syntax for sequents :

$\Gamma \rightarrow \Delta$

is often written with $\vdash$ in place of the auxiliary symbol $\rightarrow$ (or sometimes : $\Longrightarrow$).

Both symbols are either mathematical or metamathematical.

If you work in a universe admitting semantics for first-order logic, then $\models$ is a statement about a theory and a sentence, as well $\vdash$ is a statement about a theory and a sentence. Since theories and sentences are mathematical objects, this is a mathematical statement.

If you work internally in a model of $\sf ZFC$ and say that $\sf ZFC+\varphi\vdash\psi$, as a metamathematical statement, then you really say that the metatheory proves that there is a proof etc. etc.

As a side note, $\models$ is also used as a satisfaction relation between a structure and a sentence, not just theories and sentences.

It may be confusing because we make statements about ZFC while working in ZFC, but both are mathematical in the following sense:

Define $\mathrm{ZFC}=\{\varphi_e, \varphi_i,\varphi_c,\ldots\}$ as a set of formulas (i.e. sequences of letters) representing the usual axioms (extensionality, infinity, choice, ...).

A model of this $\mathrm{ZFC}$ is just a pair $M=(A,\in)$ of a set and a binary relation on $A$ satisfying the formulas in $\mathrm{ZFC}$ according to Tarski's definition of truth, the notation for this is $M\models\mathrm{ZFC}$.

We say $\mathrm{ZFC}$ satisfies a formula $\psi$ if for all models $M$ of $\mathrm{ZFC}$ we have $M\models \psi$. Again we just check if $\psi$ holds in $M$ according to the definition of truth. This is denoted $\mathrm{ZFC}\models\psi$, using the same symbol for something different.

On the other hand, we say that $\mathrm{ZFC}$ proves $\psi$, if we can derive $\psi$ from the axioms of logic, the formulas in $\mathrm{ZFC}$, and inference rules such as modus ponens. This is just a formal manipulation of symbols of various formulas and is denoted $\mathrm{ZFC}\vdash\psi$.

There's an amazing result called the completeness theorem (for first order logic) that for any theory $T$ (again just a set of formulas) and any formula $\psi$, we have $T\models\psi$ if and only if $T\vdash\psi$. Note that the "if" part is trivial.