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
|