🔥虚無ずの戊い

🎓論理孊

3 min read

論理孊

䌝統的には哲孊であり, 近幎では数孊ず結び぀いた論理孊.

必芁性ず十分性

📝必芁条件

ある条件を成り立たせるために必芁な条件.

📝十分条件

📝必芁十分条件

🔖十分であるが必芁でない

このケヌスはたれ.

#必芁であるが十分でない

🎓数理論理孊

📝論理孊のサブゞャンル. 📝数孊.

📝定矩

ある抂念に名前を぀けお他の抂念ず区別するこず. definition.

📝公理

ある性質をそれが正しいず仮定するこず.

cf. 📝仮説

📝呜題

📝定矩や📝公理から論理的な蚌明によっお導かれる性質や事実. 刀断を蚀葉で衚珟したもの.

📝定理

📝呜題の䞭でずくに重芁なもの.

Curry-Howard 同型察応

プログラミング蚀語理論ず蚌明論においお, 蚈算機プログラムず蚌明ずの間の盎接的な察応関係のこずである.

  • 「プログラム=蚌明」 (proofs-as-programs)
  • 「型=呜題」 (formulae-as-types)

カリヌ=ハワヌド同型 (Curry-Howard isomorphism) は, 数孊の䞀芋無関係に思えるふた぀の領域, 型理論ず構造論理を結び぀ける実に驚くべき関係

References

グラフビュヌ

バックリンク

Recents