|
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 variables 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: ::"Snow is white" is true if and only if snow is white. ::Therefore, there is some sequence of symbols that makes the following sentence true when every instance of φ is replaced by that sequence of symbols: "φ" is true if and only if φ. 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. 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.〔Dowty, D., Wall, R. and Peters, S.: 1981, Introduction to Montague semantics, Springer.〕〔Scott, D. and Strachey, C.: 1971, Toward a mathematical semantics for computer languages, Oxford University Computing Laboratory, Programming Research Group.〕 == 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 (wffs) of a new formal language, ''L'', with only a single logical operation, negation, via the following recursive definition: # Any lowercase Roman letter (with or without subscripts) is a wff of ''L''. # If φ is a wff of ''L'', then '~φ' is a wff of ''L''. # Nothing else is a wff of ''L''. Interpreted literally, rule 2 does not express what is intended. For '~φ' (that is, the result of concatenating '~' and 'φ', in that order, from left to right) is not a wff of ''L'', because the Greek letter 'φ' is used as a metavariable and thus cannot occur in wffs. In other words, our second rule says "If ''the sequence of symbols'' φ is a wff of ''L'', then '~''the sequence of symbols'' φ' is a wff of ''L''". Because φ stands for a sequence of symbols instead of the proposition that the sequence might denote in the object language, φ isn't the kind of thing that can be negated. Rule one tells us that lowercase letters of the object language (such as 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: :2'. If φ is a wff of ''L'', then ⌜~φ⌝ is a wff of ''L''. The quasi-quotation marks '⌜' and '⌝' are interpreted as follows. Where 'φ' denotes a wff of ''L'', '⌜~φ⌝' denotes the result of concatenating '~' and ''the wff denoted by'' 'φ' (in that order, from left to right). Thus rule 2' (unlike rule 2) entails, e.g., that if Similarly, we could not define a language with disjunction by adding this rule: :2.5. If φ and ψ are wffs of ''L'', then '(φ v ψ)' is a wff of ''L''. But instead: :2.5'. If φ and ψ are wffs of ''L'', then ⌜(φ v ψ)⌝ is a wff of ''L''. The quasi-quotation marks here are interpreted just the same. Where 'φ' and 'ψ' denote wffs of ''L'', '⌜(φ v ψ)⌝' denotes the result of concatenating left parenthesis, the wff denoted by 'φ', space, 'v', space, the wff denoted by 'ψ', and right parenthesis (in that order, from left to right). Just as before, rule 2.5' (unlike rule 2.5) entails, e.g., that if 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Quasi-quotation」の詳細全文を読む スポンサード リンク
|