[FOM] Double turnstile and other bad notations

[Arnon Avron]

I take this question as an opportunity to call against what
I believe to be bad habits of notations - something that
logicians should be more cautious about than anybody else.

The "double turnstile" (\models, or even \vDash, that  only
after reading this exchange of messages I noticeid that it 
looks a little bit different) is unfortunately used for two
completely different things, *of different types*.

1)  As the symbol used by everyone for the satisfaction
    relation between structures and formulas (or sets
    of formulas).

2) It is also frequently used for a consequence relation (CR)
   between sets of formulas and formulas, provided 
   the relation is semantically defined.

In contrast, the usual turnstile \vdash is frequently reserved
by people for denoting a relation of the second type 
(i.e. consequence relation) when that relation is 
defined by some proof system. However, it is not exclusively
used for such relations. Every book or paper I have 
ever come across which deals with general theory 
of consequence relations (whether Tarskian or Scottian)
use the ordinary \dash to denote arbitrary consequence 
relationss, no matter how they are defined.

  Keeping some discipline of types is very important for
avoiding mistakes and confusions, especially among students.
Therefore I am very cautious when I teach logic to
use \models just for satisfaction relations, and \vdash
for all sorts of consequence relations. Exactly like Feferman
(according to one of the recent messages; I was not aware
of this, but it fits well Sol's logical exactness) 
I use subscripts and superscripts to represent
how a given CR is defined. (Note that this is in any
case necessary: The same CR may be defined by completely
different types of semantics and/or several 
completely different proof systems).

  Another confusing notation that I have frequently encounter
is the use of \vdash for separating the two sides of 
a sequent in Gentzen-type systems (instead of the special
sorts of arrow used by Gentzen, Kleene, Takeuti...). 
Such notation confuses an internal  symbol of the formal
language of Gentzen-type proof symbols with the symbol used
in their *meta-language* for denoting one of the
CRs that the system might be used for. It should
be obvious that such a confusion between formal language
and its meta-language should be avoided in general. In this
particular case it has two particular bad effects:

I) It rules out (or at least makes it difficult
   even to consider) the use of consequence relations
   between sequents. It does not seem to make much sense 
   (although not impossible)  to write something like:
  
       |- p(x) |-  |-\forall x. p(x)

   while it is very useful to observe that in LJ and LK:

      => p(x) |- => \forall x. p(x)

ii) It forces (at least psychologically) users to consider only
    one possible use of a Gentzen-type system for defining CRs.
    But even for LK there are two different canonical ways
    how to use it for defining when A follows from T:

    A) If there exists a finite subset \Gamma of T 
       such that \Gamma => A is derivable in LK.
 
    B) If => A is derivable in LK from the set {=>B : B in T}.

Definition A corresponds to the "truth" (or "local") CR
of classical logic, used also in natural deduction systems
(and preserves truth of formulas, with respect to a structure
and an assignment in it).

Definition B corresponds to the "validity" (or "global") CR
of classical logic, usually associated with Hilbert-type
systems. It is the one used in the classical books of Mendelson
and Shoenfield (and preserves validity of formulas
in structures). 

The main difference between these CRS is that the
generalization rule is sound with respect to the
second, but not with respect to the first.

Arnon Avron
 
On Fri, Jan 06, 2017 at 12:47:18PM -0500, Christopher Menzel wrote:
> FOM folk,
> 
> The turnstile (\vdash) is typically traced back to Frege and was picked up by Whitehead and Russell, who used it more or less to indicate provability, and of course this largely continues to the present day. But whence the double turnstile (\models) to indicate logical consequence? I thought perhaps I'd find it in Carnap or, at least, in Kemeny's famous 1956 JSL articles, but it's not there; they just adopt ordinary language expressions to indicate semantic relations. From the very limited bit of searching I've done, the double turnstile appears to be of fairly recent vintage. Does anyone know its origins or, at least, can anyone point to an earlyish (even pre-1960) use of the notation?
> 
> Thanks.
> 
> Chris Menzel
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> http://www.cs.nyu.edu/mailman/listinfo/fom