仮定は、ツリーの一部でなくても放電できますか？

Question

次の式が与えられた場合、自然演繹を使用して、それが成り立つことを証明します。

教授からの回答は以下のとおりです。

ブラケット2のpsiのようにツリー自体から実際に派生させることなく、ブラケット3のphiの仮定をどのように放電できるかを理解したいと思います。

Answer 1

仮定は、ツリーの一部でなくても放電できますか？

はい。

たとえば、Dirk van Dalen（1997） "Logic and Structure"、p。34：

仮説の取り消しに関しては、命題のすべての出現を必ずしも取り消すわけではないことに注意してください。$\psi$。仮説を追加しても命題が理解できないと感じるので、これは明らかに正当化されます（無関係な情報が常に追加される可能性があります）。ただし、可能な限りキャンセルするのは慎重さの問題です。なぜ必要以上の仮説を立てるのですか？
さらに、適用することができます$(\to I)$ キャンセルに利用できる仮説がない場合。 $\dfrac{\phi}{\psi \to \phi}(\to I)$ を使用して、正しい派生です $(\to I)$。
要約すると、[...]発生があれば、いくつか（またはすべて）を削除します[...]。

これの意味論的正当化は単調性（弱体化としても知られています）です：私たちはそれを持っています

場合 $\Gamma \vDash \phi$、その後 $\Gamma, \psi \vDash \phi$。

演繹定理により、次のようにもなります。

場合 $\Gamma \vDash \phi$、その後 $\Gamma \vDash \psi \to \phi$。

特定の前提のセットから結論を確立できる場合、知識を追加しても「失われる」ことはないため、実際には必要のない前提や前提条件をいつでも追加できます。このセマンティックアイデアは派生に移行します。

同じことが、仮定を実行することを許可する他のすべてのルールにも当てはまります。 $(\lor E)$、 $(\neg I)$ そして $(RAA)$。