健全性とは？
けんぜんせい
健全性とは、ある論理体系において証明できる命題はすべて意味論的に真である、という性質のことです。
健全性（soundness）とは、形式的な論理体系における重要な性質の一つで、「その体系で証明可能なすべての命題は、意味論的にも妥当（真）である」ことを指します。証明可能性（統語論的な側面）と真であること（意味論的な側面）の整合性を保証する性質です。
形式的に述べると、論理体系Lにおいて「Lで⊢φが成り立つならば⊨φも成り立つ」ことが健全性です。ここで⊢は証明可能性を、⊨は意味論的妥当性（すべての解釈のもとで真）を表します。
健全性が保証されていない体系では、偽である命題を証明できてしまう可能性があり、その体系で導かれる結論が実際に正しいという保証がなくなります。逆に、健全な体系では証明が「信頼できる」ことが約束されます。
健全性と対をなす概念として完全性があります。完全性は「意味論的に真な命題はすべて証明できる」という性質で、健全性と完全性がともに成り立つ体系が最も望ましいとされます。古典命題論理や述語論理（一階述語論理）はどちらの性質も満たすことが知られています。
健全性の証明は、推論規則が意味論的に正しい操作であること、すなわち前提が真であれば結論も真になることを示すことで行われます。
使い方・例文
古典命題論理の体系において、「P∧Q → P」という推論規則はどんな解釈でも前提が真なら結論も真になるため、健全性を支える推論規則の一例です。健全性が保証されることで、形式的な証明を信頼して使えます。
この用語をシェア
最終更新: