意味論的に真である命題は形式的に証明できる

論理式\varphi(X_1,\cdots,X_n)がトートロジーならば、証明可能である

逆に

完全な型推論を持つコンパイラは、正しいプログラムであるならば、型が推定できると保証される

と言えるのか

型理論の文脈では

型エラーがあれば、バグが絶対にある

不正な動作をしないプログラムは、型検査を通過する

健全性の逆

内容的に正しい判断は全て導出できる

成り立つ命題は証明できる

ゲンツェンの自然演繹(NK)では、完全性定理が成り立つ

参考

型以外の具体例あり