完全性定理 意味
数学的に正確な概念「φはＴから証明できる」が定義できて，それが直観的な概念「φはＴから論理法則のみによって従う」を完全に捉えることができることを示そう．（中略）必要なことのすべては「φがＴから論理法則のみによって従う」とき，少なくとも次のことが成り立つことに同意するだけである：φがＴを充たす任意の構造で正しくなる（これをＴ|=φと書いたのだった（cf.1.3.9）．換言すれば，φやＴに含まれている概念・言葉を（論理的にではあるが）如何様に解釈しても，その解釈のもとでＴが正しければ必ずφも正しくなる，ということを意味する．
従って上の目標を達成するためには，正しい推論をいくつか抽出して，Ｔ|=φということと，φが仮定Ｔを伴った，これらの推論のみによる証明を有することが同値になることを言えばよい．
これが完全性定理の実際である．
（「数学基礎論」新井敏康著 p.36）
完全性定理の導入部が、あまりにも素晴らしすぎて鱗から目が落ちたので引用します。ここでＴは論理式の集合のことです。
完全性・健全性定理は、
Ｔ |= φ ⇔ Ｔ |- φ
と書かれ、
「φがＴの論理的帰結であることと、φがＴで証明可能であることは同値である」と読みます。左向き矢印が健全性で、右向き矢印が完全性、だと思います。ここでは「証明可能である」という概念と、「論理的帰結である」という概念とは別々に定義されています。論理的帰結のほうはすでに出てきた概念でしたな。
（一瞬復習）
Ｔ |= φ （φはＴの論理的帰結である・φはＴの定理である）
とは、１階述語論理では、Ｔの任意のモデルが論理式φの全称閉包を充たすこととして定義されたのでした。モデルとは論理式を解釈する集合のことだったので、論理的帰結とはφをどのように解釈してもＴが真になるような解釈なら、φも真になる、ということになるわけですね。
（一瞬復習終わり）
健全性って何が健全なのっと
夜遊びしないとか、エッチな漫画を読まないとかそういう健全ではないみたいです。「証明可能である」という概念が健全に機能していますよ、ということだとぼくは理解しています。証明体系Ｈをいくつかの公理と推論規則のセットで定義して、「φのＴからの証明」を論理式の有限列として定義します。この時に、もしも証明体系の定義がうまくいかなくって、極端な話、「φが証明体系Ｈで証明できたんだけど、実は¬φがトートロジーだと判明して、φは任意のモデルで真じゃなかったんだけど何か質問ある？」みたいなことが起こっては困ります。
そこで、「証明可能である」という概念にはいろいろな定義がありえるだろうけど、仮定Ｔから証明可能な論理式については、Ｔのモデルで真であってほしいですよね。これが健全な「証明」の概念でしょう、ということだと思います。
