論理的調和

論理的調和とは、マイケル・ダメットによって造られた名前であり、特定の論理体系で使用できる推論規則に対する想定される制約です。

論理学者ゲルハルト・ゲンツェンは、論理接続詞の意味は、それを談話に導入するための規則によって与えられると提唱した。例えば、空は青いと信じており、また草は緑色であると信じているなら、接続詞および を次のように導入できる。空は青い、そして、草は緑色である。 ゲンツェンの考えは、このような規則があることで、言葉、少なくとも特定の言葉に意味が与えられるというものである。この考えは、多くの場合、意味は使用であると言うことができるというウィトゲンシュタインの考えとも関連している。現代の論理学者の多くは、表現の導入規則と除去規則は同等に重要であると考える傾向がある。この場合、および は次の規則によって特徴付けられる。

これには明らかな問題があることがArthur Priorによって指摘されました。なぜ、導入規則が OR (「p」から「p tonk q」へ) で、除去規則が AND (「p tonk q」から「q」へ) である表現 (「 tonk 」と呼ぶ) ができないのでしょうか。これにより、任意の開始点から何でも推論できます。Prior は、これは推論規則では意味を決定できないことを意味すると示唆しました。Nuel Belnapは、導入規則と除去規則で意味を構成できるとしても、そのような規則の任意の組み合わせで意味のある表現が決定されるわけではなく、古い語彙で新しい真実を推論できないなど、特定の制約を満たす必要があると答えました。これらの制約こそ、ダメットが言及していたものです。

調和とは、証明システムが意味を持つために、言い換えれば、その推論規則が意味を構成するために、証明システム が導入規則と除去規則の間で保持する必要がある特定の制約を指します。

論理への調和の適用は特別なケースとみなすことができます。推論システムだけでなく、人間の認知における概念システムやプログラミング言語の型システムに関しても調和について語ることは理にかなっています。

この形式の意味論はタルスキの真理の意味論に概説されたものに対して大きな挑戦とはなっていないが、ルートヴィヒ・ヴィトゲンシュタインの意味は使用であるという考え方を尊重する方法で論理の意味論を再構築することに関心を持つ多くの哲学者は、調和が鍵を握っていると感じてきた。

• アーサー・プライアー、「ランナバウト推論チケット」。分析、21、pp.38-39、1960-61年。
• Nuel D. Belnap Jr.、「Tonk、Plonk、および Plink」、Analytics、22、130 ～ 134 ページ、1961 ～ 62 年。
• マイケル・ダメット『形而上学の論理的基礎』（ハーバード大学出版、1991年）

• Greg Restallの Proof and Consequence wikiの harmony (アーカイブ コピー、2012 年 7 月)