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

Question

I'm confused about the use of symbols $\vdash$ and $ \models$. Reading the answers to
Notation Question: What does $\vdash$ mean in logic? and What is the meaning of the double turnstile symbol ($\models$)? I see that:

the turnstile symbol $ \vdash $ denotes syntactic implication. Then $ S \vdash \psi$ means that $\psi$ can be derived from the formulae in $S$

the double turnstile $ \models $, denotes semantic implication. Then the notation $A \models B$ means simply that B is true in every model in which A is true.

So I understand that, e.g., $(ZFC+ A) \vdash B$ means that $A \Rightarrow B$ is a theorem in ZFC and, in this sense $\vdash$ is a mathematical symbol for a theorem. While $(ZFC+ A) \models B$ means that $ B$ is true in every model of ZFC in which $A$ is true, and, in this sense $\models$ is not a mathematical but a metamathematical symbol. I understand correctly? And those are the only uses of the two symbols?

Answer 1

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$).

Answer 2

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.

Answer 3

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.

Answer 4

"So I understand that, e.g., (ZFC+A)⊢B means that A⇒B is a theorem in ZFC and, in this sense ⊢ is a mathematical symbol for a theorem."

No. (ZFC+A)⊢B means that given ZFC and A, B is provable. (A⇒B) may not be provable, if say the Deduction Meta-Theorem does not hold for the system.

To illustrate the difference between the two symbols, suppose we have a system which has only one axiom: CCpqCCqrCpr and the only rule of inference is condensed detachment, and has semantics captured by the following matrix with "0" standing for falsity, and "1" for truth:

C  0  1
0  1  1
1  0  1

It holds that CCpqCCqrCpr $ \models $ CpCqp, since whenever CCpqCCqrCpr is true, so is CpCqp. However, CCpqCCqrCpr $\vdash$ CpCqp is not true, since we can't prove CpCqp from just CCpqCCqrCpr under the rule of condensed detachment.