逻辑和谐

逻辑和谐，由迈克尔·达米特命名，是对可以用于给定的逻辑系统的推理规则的假定约束。

逻辑学家格哈德·根岑提议了逻辑连结词的意义可以用把它们介入到论述中的规则给出。例如，如果你相信“天是蓝的”并且还相信“草是绿的”，则你可以如下这样介入逻辑连接词“与”: “天是蓝的 AND 草是绿的”。Gentzen 的想法是拥有这样的规则就是对你的词语，至少对特定词语的给出意义的东西。这个想法也关联于维特根斯坦的格言，在很多情况下我们可以说意义是使用。多数当代逻辑学家偏好认为介入规则和除去规则对于表达是同等重要的。在这种情况下，“与”被如下规则所特征化:

介入:	除去:
p q	p and q	p and q
……	……	……
p and q	p	q

Arthur Prior 指出了它的一个明显的问题: 为什么不能有一个表达(称它为"tonk")，它的介入规则是 OR 形式的(从 "p" 到 "p tonk q") 而它的除去规则是 AND 形式的(从 "p tonk q" 到 "q")? 这让我们根本上从任何起点演绎任何东西。Prior 建议这意味着推理规则不能确定意义。Nuel Belnap 回答说，即使介入和除去规则不能建立意义，任何一对这种规则不能确定一个有意义的表达--它们必须满足特定约束，比如不允许我们在旧的词汇表中演绎出任何新真理。这种约束就是 Dummett 所提及的。

和谐指称的是一个证明论必须使其在介入和除去规则之间成立的特定约束，这样它才有意义，换句话说，它的推理规则是有意义建立的。

把和谐应用于逻辑可以被当作是一种特殊情况；谈论和谐不只有关推理系统才有意义，还有在人类认知中的概念系统，和编程语言中的类型系统。

这种形式的语义没有被证实对塔斯基的真理的语义理论形成巨大的挑战，但是很多哲学家感兴趣于用维特根斯坦的"意义是使用"的方式重建逻辑的语义，他们认为和谐是关键。

外部链接

• Harmony at Greg Restall's Proof and Consequence wiki

引用

Prior, Arthur. "The runabout inference ticket." Analysis, 21, pp38-39, 1960-61.

Belnap, Nuel D. Jr. "Tonk, Plonk, and Plink", Analysis, 22, pp130-134, 1961-62.