健全性と完全性
いつも忘れるwint.icon
2つ合せても完全性と呼ぶ
つまり部分は狭義の完全性である。
ぶっちゃけ やめてほしい wint.icon
健全性: 証明できる ⇒ 正しい（モデルがあり、その すべてで…）
soundness: $ \Gamma \vdash T \implies \Gamma \models T
完全性: 正しい（モデルがあり、その すべててで…）⇒ 証明できる
completeness: $ \Gamma \models T \implies \Gamma \vdash T
番外編
（形式）数学: 理論の完全性（aka. 否定完全性） $ \forall\varphi\,(\Gamma \vdash \varphi \;\text{ or }\; \Gamma \vdash \neg{\varphi})
健全性との対比ではない。
健全性: 型チェックが通る ⇒ 正しい
vs. 不健全: 型チェックが通ったからと言って、実行時（型）エラーが起きないとは限らない
完全性: 正しい ⇒ 型チェックが通る
大抵は求めない。
てか使わない？
cf. 正当性
en: correctness
ざつにやると停止性問題にぶちあたる。
ref
構文論的完全性