- 6 名前：前スレ969 [2012/01/02(月) 23:53:05.11 ]
- 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]
証明終わり
