- 9 名前：前スレ969 [2012/01/02(月) 23:54:02.47 ]
- （ⅱ）PA|- ∀x〔(x+y=z→□[x+y=z])→(x+y=z→□[x+y=z])[Sx/x] 〕を示す
まず、以下のことに注意する。
/////////////////////////////////////////////
(x+y=z)[Sy/y] ≡ (x+y=z)[Sx/x]
よって、
□[x+y=z][Sy/y] ≡ □[x+y=z][Sx/x]
/////////////////////////////////////////////
これを踏まえた上で、
∀y∀z(x+y=z→□[x+y=z])|- ∀y∀z(x+y=z→□[x+y=z])[Sx/x] を示す
∀y∀z(x+y=z→□[x+y=z])|- (x+y=z)[Sy/y]→□[x+y=z][Sy/y]
|- (x+y=z)[Sx/x]→□[x+y=z][Sx/x]
≡ (x+y=z → □[x+y=z])[Sx/x]
したがって、（ⅰ）（ⅱ）と帰納法の公理より
PA|- x+y=z→□[x+y=z]
証明終わり
