国立公園管理事務局
settings
狭義の有界量化子による帰納法と(広義の)有界量化子による帰納法は等価
帰納法図式
多項式帰納法図式
列長帰納法図式
Bounded Arithmetic, Propositional Logic, and Complexity Theory
鋭限定論理式
Tait計算
NuonはΣ₀論理式で定義可能. 帰納的性質はIΣ₀で証明可能
べき乗のグラフはΣ₀定義可能, 帰納的性質はIΣ₀で証明可能
第一不完全性定理の(計算論的)証明
Introduction to Game-Theoretic Probability
算術におけるメタ数学
PA⁻
Models of Peano Arithmetic
lean4-logic
many-sorted logic
Leanプロジェクト
Tait計算の完全性定理:統語論的主補題