健全性

論理学において、健全性とは、議論の性質、あるいは形式的演繹体系の性質のいずれかを指す場合がある。

議論が健全 であるのは、形式的に妥当であり、かつ誤った前提を持たない場合に限る。^{[ 1 ]}

形式体系が健全であるのは、その体系内で証明可能なすべての整形式式が、その体系の論理意味論に関して論理的に妥当である場合（かつその場合に限る）である。

これら二つの性質は異なるものの、密接に関連している。前者は入門的な演繹的推論の文脈により関連があり、後者はメタ論理学や数理論理学において現れる。

演繹的推論において、健全な議論とは、妥当であり、かつすべての前提が真である（したがって結論も真である）議論のことである。前提が真であると仮定すれば、結論が必ず真となる場合、その議論は妥当である。健全な議論の例として、次のよく知られた三段論法が挙げられる。

（敷地内）

全ての人間は死ぬ運命にある。

ソクラテスは男性である。

（結論）

したがって、ソクラテスは死ぬべき存在である。

結論が論理的に必然的であるため、この議論は妥当である。そして、議論が妥当であり、その前提が真であるため、この議論は健全である。

しかし、議論は正当でなくても妥当である場合がある。例えば：

すべての鳥は飛べる。

ペンギンは鳥類です。

したがって、ペンギンは飛ぶことができる。

この議論は、前提が真であると仮定すれば結論が真でなければならないため、妥当である。しかし、最初の前提は偽である。すべての鳥が飛べるわけではない（例えば、ペンギン）。議論が健全であるためには、議論が妥当であり、かつ前提が真でなければならない。^{[ 2 ]}

レモンなどの著者の中には、「健全性」という用語を、現在「妥当性」と同義語として使用した者もおり^{[ 3 ]}、そのため、現在「健全性」と呼ばれるものを表す特定の言葉がなかった。しかし今日では、このような用語の区分は非常に広く普及している。

数理論理学において、論理体系は、その体系で証明可能なすべての式が体系の意味論に関して論理的に妥当である場合に、健全性という性質を持つ。ほとんどの場合、これはその規則が真理を保持する性質を持つことに帰着する。^{[ 4 ]}健全性の反対は完全性として知られている。

構文的含意を持つ論理体系${\displaystyle \vdash }$そして意味的含意${\displaystyle \models }$任意のシーケンスに対して健全である${\displaystyle A_{1},A_{2},...,A_{n}}$その言語の文の場合、${\displaystyle A_{1},A_{2},...,A_{n}\vdash C}$、 それから${\displaystyle A_{1},A_{2},...,A_{n}\models C}$言い換えれば、その体系は、そのすべての定理が妥当である場合に健全である。

健全性は、数理論理学における最も基本的な性質の一つです。健全性という性質は、論理体系を望ましいものとみなす最初の理由となります。完全性とは、すべての妥当性（真理）が証明可能であることを意味します。これら二つを合わせると、すべての妥当性のみが証明可能であるという結論になります。

健全性の証明のほとんどは自明である。^{[ 5 ]}例えば、公理系では、健全性の証明は、公理の妥当性と推論規則が妥当性（またはより弱い性質である真理）を保持していることを検証することに等しい。システムがヒルベルト型の演繹を許容する場合、公理の妥当性と1つの推論規則、すなわちモーダス・ポネンス（および場合によっては置換）を検証するだけでよい。

健全性には大きく分けて弱健全性と強健性の2種類があり、前者は後者の限定された形態である。強健性とは本節で先に述べた定義であり、弱健全性とはこれを前提から証明できない文、つまりターンゲートの右側に文が存在しない文に限定したものである。

• 健全性（対話型証明）
• 型の健全性

• ヒンマン、P. (2005).数理論理学の基礎. AK Peters. ISBN 1-56881-262-0。
• コピ、アーヴィング（1979）『記号論理学』（第5 版）、マクミラン出版、ISBN 0-02-324880-7
• ブーロス、バージェス、ジェフリー。『計算可能性と論理』第4版、ケンブリッジ、2002年。

• インターネット哲学百科事典における妥当性と健全性。