>>92
では議論に資するだろうことを期待して、該当部分の引用をしてみる。
（引用にしてはちょっと長いかもしれないがフェアユースの範囲内でしょ）

５.形式証明の正しさ
　形式証明の正しさについてはヘールズの論文[7]に
概説されている。形式的論理体系の性質で重要なもの
に健全性と完全性がある。完全であるとは正しい命題
が必ず証明できる形式論理体系を意味する。今考えて
いるHOLは自然数を含むので、ゲーデルの不完全性
定理により完全ではない。健全性とは証明された定理
が必ず正しいことを保証するもので、矛盾を導かない
ことである。健全性は、一般にはモデルを与えること
で保証できる。すなわち、形式体系の記号にモデルの
対象や操作を結びつけ、すべての公理と推論がモデル
で成立することを示す。矛盾のないモデルを持つ形式
体系は無矛盾である。…

ヘールズの論文[7]というのはT.Hales. "Developments in formal proofs",2014.のこと