5.12 Iu interesa. $P\vee Q,\ \neg P\vdash Q$

Ankaŭ ŝajnas facila: $P\vee Q,\ \neg P\vdash Q$. Jen:

$$\begin{fitch} \par P \vee Q \\ \par \neg P \\ \par \fh P & ... ...par \fa Q & IT 9 \\ \par Q & E$\vee$\ 1,8,10 \par \end{fitch}$$

Estas facilege kompreneble por iu ajn: certas $P\vee Q$, sed $P$ estas falsa, do la vero estas $Q$.

Diversaj metodoj ekzistas, sed iam oni devos uzi elaŭigon por ion fari kun $P\vee Q$. Provu pruvi ke ambaŭ $P$ kaj $Q$ kondukas al la sama loko, kiu estos nian celan formulon $Q$ (ĉar eblas iri direkte al $Q$, do profitu).

Do oni malfermas subderivon supozante $P$, kaj celas eltrovi ke $Q$. Ne estas tre kompleksa, ĉar oni havas la $\neg P$ en linio 2; tio helpas kontraŭdiri ion ajn. Oni serĉas $Q$, do supozu $\neg Q$ kaj per kunnegigo ricevu $\neg\neg Q$, kiu estas $Q$.

La alian vojon, supozinte $Q$ certa, kondukas direkte al $Q$.

Do, ambaŭ vojoj iras al $Q$ kaj per elaŭigo oni pruvas ke $Q$ ĉiam certas.