I am new to formal languages and their theories and I am confused by these two particular symbols: $\models$ and $\vdash$. For example, let's say that we are working with the language of an ordered field:
$$\mathcal L = (\{+, \cdot)\}, \{\le\}, \{0, 1\})$$ where the functions and the predicate are binary. Now, let's also assume that our model is the field of the real numbers and let our theory be the set of the field axioms.
Let's denote our theory by $\mathcal T$. Now, what is the difference between these two notations:
$$\mathcal T \models (\forall x)(\forall t)(x \cdot x \le x \cdot x + t \cdot t)$$
$$\mathcal T \vdash (\forall x)(\forall t)(x \cdot x \le x \cdot x + t \cdot t)$$
$\begingroup$
$\endgroup$
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
4
$\Gamma \vDash \varphi$ means that based on the formal semantics of the symbols involved, it is impossible for all statements in $\Gamma$ to be true while $\varphi$ is false.
$\Gamma \vdash \varphi$ means that we can syntactically derive $\varphi$ from $\Gamma$. So that should really be defined relative to some kind of proof system with specific rules of derivations. That is, if $S$ is such a system, then we can say that $\Gamma \vdash_S \varphi$ if and only if using the rules of derivation of system $S$, we can derive $\varphi$ from $\Gamma$.
We can then also define the impotant notions of soundness and completeness of system $S$:
$S$ is sound iff for any $\Gamma$ and $\varphi$: If $\Gamma \vdash_S \varphi$ then $\Gamma \vDash \varphi$ (in other words, $S$ does not allow you to infer things that don't logically follow)
$S$ is complete iff for any $\Gamma$ and $\varphi$: If $\Gamma \vDash \varphi$ then $\Gamma \vdash_S \varphi$ (in other words, the rules of $S$ are string enough so that anything that logically follows can in fact be derived using the rules in $S$)
Since we typically assume that the formal proof system we are working with is both sounds and complete, we often drop the $S$ from $\Gamma \vdash_S \varphi$ and simply say $\Gamma \vdash \varphi$
-
$\begingroup$ So, in my example: $T \models \phi$ means that - if the field axioms hold - the square of a number can never be negative $T \vdash \phi$ means that it is possible to derive from the set of field axioms the fact that the square of a number is never negative? $\endgroup$– AemiliusFeb 5, 2018 at 18:51
-
$\begingroup$ I would also note that $\vDash $ means "(tauto)logical consequence" $\endgroup$ Feb 5, 2018 at 18:51
-
1
-
$\begingroup$ @Aemilius I think you mean "ordered field axioms" - there is no general notion of "positive" or "negative" in an ordinary field. (And indeed in some fields the additive inverse of the multiplicative unit - that is, $-1$ - can have a square root. For example, in $\mathbb{Z}/2\mathbb{Z}$ we have $-1=1$ so $-1$ is its own square root, and less trivially in $\mathbb{Z}/5\mathbb{Z}$ we have $2^2=-1$.) $\endgroup$ Feb 5, 2018 at 19:30