Post History
#3: Post edited
by
clemens
·
2026-03-29T18:05:55Z (6 months ago)
- 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 ).<sup>1</sup> E.g. whereas $\ulcorner P ∧ Q \urcorner$ stands for the literal statement "$P ∧ Q$", $\ulcorner \Psi ∧ \Phi \urcorner$ stands for 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-language<sup>2</sup>, 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}))$.)
- ---
- <sup>1</sup>My current source for this is [Mark Dominus's article](https://www.plover.com/misc/math/quasiquotes.html). It references Quine's *Mathematical Logic* (1940) for the convention of uppercase Greek letters.
- <sup>2</sup> 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}$.
- 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 ).<sup>1</sup> 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-language<sup>2</sup>, 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}))$.)
- ---
- <sup>1</sup>My current source for this is [Mark Dominus's article](https://www.plover.com/misc/math/quasiquotes.html). It references Quine's *Mathematical Logic* (1940) for the convention of uppercase Greek letters.
- <sup>2</sup> 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}$.
#2: Post edited
by
clemens
·
2026-03-29T18:04:13Z (6 months ago)
- 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 ).<sup>1</sup> E.g. whereas $\ulcorner P ∧ Q \urcorner$ stands for the literal statement "$P ∧ Q$", $\ulcorner \Psi ∧ \Phi \urcorner$ stands for . 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-language<sup>2</sup>, 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}))$.)
- ---
- <sup>1</sup>My current source for this is [Mark Dominus's article](https://www.plover.com/misc/math/quasiquotes.html). It references Quine's *Mathematical Logic* (1940) for the convention of uppercase Greek letters.
- <sup>2</sup> 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}$.
- 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 ).<sup>1</sup> E.g. whereas $\ulcorner P ∧ Q \urcorner$ stands for the literal statement "$P ∧ Q$", $\ulcorner \Psi ∧ \Phi \urcorner$ stands for 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-language<sup>2</sup>, 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}))$.)
- ---
- <sup>1</sup>My current source for this is [Mark Dominus's article](https://www.plover.com/misc/math/quasiquotes.html). It references Quine's *Mathematical Logic* (1940) for the convention of uppercase Greek letters.
- <sup>2</sup> 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}$.
#1: Initial revision
by
clemens
·
2026-03-25T21:52:16Z (6 months ago)
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 ).<sup>1</sup> E.g. whereas $\ulcorner P ∧ Q \urcorner$ stands for the literal statement "$P ∧ Q$", $\ulcorner \Psi ∧ \Phi \urcorner$ stands for . 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-language<sup>2</sup>, 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}))$.)
---
<sup>1</sup>My current source for this is [Mark Dominus's article](https://www.plover.com/misc/math/quasiquotes.html). It references Quine's *Mathematical Logic* (1940) for the convention of uppercase Greek letters.
<sup>2</sup> 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}$.