- 310 名前：１３２人目の素数さん mailto:sage [2012/02/03(金) 21:58:56.39 ]
- F[t/x]
Fの自由変数xにtを代入した論理式を表す
１、PA|- x=y→□[x=y]
証明
PA,x=y|- □[x=y] を示せばよい。すなわち
PA,x=y|- □[x=y][x/y]
|- □[x=y [x/y]]
|- □[x=x]
を示せばよい。
公理より、PA|-x=x
これにD1を適用すると、
PA|- □[x=x]
したがって、
PA,x=y|- □[x=y]
すなわち、
PA|- x=y→□[x=y]
証明終わり
