邏輯和諧

邏輯和諧，由米高·達米特命名，是對可以用於給定的邏輯系統的推理規則的假定約束。

邏輯學家格哈德·根岑提議了邏輯連結詞的意義可以用把它們介入到論述中的規則給出。例如，如果你相信「天是藍的」並且還相信「草是綠的」，則你可以如下這樣介入邏輯連接詞「與」: 「天是藍的 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.