[FOM] Is the derivability sign a metalinguistic sign?

[Arnon Avron]

> A simple problem about language and metalanguage in formal theory. 
> It is usually stated that |- (sign of derivability) is a 
> metalinguistic sign denoting (in a sequent calculus) a 
> relation between sets of formulas and formulas. 

It is a conceptual mistake to use |- (which is otherwise used
as a meta-language symbol for denotsing consequence
in formal systems) as a formal sign in a sequent calculus.
Unfortunately, some authors are doing this confusing mistake -
but no serious book in Proof theory is doing it. Gentzen
himself, as well as Takeuti in "Proof Theory", Troelstra
and Schwichtenberg in "Basic Proof Theory" (and Kleene in
"introduction to Metamathematics") are all using a special
formal symbol (like =>) to separate the two sides of a sequent,
never |-. Then one can write |-\Gamma=>\delta to denote
that \Gamma=>\delta is a theorem of the system, and 
S|-\Gamma=>\delta to denote the dertivability in the system
of \Gamma=>\delta from the set of sequents S.


Arnon Avron