練習問題 3.2.7

本文では，等式

P(n)

がすべての擬数

に対して成り立てば

P(infinity)

も成り立つと主張している．

中のすべての自由変数は全称限量されていなければならない．たとえば，以下の2つはどちらを

P(n)

としても成り立つ．

 すべての x および m に対して  x↑(m + n)   =  (x↑m) * (x↑n)
 すべての$m$に対して           (m + n) - n  =  m

一般には等式

P(n)

に存在限量された変数を含められない．しかしながら，たとえば，以下のように定義された命題

P(n)

を考える．

ある有限数 m が存在して n `ominus` m = ⊥

ここで，

`ominus`

は減算の全域版であり，

n < m

ならば

n `ominus` m= Zero

である．帰納法を用いて

P(n)

が任意の擬数

に対して成り立つことを示せ．さらに，帰納法により，

infinity `ominus` m = infinity

が任意の有限数

について成り立つことを証明せよ．

⊥の場合
    ⊥ `ominus` m
=   { ominus の定義．場合の枯渇 }
    ⊥
    この場合は任意の有限 m についてP(n)が成り立つ．
Succ n の場合
    帰納法の仮定より∃m : n `ominus` m = ⊥
    Succ n `ominus` Succ m
=   { ominus の定義 }
    n `ominus` m
=   { 帰納法の仮定 }
    ⊥

infinity `ominus` m = infinity

は

上の帰納法による

Zeroの場合
    infinity `ominus` Zero
=   { ominusの定義 }
    infinity

Succ n の場合
    infinity `ominus` Succ n
=   { infinityの定義 }
    Succ infinity `ominus` Succ n
=   { ominusの定義 }
    infinity `ominus` n
=   { 帰納法の仮定 }
    infinity

IFPH — 練習問題 3.2.7

練習問題 3.2.7