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. 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 (usually in more complex formulas) 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 (expressions not containing any variables). 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 ⌝ (unicode U+231C, U+231D), or double square brackets, ⟦ ⟧ ('Oxford brackets'), instead of ordinary quotation marks. Quasi-quotation is particularly useful for stating formation rules for formal languages. Suppose, for example, that one wants to define the well-formed formulas (wffs) of a new formal language, L, with only a single logical operation, negation, via the following recursive definition: Interpreted literally, rule 2 does not express what is apparently intended. For '~φ' (that is, the result of concatenating '~' and 'φ', in that order, from left to right) is not a wff of L, because no Greek letter can occur in wffs, according to the apparently intended meaning of the rules. In other words, our second rule says 'If some sequence of symbols φ (for example, the sequence of 3 symbols φ = '~~p') is a wff of L, then the sequence of 2 symbols '~φ' is a wff of L'. Rule 2 needs to be changed so that the second occurrence of 'φ' (in quotes) be not taken literally.