11/09/01 16:48:08.21
あるいは、「(*)のチェックが どうだこうだ」とかの話題とは関係なしに、
>>423の切り口で説明してもよい。
本当に君が「 P ⇒ Q 」しか証明してないのなら、その証明をSとすれば、
Sは「Pが真である」という過程を最初に置いてしまっているので、
Sを実際に活用するときは、「Pが真である」を追加で
証明しておかなければ、Sは全く機能しない。
つまり、本当に君が「 P ⇒ Q 」しか証明してないなら、
"「 P ⇒ Q 」の証明Sの結果として、「Pが真」も言えている"
ということは起きない。証明Sを活用するためには、
「Pが真」を追加で証明しておかなければならないからだ。