is the computer a mathmatician?

この本を今読んでるので、わからなくて調べたこと、面白かったこと、感想を書いていく

自由変数

自由変数

固有変数条件についてあまり理解しなくてもいいと書かれていたが、そう言われると理解したくなるもので、定義だけだと確かによくわからなかったので調べてみた。

そこで自由変数と束縛変数の定義はわかるのだが、自由変数と$\forall$で束縛された変数の実用上の違いがよくわかっていない気がした。

京都大学の授業で使っているのか知らないが固有変数条件について説明しているwebページがあり、そこでの説明は良い気がした。

$\forall$導入を考えてみよう． 数学では「…という前提のもとで$\forall x .\phi(x)$が成立する」 という定理を証明するときに「$a$ を任意の…とする．このとき …（一連の推論が続く）…．ゆえに $\phi(a)$ が成立する」 という形の推論を行うのが普通である．自由変数 $a$ とは，要するに， このような証明を書き下すための「仮の変数」である．

$\forall$導入と$\exists$除去がどれくらい便利なのか、まだ体感できていない。 固有変数条件を見るとそこまで便利には見えない。なので使用例を見てみる。

このwebページには使用例も書いてあったので自分で証明図を書いた。

自由変数という仮の変数を使って$\forall$記号を使う論理式を証明している。

大雑把に言えば、$\forall$記号を使った論理式を証明体系で証明するのは難しい($\Pi_1$文の正しさを確かめるには無限の計算が必要だった)ので、この$\forall$導入が便利なのだろうと考えた。