5.6 Kun subderivoj. $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$

La afero malfaciliĝas. Jen la solvo de $P\Rightarrow(Q\Rightarrow R)\vdash Q\Rightarrow(P\Rightarrow R)$:

$$\begin{fitch} \par P \Rightarrow (Q \Rightarrow R) \\ \par \... ...arrow (P \Rightarrow R) & I$\Rightarrow$\ 2,6 \par \end{fitch}$$

Unue: ĉi tie oni nur uzos la du derivregulojn kiuj helpas enigi kaj forigi implikaciojn, ĉar ĝi estas la sola operatoro kiun oni havas.

Oni volas atingi $Q\Rightarrow(P\Rightarrow R)$, do oni devos fari hipotezon $Q$ ĉe kie oni devos montri ke $P\Rightarrow R$. Faru tion nun por faciligi la problemon: oni malfermas la subderivon en linio 2. Oni ne fermos ĝin ĝis kiam oni scias ke $P\Rightarrow R$ estas certa.

Nun la problemo estas iom pli facila. Oni bezonas pruvi $P\Rightarrow R$, kaj havas du liniojn kun du veraĵoj: la unua diras $P\Rightarrow(Q\Rightarrow R)$, kaj la dua $Q$.

Kiel povas oni alproksimiĝi al $P\Rightarrow R$? Nu, same kiel iam ajn: ni devas supozi ke $P$, kaj eltrovi ke $R$, iel. Eĉ se tio ne ŝajnas facila, estas kion oni faru, ĉar la kunimplikaciigo tiel funkcias. Do, malfermu alian hipotezon, nun supozante ke $P$, kaj eble oni atingos $R$. Ĉi tiu estas hipotezo en hipotezo, tamen tio estas nenia problemo.

Skribinte la linio 3, kaj, metite en subsubderivo, oni disponas de tri scioj: ke $P\Rightarrow(Q\Rightarrow R)$, ke $Q$, kaj ke $P$. Oni devas pruvi ke $R$. Ne estas tiom malfacile, ĉu? Se oni scias ke $P$, uzante elimplikaciigon kun linio 1 oni ricevos la certan formulon $Q\Rightarrow R$. Ĉar $Q$ ankaŭ certas (linio 2), oni povas reapliki tiun regulon por ekscii ke $R$.

Videble, supozinte $P$ oni atingis la konkludon $R$, do eblas skribi en nova linio ke $P\Rightarrow R$, kion ni serĉadis. Nun jam eliris el la subsubderivo, kaj nur estas sub la supozo ke $Q$ certas. Ĉar oni vidas ke tiu supozo entenas la certecon de la formulo $P\Rightarrow R$, oni povas eliri tiun subderivon konkludante ke $Q\Rightarrow(P\Rightarrow R)$.

$Q\Rightarrow(P\Rightarrow R)$ estis precipe kion oni volis pruvi, do jam estas finata la derivo.