16/06/04 19:48:34.23 CtkyGlEO.net
>>372
直観論理
URLﾘﾝｸ(ja.wikipedia.org)
直観論理
(抜粋)
直観主義論理の色々な意味論が研究されている。ひとつの意味論は古典的なブール代数値意味論を写しとったものでブール代数の代わりにハイティング代数を用いる。別の意味論ではクリプキ・モデルを用いる。
直観主義論理は実際的な有用性を持つ。何故ならばこの制限によって存在具体性を持つ証明が作られるからであり、これは直観主義論理が数学的構成主義のある形態として適当なものとする。
非正式には、ある対象が存在することの構成的証明があれば、その構成的証明はそのような対象の例を生成するアルゴリズムとして使える、ということを意味する。
形式化された直観主義論理はアレン・ハイティングによってヤン・ブラウワーの直観主義プログラムの形式的な基礎として発展せられたものである。
目次
1 構文論と証明体系
1.1 シークエント計算
1.2 ヒルベルト流の計算
1.2.1 オプションの結合子
1.2.1.1 否定
1.2.1.2 同値
1.2.2 古典論理との関係
1.3 結合子の定義不可能性
2 意味論
2.1 ハイティング代数意味論
2.2 クリプキ意味論
2.3 タルスキ流のモデル論
2.4 他の論理との関係
2.4.1 多値論理との関係
2.4.2 中間論理との関係
2.4.3 様相論理との関係
2.5 ラムダ計算
3 関連項目
4 注釈
5 参考文献
6 外部リンク