20/04/23 20:10:37 zY/+UvEc.net
>>141
1、P0∧∀x(Px→Psx)→∀xPx ・・・数学的帰納法
2、P0∧∃x¬Px ・・・仮定
3、∀x(Px→Psx) ・・・仮定
4、P0 ・・・2より∧除去
5、P0∧∀x(Px→Psx) ・・・4と3より∧導入
6、∀xPx ・・・1と5より→除去
7、Pa ・・・6より全称例示仮
8、∃xPx ・・・7より存在汎化
9、∃x¬Px ・・・2より∧除去
10、矛盾 ・・・8と9より矛盾導入
11、¬∀x(Px→Psx) ・・・3より¬導入
12、¬∃x(Px∧¬Psx) ・・・仮定
13、Pa∧¬Psa ・・・仮定
14、∃x(Px∧¬Psx) ・・・13より存在汎化
15、矛盾 ・・・12と14より矛盾導入
16、¬(Pa∧¬Psa) ・・・15と13より¬導入
17、Pa→Psa ・・・16より
18、∀x(Px→Psx) ・・・17より全称汎化
19、矛盾 ・・・17と11より
20、∃x(Px∧¬Psx) ・・・12と19より¬導入と二重否定除去
21、(P0∧∃x¬Px)→∃x(Px∧¬Psx) ・・・2と20より→導入
22、{P0∧∀x(Px→Psx)→∀xPx}→{(P0∧∃x¬Px)→∃x(Px∧¬Psx)} 1と21より
逆も同様に示せるので↔が示せる