[FOM] Is the derivability sign a metalinguistic sign?

[Giordani Alessandro]

Dear Fomers,

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. In this case, the relata should be metalinguistic signs as well. But in a simple derivation like this:

	|- 0 = 0

the string of signs on the right is a linguistic one, isn't it? Actually, "0 = 0" is an element of the language and the name just written is a metalinguistic name for that object. Thus, we have a matalinguistic string consisting in a metalinguistic relation sign and a linguistic string. Is it possible?

Alessandro Giordani & Ciro De Florio