Quotation notation in mathematics
In mathematics it is very often necessary to distinguish between an expression and its referent, as we do in English with quotation marks. For instance, we'd like to say that any statement of the form "$P ∧ Q$" entails "$P$" and "$Q$".
Are there any customary "mathematical quotation marks" that allow this? I looked in some books on model theory and logic I happened to have on hand (e.g. Cohen (1963) and Yasuhara (1971)) but haven't found anything (Rosser (1969) sometimes uses regular quotation marks, but I don't think that's typical).
(Incidentally, it seems as though what's needed is more a form of "quasiquotation" (as done in Lisp) than regular quotation, as saying that "$P∧Q$" entails "$P$" is useless if there isn't an understanding that "$P$" and "$Q$" are placeholders for arbitrary expressions.)
1 answer
Apparently the punctuation marks $\ulcorner \urcorner$, known as Quine corners, are sometimes used to denote quotation.
They're particularly good in the use case in the OP because Quine adopted a quasiquotation convention where uppercase Greek letters stood for variables in the meta-language (other letters stood for constants or variables in the object ).1 E.g. whereas $\ulcorner P ∧ Q \urcorner$ stands for the literal statement "$P ∧ Q$", $\ulcorner \Psi ∧ \Phi \urcorner$ stands for what you get when you replace $\Psi$ and $\Phi$ by their values in the statement "$\Psi ∧ \Phi$" (in this particular case you get the conjunction of the statements $\Psi$ and $\Phi$).
So one can quite conveniently write meta-language statements like $\forall \Psi \forall \Phi ((\ulcorner \Psi ∧ \Phi \urcorner \text{ is true}) \Rightarrow (\ulcorner \Psi \urcorner \text{ is true} ∧ \ulcorner \Phi \urcorner \text{ is true}))$ to express that a conjunction entails its conjuncts!
It'd be interesting to know if there are any other notations out there for mathematical quasiquotation. Quine's uppercase-Greek-letter convention is nice but unfortunately still ambiguous when we want to refer to functions in the meta-language2, which is needed for e.g. precisely specifying the axioms of quantifier logic (e.g. universal instantiation: $\forall \Psi \forall \Theta \forall \Phi (\ulcorner \forall \Theta \Psi(\Theta) \urcorner \text{ is true} \Rightarrow (\ulcorner \Psi(\Phi) \urcorner \text{is true}))$.)
1My current source for this is Mark Dominus's article. It references Quine's Mathematical Logic (1940) for the convention of uppercase Greek letters.
2 I.e. it's unclear whether an expression like $\ulcorner\Psi(\Phi)\urcorner$ means "the expression denoting the application of the object-level function denoted by the expression $\Psi$ to the object-level value denoted by the expression $\Phi$" or "the result of applying the meta-level function $\Psi$ to the expression $\Phi$". That being said, this difficulty can be resolved if the type of the meta-language variables $\Psi$ and $\Phi$ is explicitly specified. E.g. the first interpretation ($\Psi$ as denoting a function in the object-language) works if we type our variables like $\Phi: \text{Expr}, \Psi: \text{Expr}$; the second interpretation ($\Psi$ as being a function in the meta-language) works if we type our variables like $\Phi: \text{Expr}, \Psi: \text{Expr → Expr}$.
0 comment threads
0 comment threads