1
$\begingroup$

I've read in some textbooks that $\vdash$ and $\vDash$ are symbols present only in metalanguage. From this, I infer that their use in object language is unacceptable.

I would like to know why. Can't we define them as relation symbols in a structure? Or introduce them in statements for the sake of formal proofs?

$\endgroup$
5
$\begingroup$

Consider for example propositional logic

The syntax specifications of the language allows us to build formulae from propositional variables : $p, q, \ldots$ and constants : $\bot, \top$ with the connectives; usually :

$\lnot, \lor, \land, \to$.

Thus, $p \to q$ is a "well-formed" formula, while, e.g. $p+q$ is not.

With the symbol :

$\varphi \vdash \psi$

we mean that the formula $\psi$ can be derived in the calculus from the formula $\varphi$.

Thus, $\vdash$ express a relation between formulae of the calculus but it is not a symbol of the language : it is not present in the syntax specifications above.

The "statements" in the metalanguage express "facts" about the language and the calculus, and thus are not formulae of the language.

This is the reason why the symbols : $\vdash$ and $\vDash$ are only part of the meta-language.

$\endgroup$
  • $\begingroup$ Yep, exactly. Well-explained. $\endgroup$ – goblin Apr 3 '15 at 9:39
  • $\begingroup$ Is "+" a symbol from the language of Peano Arithmetic? $\endgroup$ – Bruno Schiavo Apr 3 '15 at 17:18
  • $\begingroup$ @BrunoSchiavo - yes, it is a symbol of first order arithmetic. $\endgroup$ – Mauro ALLEGRANZA Apr 4 '15 at 11:55
  • 1
    $\begingroup$ Of course, just to confuse the picture, $\vdash$ often is used as an object language symbol in sequent calculus presentations of logics, and then you have to use some other notation for the logical consequence relation. $\endgroup$ – Rob Arthan Apr 5 '15 at 16:17
  • $\begingroup$ @RobArthan - you are right; this is due to the fact that the sequent calculus can be viewed as a calculus for the derivability relation ... $\endgroup$ – Mauro ALLEGRANZA Apr 6 '15 at 19:51
1
$\begingroup$

I can explain it like this.

Given a set $X$, write $X^*$ for the collection of all finite sequences in $X$, including the empty sequence. Now let $L$ denote an arbitrary set, which we think of as a "language"; so you should be thinking of the elements of $L$ as "formulae". Then:

Definition. An inference relation over $L$ is subset $\vdash$ of $L^* \times L$ subject to certain axioms, like:

  1. For all $\Gamma \in L^*$ and all $\varphi \in L$, if $\varphi$ occurs somewhere in $\Gamma$, then $\Gamma \vdash \varphi$.

  2. etc.

Note that we write $\Gamma \vdash \varphi$ as a more readable alternative to the more correct $(\Gamma,\varphi) \in \;\vdash$. This notation can be seen in axiom 1, for example.

Now here's where the ambiguity creeps in. Suppose $L$ is the set of all strings featuring the symbols $0,1$, the comma symbol, and the symbol $\vdash$. So a generic element of $L$ looks like:

$$0\vdash 1,,0\vdash,1$$

You can see the issue, right? If we suppose furthermore that $\vdash$ is an inference relation on $L$, then we cannot tell what "$01,1 \vdash 1$" means. It could be an element of $L$. Or, it could be the writer attempting to claim that $(\langle 01,1\rangle,1) \in \;\vdash$. Without further information, we cannot know.

To avoid this kind of ambiguity, we would choose a different symbol for the inference relation, as in:

Suppose furthermore that $\vdash'$ is an inference relation on $L$.

It now becomes clear that $01,1 \vdash 1$ is intended to denote an element of $L$, whereas $01,1 \vdash' 1$ is expressing the proposition that $(\langle 01,1\rangle,1) \in \;\vdash'$.

Make sense?

$\endgroup$
  • $\begingroup$ That $*$ is the Kleene Star, right? $\endgroup$ – Luis Orion Mar 14 at 21:12
  • $\begingroup$ @LuisOrion, indeed. "Given a set $X$, write $X^*$ for the collection of all finite sequences in $X$, including the empty sequence." $\endgroup$ – goblin Mar 15 at 2:06
1
$\begingroup$

You can use whatever symbols you want to denote whatever you want. For example, you can use ${\mathfrak w}_\$^7$ as a binary function symbol for addition of natural numbers. The utility of that is questionable, though.

More seriously, you certainly can introduce them if the structure in question is rich enough to intepret those in a meaningful way: for example, we can certainly interpret $\vdash$ and $\vDash$ in models of set theory.

This is actually how Gödel's incompleteness theorems are proved: by interpreting $\vdash$ in a theory of arithmetic. The problem with that is this is merely an interpretation, and depending on the model in which it is considered (which is why the second incompleteness theorem is possible).

Those interpretations are distinct from the "true" $\vdash$ and $\vDash$ (though they will, of course, coincide in case of "true" natural numbers and "true" set-theoretic universe).

For an illustration of how such an interpretation can stray from being "true", consider the natural numbers $({\bf N},<)$ with standard ordering. This is a nice structure. It is isomorphic to $({\bf N},<_1)$ where $n<_1m$ iff $m=0$ and $n=1$ or $n<m$. So now you have an interpretation of $<$ which is quite different from the "true" $<$. Worse yet, there are (countable!) structures elementarily equivalent to $({\bf N},<)$ with infinite descending chains. In those structures, the interpretation of $<$ is (in some ways) very different from the standard interpretation.

The same can happen whenever you try to express $\vdash,\vDash$ in a formal language.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.