Seeing Quantifier Scope: Quine’s Bond Notation

在一阶逻辑公式中，变量字母常被重复书写，用来标明哪些论元位置由同一个量词约束。例如，在 ∃x (P(x) ∧ R(x,y)) 中，两个 x 都由 ∃x 约束，而 y 是自由变量。

哲学家、逻辑学家蒯因（W. V. Quine）的 bond notation（连线记法）提供了另一种表示方式：保留量词，但不在受约束的位置重复写变量字母，而是用弧线将量词连接到它所约束的论元位置。绑定关系由连线表示，不必依靠相同的变量名。

Quine 在《数理逻辑》（Mathematical Logic, 1940）中介绍过这种量化图示，但认为它繁琐、实用性有限。但它的优点是更可视化、互动性更强，也有趣味性。我们做了一个 Quine 记号的交互式体验网页。欢迎大家探索和操作：

https://finalfantasy27.github.io/quine-bond-notation.html

一个例子是：

公式对应的连线效果：

下面是一个较复杂的公式。我的网页也提供彩色模式：

---

In first-order formulas, variable letters are often repeated to indicate which argument positions are bound by the same quantifier. For example, in ∃x (P(x) ∧ R(x,y)), both occurrences of x are bound by ∃x, while y is free.

The philosopher and logician W. V. Quine introduced bond notation as an alternative: quantifiers remain, but arcs connect them to the argument positions they bind, instead of repeating bound-variable letters at those positions. The binding relation is shown by the bonds rather than by repeated variable names.

Quine presented this kind of quantificational diagram in Mathematical Logic (1940), while judging it cumbersome and impractical. Its advantages, however, are visual clarity, interactivity, and a certain playfulness. We made an interactive page for exploring Quine’s notation. Give it a try:

https://finalfantasy27.github.io/quine-bond-notation.html

Here is a simple example:

The corresponding bond diagram:

Here is a more complex formula. The page also offers a color mode: