2026-05-02

2026-05-01←前　次→2026-05-03

GW ゲームのセール情報 2026

この本，めちゃくちゃ面白そう．論理の多元論に反対して，唯一の「正しい」論理が存在するという一元論を擁護する．論理体系「について」推論する際のメタ論理は多元的ではあり得ないのでは？という直観があるので，気になる．

PDF(一部): https://api.pageplace.de/preview/DT0400.9780192565242_A43448650/preview-9780192565242_A43448650.pdf

「論理体系「について」推論する際のメタ論理は多元的ではあり得ないのでは？という直観」って、古典論理上の集合論とマーティン・レーフの構成的型理論と縮約規則のない論理上の素朴集合論のどれかだけが正しいという直観なのだと解釈すると、16世紀の教会合同論みたいに聞こえてしまう件。

ChatGPT.icon

メタ論理の多元性に関する議論の整理

メタ論理

論理体系そのものを外側から評価する立場

無矛盾性・完全性などを議論する

問題の直観

「メタ論理は多元的ではあり得ない」

評価基準は1つに決まるはず

この直観の帰結

論理体系のうちどれか1つだけが正しい

古典論理 + 集合論

マーティン・レーフの型理論

縮約なし論理 + 素朴集合論

のどれかが唯一の正統になる

批判

これは構造的に

宗教の正統争いと同じ

比喩

16世紀の教会合同論

正しい教義を1つに決めようとする運動

背景にある現代的立場

論理体系は複数存在してよい

用途・意味によって使い分ける

例

古典論理 → 標準的数学

構成的論理 → 計算可能性

線形論理 → 資源管理

結論

「唯一のメタ論理がある」という直観は

多元性を否定し

宗教的な一元化と同じ構造を持つ

ChatGPT.iconhttps://chatgpt.com/share/69ff0b6a-9a84-83e9-8424-a3772bbe725b

Lean 4、排中律、選択原理

NyxFoundation

Lean入門動画を撮りました！

主に、数学の証明をプログラミングするという点に注目して解説しています。

ゴールデンウィークの暇な時にでもぜひ見てください！

banr1_

Coqに詳しい方から、実数の定義についてツッコミが入ったので補足します。

数学や定理証明支援系において、実数という概念はある種センシティブに扱われます。

Leanにおける実数の定義は、以下3つの公理に依存しています。

- 命題外延性 (propext)

- 商の公理 (Quot.sound)

- 選択原理 (Classical.choice)

Leanにおける主要な公理はこの3つのみであり、これら3公理から排中律(Classical.em)が導けます。

(ディアコネスクの定理)

選択原理は非常に強力な公理なので、これに依存するあらゆる概念は証明のみ可能であり、プログラムとして計算することは不可能

そういった整理になっています。