Quasi-quotation


Quasi-quotation or Quine quotation is a linguistic device in formal languages that facilitates rigorous and terse formulation of general rules about linguistic expressions while properly observing the use–mention distinction. It was introduced by the philosopher and logician Willard Van Orman Quine in his book Mathematical Logic, originally published in 1940. Put simply, quasi-quotation enables one to introduce symbols that stand for a linguistic expression in a given instance and are used as that linguistic expression in a different instance.
For example, one can use quasi-quotation to illustrate an instance of substitutional quantification, like the following:
Quasi-quotation is used to indicate that the φ and "φ" in this sentence are related things, that one is the iteration of the other in a metalanguage. Quine introduced quasiquotes because he wished to avoid the use of variables, and work only with closed sentences. However, he still needed to be able to talk about sentences with arbitrary predicates in them, and thus, the quasiquotes provided the mechanism to make such statements. Quine had hoped that, by avoiding variables and schemata, he would minimize confusion for the readers, as well as staying closer to the language that mathematicians actually use.
Quasi-quotation is sometimes denoted using the symbols ⌜ and ⌝, or double square brackets, ⟦ ⟧, instead of ordinary quotation marks.

How it works

Quasi-quotation is particularly useful for stating formation rules for formal languages. Suppose, for example, that one wants to define the well-formed formulas of a new formal language, L, with only a single logical operation, negation, via the following recursive definition:
  1. Any lowercase Roman letter is a well-formed formula of L.
  2. If φ is a well-formed formula of L, then '~φ' is a well-formed formula of L.
  3. Nothing else is a well-formed formula of L.
Interpreted literally, rule 2 does not express what is apparently intended. For '~φ' is not a well-formed formula of L, because no Greek letter can occur in well-formed formulas, according to the apparently intended meaning of the rules. In other words, our second rule says "If some sequence of symbols φ is a well-formed formula of L, then the sequence of 2 symbols '~φ' is a well-formed formula of L". Rule 2 needs to be changed so that the second occurrence of 'φ' be not taken literally.
Quasi-quotation is introduced as shorthand to capture the fact that what the formula expresses isn't precisely quotation, but instead something about the concatenation of symbols. Our replacement for rule 2 using quasi-quotation looks like this:
The quasi-quotation marks '⌜' and '⌝' are interpreted as follows. Where 'φ' denotes a well-formed formula of L, '⌜~φ⌝' denotes the result of concatenating '~' and the well-formed formula denoted by 'φ'. Thus rule 2' entails, e.g., that if 'p' is a well-formed formula of L, then '~p' is a well-formed formula of L.
Similarly, we could not define a language with disjunction by adding this rule:
But instead:
The quasi-quotation marks here are interpreted just the same. Where 'φ' and 'ψ' denote well-formed formulas of L, '⌜⌝' denotes the result of concatenating left parenthesis, the well-formed formula denoted by 'φ', space, 'v', space, the well-formed formula denoted by 'ψ', and right parenthesis. Just as before, rule 2.5' entails, e.g., that if 'p' and 'q' are well-formed formulas of L, then is a well-formed formula of L''.

Scope issues

It does not make sense to quantify into quasi-quoted contexts using variables that range over things other than character strings. Suppose, for example, that one wants to express the idea that 's denotes the successor of 0, s' denotes the successor of 1, etc. One might be tempted to say:
Suppose, for example, φ = 7. What is ⌜s⌝ in this case? The following tentative interpretations would all be equally absurd:
  1. ⌜s⌝ = 's',
  2. ⌜s⌝ = 's',
  3. ⌜s⌝ = 's',
  4. ⌜s⌝ = 's',
  5. ⌜s⌝ = 's',
  6. ⌜s⌝ = 's'.
On the other hand, if φ = '7', then ⌜s⌝ = 's', and if φ = 'seven', then ⌜s⌝ = 's'.
The expanded version of this statement reads as follows:
  • If φ is a natural number, then the result of concatenating 's', left parenthesis, φ, and right parenthesis denotes the successor of φ.
This is a category mistake, because a number is not the sort of thing that can be concatenated.
The proper way to state the principle is:
  • If φ is an Arabic numeral that denotes a natural number, then ⌜s⌝ denotes the successor of the number denoted by φ.
It is tempting to characterize quasi-quotation as a device that allows quantification into quoted contexts, but this is incorrect: quantifying into quoted contexts is always illegitimate. Rather, quasi-quotation is just a convenient shortcut for formulating ordinary quantified expressions—the kind that can be expressed in first-order logic.
As long as these considerations are taken into account, it is perfectly harmless to "abuse" the corner quote notation and simply use it whenever something like quotation is necessary but ordinary quotation is clearly not appropriate.