1 健全性の基本概念
1.1 用語の定義と直観
健全性とは、ある推論・判断・体系が、入力された前提や採用された規則に従った結果として生じる結論が、誤りを不適切に増幅しないという性質を指す。形式的には「その体系が導く任意の結論が、所定の意味で正しい（真である、正当化される等）」といった普遍量化の形で表される。直観的には、推論の手続きが“間違ったものを正しいとみなすように働かない”という期待を、論理的な条件として固定した概念である。
1.2 関連概念との区別
健全性は、しばしば「悪い結論が出てこない」ことに焦点を当てる。一方で、体系の望ましい性質は健全性以外にも存在し、導出可能性、比較可能性、頑健性など多様な観点から評価される。そのため、健全性は“正しさの保証”として理解されつつ、別の性質との役割分担を明確にする必要がある。
1.2.1 完全性との関係
完全性は、健全性とは対称的な方向で捉えられることが多い。すなわち、健全性が「導けるものは正しい」ことを保証するなら、完全性は「正しいものは導ける」ことを主張する。両者が揃うと、形式体系が持つ表現力と推論手続きの組合せが、対象に関する真理観と一致する度合いが高まる。もっとも、体系によっては片方のみ成立し、あるいは成立条件が限定される場合もある。
1.2.2 健全性と健全性（整合性）に似た用語
「整合性」は一般に、体系が自己矛盾を生まないことを指す。形式的には、ある文が同時にその否定も証明できない（あるいは“偽”が導出できない）といった形で定義されることが多い。整合性は“体系内で論理的に破綻しない”という観点に近いが、健全性のように意味（真理）と対応する形での保証とは一致しないことがある。両者は実務上混同されやすいが、健全性は「意味に照らして誤った結論が出ない」点で、整合性は「内部的な矛盾が生じない」点で主たる焦点が異なる。
1.3 射程（何に対する健全性か）
健全性を問う対象は一つに限られない。たとえば、(1) 推論規則が与えられた前提から導出する妥当性、(2) 公理系や証明体系がどの文を証明できるか、(3) 知識や正当化の理論が認識上信頼できる根拠の枠を与えているか、といった具合に異なる層で定式化される。さらに、何を「正しい」と呼ぶか（真理、正当化、望ましさ、情報保存など）も射程に直結する。したがって評価は、まず対象を特定し、その対象に対応する正しさ基準を定めるところから始まる。
2 形式論理・形式体系における健全性
2.1 推論規則の健全性
推論規則の健全性は、規則が前提の真偽や意味論的性質を損なわず、導出される結論が前提が満たす条件を引き継ぐことを意味する。典型的には、前提がすべて真であるなら結論も真となる、という含意の形で要求される。ここでの“真”は、体系に与えられた解釈（意味論）に依存する。
2.1.1 妥当性・保存性の見方
推論規則を、ある性質の保存として捉える見方がある。たとえば、前提が満たす性質を結論が保持していることを示せれば、規則は健全である。保存性は、局所的には規則ごとの検証に使いやすく、健全性が「各適用のたびに誤りが混入しない」ことに対応する。
2.1.1.1 具体例：単純な推論規則の点検
例として、含意除去に類する形の規則を考える。前提として「A」および「AからBが従う」という情報が与えられ、そのもとで「B」を結論として採用する規則があるとする。この規則が健全であるためには、意味論上でAが真かつA→Bが真ならBも真になることを確認する必要がある。これは、真理表や解釈の定義に沿って、前提同時充足が結論同時充足を必ず引き起こすかを点検する作業に相当する。規則が要求を満たさない場合、前提が真でも結論が偽になる解釈が存在し、健全性は破れる。
2.2 公理系・証明体系の健全性
公理系や証明体系の健全性は、個々の規則ではなく「体系全体が導出するもの」に焦点を当てる。通常、意味論的に真でない文が証明されるなら健全性は否定される。従って検証では、証明の形式（どの規則をどの順序で用いるか）に関わらず、任意の導出結果が真に対応することを示すことが目標となる。
2.2.1 意味論（真理）との対応
健全性を議論するには、導出される構文（文、式）と、解釈における真理条件を結びつける仕組みが必要である。意味論（モデル）を指定すると、各文がどの意味で真と評価されるかが定まり、健全性は「証明可能性から真理への含意」によって表現される。
2.2.1.1 構文と意味の接続
構文と意味の接続は、解釈関数や充足関係として与えられる。具体的には、変数割当や構造が与えられたときに、式が真になる条件を定義することで、証明手続きが作り出す合成構造が意味的に正しいことを追跡できるようになる。健全性の主張は、構文的な導出系列が意味的な満足条件を決して壊さないことの保証として整理される。
2.3 健全性の証明方法
健全性の証明には、意味論的性質と証明理論的構造との橋渡しを行う手段が用いられる。代表的には、帰納的な検証やモデル論的な証明がある。どちらも「局所的に正しい操作が積み重なっても全体として誤りが入らない」ことを、論理学的に確かめる。
2.3.1 帰納的検証
帰納的検証では、導出の長さや適用回数に関する帰納法を用いる。基底部では、公理（初期式）が意味論的に真であることを示す。次に、帰納仮定として、ある時点までの導出結果がすべて真であると仮定し、そこに健全な推論規則を適用したとき結論が真であることを確かめる。各ステップで正しさが保持される限り、最後の導出結果も真になるため、体系の健全性が従う。
2.3.2 モデル論的手法
モデル論的手法は、反例構成に近い形で進むことが多い。すなわち、もし健全性が破れているなら、真理条件を満たす解釈の下で結論だけが偽になる状況が存在するはずである、と仮定する。そこから、証明された文が満足関係に従うべきという要請に反する矛盾を導いて、健全性の主張を確かめる。モデル論的な観点は、意味論の定義と密接であり、対象理論の性質（充足可能性や反モデルの構成可能性）に依存する。
3 認識論における健全性
3.1 知識・正当化の枠組みとしての健全性
認識論での健全性は、知識や正当化の理論が「信頼できる基盤に基づく推論を通じて、誤りの混入を体系的に避ける」かどうかという問題として現れる。ここで重要なのは、論理学的な形式的真理だけでなく、“正当化の基準”がどの程度、対象世界に対する誤導を抑えるかである。枠組みが健全であるとは、正当とみなされた主張が、適切な条件下で実際にも正しい方向へ結びつくという保証があることを意味する。
3.2 推論手続きの信頼性
推論手続きの信頼性は、認識行為における手続きが、誤った情報を選別する能力をどれほど備えているかに関わる。たとえば、証拠の扱い、推論規則の採用、根拠の更新の仕方などが、誤差を増やす構造になっていないかが問われる。健全性の観点からは、手続きがどの仮定の下で妥当な更新を行い、どの条件で逸脱する可能性が生じるかを境界づけることが中心課題となる。
3.3 反例と境界条件
健全性が成立しない場合、典型的には「想定していないタイプの入力」や「推論の前提が崩れる状況」が原因となる。従って単に“成否”だけでなく、どのような条件なら健全性が保たれ、どの領域では保証が弱まるのかを明確にする必要がある。
3.3.1 「常に正しい」と言えない場合の扱い
認識論では、絶対的な正しさを無条件に要求すると成立条件が厳しすぎることがある。そのため現実的には、「ある種類の状況では誤りを増幅しない」といった条件付きの健全性が検討される。例えば、情報源の信頼性が一定以上である、推論規則の適用範囲が限定されている、などの条件が満たされるときに健全性を主張する形になる。これにより、無限の一般性を捨てつつも、実務上の信頼度を評価できる。
4 実践的応用と評価
4.1 証明支援・検証における健全性
証明支援環境やソフトウェア検証では、健全性は「証明されたという主張が、仕様や意味に照らして外れていない」ことを意味する。形式的な証明器が生成する導出が、モデル上で成立する性質に対応しているなら、検証結果は信頼できる。逆に健全性が欠けると、検証済みと見なして導入したシステムが、意図した性質を実際には満たさない危険が生じる。実務では、核となる推論規則や公理だけでなく、基盤ライブラリや形式化の対応づけ部分も含めた信頼性の設計が求められる。
4.2 倫理・安全設計への含意（誤り削減の観点）
安全設計において健全性は、誤りの発生確率をゼロにするというより、誤った判断の連鎖を抑える方向で寄与する。形式手続きが健全であれば、検出済みとされる異常が、意味上の要請を満たさない形で“見逃されにくくなる”。この効果は、ヒトが行う推論や運用判断にも波及しうる。特に、監査可能な証拠形式を用いる場合には、誤った結論が内部で増殖しない構造を作れるため、責任分界の観点でも利点がある。
4.3 健全性評価の手順テンプレート
健全性を評価する作業は、対象の定義と対応づけの明確化から始まる。次に、どの操作が健全性を損なう可能性を持つかを洗い出し、それらが要求条件を満たすかを検証する。最後に、健全性の主張が成り立つ範囲を明示し、境界を越えたときの扱いを記録するのが実務上有用である。
4.3.1 対象の特定と仕様化
まず「何が健全性の対象か」を列挙する。たとえば推論規則、証明体系、知識モデル、評価関数などであり、対象に応じて“正しい”の定義が変わる。次に仕様化として、入力・出力の形式、採用する意味（真理条件や正当化条件）、例外や前提の置き方を文書化する。ここでの曖昧さは、後続の検証を無意味にするため、評価者が誤解しない粒度で記述することが重要となる。