• 国立公園管理事務局
  • settings
  • The Type Theory of Lean
  • FormalizedFormalLogic/Incompleteness
  • FormalizedFormalLogic/Arithmetization
  • FormalizedFormalLogic/Foundation
  • Σᵇ₀(Σᵇᵢ)-内包図式 (S₂)
  • S₂でnuon(x)はΔᵇ₁定義可能
  • 形式化された有限列（限定算術）
  • V.Sazonov, On Feasible Numbers
  • 帰納法図式
  • 多項式帰納法図式
  • 列長帰納法図式
  • Bounded Arithmetic, Propositional Logic, and Complexity Theory
  • 鋭限定論理式
  • Tait計算
  • NuonはΣ₀論理式で定義可能. 帰納的性質はIΣ₀で証明可能
  • べき乗のグラフはΣ₀定義可能, 帰納的性質はIΣ₀で証明可能
  • 第一不完全性定理の（計算論的）証明
  • 算術におけるメタ数学