雑記

雑記

現在広く数学で採用されている基礎論は論理主義であり、少ない論理記号といくつかの記号を用いられて集合論が形成され、その上で数学が行われる理論です。この場合は、集合そのものや、集合同士の関係などが重要であり、集合の名前や数学概念の名前などは重要ではありません。

直観主義というと、名前からだけでは他の理論と比べて厳密に議論してない感じがします。
直観主義と呼ばれるのは、ひとつひとつの数学の概念に対し型と呼ばれるラベルを付与していることが特徴的だからです。

例えば群なら群という型、自然数なら自然数という型が必要になります。
論理主義と異なり、数学の理論が積み上げれば積み上がるほど型がどんどん増えていきます。

※結局論理主義と論理主義は等価だというのをどこかで見た気がします。

Lean4

ここでは最近リリースされた直観主義に根ざしたプログラミング言語LEAN4のプログラム例を紹介してみます。

      theorem ex1 : p ∨ q → q ∨ p := by {
  intro h;
  cases h;
  case inr => {
    apply Or.inl;
    assumption;
  }
  case inl => {
    apply Or.inr;
    assumption;
  }
}

    

intro h;

p q : Prop
h : p ∨ q
⊢ q ∨ p

cases h;

case inl
p q : Prop
 : p
⊢ q ∨ p
case inr
p q : Prop
 : q
⊢ q ∨ p

case inr => {
    apply Or.inl;
    assumption;
}

goals accomplished

case inl => {
    apply Or.inr;
    assumption;
}

goals accomplished

goals accomplished