昨日の記事「述語論理とインデックス付き圏と限量随伴性」で、述語論理のモデルの基本事項を述べたので、これを元にして、個別の話をチョビチョビしていくことにします。 自然演繹の悪口を書いた記事「自然演繹はちっとも自然じゃない -- 圏論による再考」で述語論理は扱わなかったので、自然演繹における「∀導入規則」について詮索(むしろダメ出し)します。 内容: 全称記号の導入と除去の規則 証明ボックスを使った図示 チャンとした∀導入の方法 シーケントによるリーズニング記述 全称限量随伴性と∀導入リーズニング規則 全称記号の導入と除去の規則 自然演繹の推論規則(の図)で、全称記号'∀'の導入(introduction)と除去(elimination)は次のような形です。 P -------[∀導入] ∀x.P ∀x.P ----------[∀除去] P[x:=t] まー、見た目は簡単です。「自然演繹はち
自然演繹は、その名の通りに「自然で分かりやすい」と言われたりします。僕は、そうは思いません。むしろ「不自然で分かりにくい」と感じます。導入規則と除去規則のあいだに綺麗な対称性がある、と言う人がいます。僕にはどこが綺麗か分かりません。無理クリに対称に見せてるだけで、むしろ歪んでいて汚ないじゃないか、と思います。 自然かどうか、綺麗かどうかは主観の問題ですから、議論しても不毛です。しかし、代替の定式化を示して、それを自然演繹と比較することにより、自然演繹を相対化することは出来ます。やってみます。 この記事の内容は、ここ10年くらい思っていたことです。口頭でしゃべったことはありますが(最後の節を参照)、まとまった記述はなかったので、割と丁寧に書きました。その結果、けっこう長大な記事となりました。 論理や圏論を学ぶには、まっとうな教科書を手元に置くのがよいでしょう。その教科書が主治医とするなら、僕
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く