lean4-logic

lean4-logic copied to clipboard

chore: Update to v4.19.0 rc3 (FirstOrder)

1

なぜかメモリーリークが起きるので一旦保留．

iehality

Provable predicate should not depend on base theory

3

現状理論 `T` の可証性述語 `ProvabilityPredicate U T` はその性質を保証するベース理論である `U` にも依存しているが，可証性述語それ自体は `U` に依存しないのだから依存すべきでないと思う． ```lean structure ProvabilityPredicate (T : Theory L) where prov : Semisentence L 1 class HBL (T₀ : Theory L)...

iehality

SnO2WMaN

#240 と同じような理由で`Logic.S`を追加するとCI上でKiteの生成が壊れてしまう気がする．

SnO2WMaN

SnO2WMaN

SnO2WMaN

算術的完全性の諸々が終わったタイミングで作業に取り掛かった方が良いと思う．

SnO2WMaN

iehality

Pi_2-Sound is Sigma_1-Sound

1

算術的完全性においてPi_2 Soundnessを仮定しているが，これをSigma_1 Soundnessに直す（より一般的に示すことが可能？）

SnO2WMaN

Visserの定理（黒本 Thm 5.3.3） #304 のあとにマージする．

SnO2WMaN