1. Formal Languages

Geoffrey Hunter, Metalogic. An Introduction to the Metatheory of Standard First Order Logic, Berkeley and Los Angeles: University of California Press, 1996, pp. 3-6.

 

(1) truths of logic

(2) sentences used to express truths of logic

Notably, (1) and (2) are not the same; for two different sentences, e.g. one in French, one in English, might be used to express the same truths of logic.

Keeping the above distinction, the metatheory of logic is

(3) the theory of sentences-used-to-express-truths-of-logic

This is a definition of the metatheory of logic in a rough sense. However, the author points out that (3) may include both formal and informal languages.

In this book, the sentences-used-to-express-truths-of-logic must be formulas of a formal language, i.e. a 'language' that can be completely specified without any reference at all, direct or indirect, to the meaning of the formulas of the 'language.'

 

1. Formal Langugues

① The basic objects of meta theory are formal languages.

② The essential thing about a formal language is that, even if it is given an interpretation, it can be completely defined without reference to any interpretation for it: and it need not be given any interpretation. 

③ A formal language can be identified with the set of its well-formed formulas (also called formulas or wffs).

④ If the set of all wffs of a formal language L is exactly the same as the set of all wffs of a formal language L', then L is the same formal language as L'. If not, not.

⑤ A formula is an abstract thing. A token of a formula is a mark or a string of marks. Two different strings of marks may be tokens of the same formula. It is not necessary for the existence of a formula that there should be any tokens of it. (We want, for example, to speak of formal languages with infinitely many formulas.)

⑥ The set of well-formed formulas of a particular formal language is determined by a fiat of its creator, who simply lays down what things are to be wffs of his language.

특정한 형식 언어의 적형식의 집합은 그 창조자의 명령에 의해서 결정된다. 창조자는 무엇이 그의 언어의 적형식이 되어야 하는지를 단순히 규정하는 사람이다.

Usually he does this by specifying 

(1) a set of symbols (the alphabet of his language)
and
(2) a set of formation rules determining which sequences of symbols from his alphabet are wffs of his language. 

It must be possible to define both sets without any reference to interpretation: otherwise the language is not a formal language.

⑦ The word 'symbols' in the last paragraph is a technical term: symbols, in this technical sense of the word, need not be symbols of anything, and they must be capable of being specified without reference to any interpretation for them.

⑧ Symbols are abstract things, like formulas. A token of a symbol is a mark or configuartion of marks.

⑨ Roughly, a formal language is completely mastered by a suitable machine, without any understanding (this need quantification where the formal language has an uncountable alphabet: in such case it is not clear that the formal language could be completely mastered by anything.)

⑩ Given a particular formal language, we may go on to do either or both of the following things:

(1) we may define the notion of an interpretation of the language. This takes us into Model Theory.
(2) we may specify a deductive apparatus for the language. This takes us into Proof Theory. 

⑪

Terms	Meaning
A formal language	A certain type of language that can be completely defined without reference to any interpretation for it (even if it is given an interpretation).
Well-formed formulas (formulas or wffs)	What constitutes a formal language, which is determined by specifying a set of symbols and a set of formation rules
Symbols	The alphabet of a formal language. They must be capable of being specified without reference to any interpretation for them.
Formation rules	What determines which sequences of symbols from the alphabet are wffs of a formal language.
Model Theory	Defining the notion of an interpretation of the language.
Proof Theory	Specifying a deductive apparatus for the language.

1. Yes. Recall that a formal language can be identified with the set of its wffs. Here, wffs are determined by a set of symbols (Alphabet) with its formation rule.

2. No. A formal language can be completely defined without reference to any interpretation for it. However, the definition of formula of X involves essentially reference to meaning, since a thing is an English word only if it has a meaning.

3. No. In order to tell whether or not a string of symbols from the alphabet of Y you have to know whether or not it is an English word, and so whether or not it has a meaning.