5.13 Tiu aperis en mia ekzameno. $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$

Ĉe la fina ekzameno de ILO oni demandis al mi $A\vee B,\ A\Rightarrow C,\ \neg D\Rightarrow\neg B\vdash C\vee D$, kaj mi pasigis multan, multan tempon ĝis mi fine sukcesis:

$$\begin{fitch} \par A \vee B \\ \par A \Rightarrow C \\ \par... ...\vee$\ 12 \\ \par C \vee D & E$\vee$\ 1,6,13 \par \end{fitch}$$

Rimarku ke la rezulton ni serĉas, $C\vee D$, estas aŭo. Ĉar vi jam konas kunaŭigon, vi povus simple serĉi $C$, kaj poste uzi tiun regulon por eltrovi $C\vee D$. Se vi ne trovus ke $C$ certas, vi eblus provi kun $D$, ĉar se $D$ certas, tiam $C\vee D$ ankaŭ estas, kaj oni finas tie.

Bedaŭrinde, $C$ ne estas ĉiam certa, nek $D$ estas ĉiam certa (tamen, $C\vee D$ ja ĉiam certas, kaj tio estas kion oni volas pruvi). Tion komprenite, oni devos serĉi alian rimedon kiu prilaboras kun ambaŭ formulojn, $C$ kaj $D$, samtempe, ĉar ŝajne se oni prenas unu solan sen uzi la alian, ĝi ne aldonas multon da informo.

Por uzi $A\vee B$ oni aplikos provon per okazoj. Oni provos ekscii ke tiel $A$ kiel $B$ kondukas al $C\vee D$, ĉar se oni tion atingas, ne plua laboro restas.

$A$ entenas $C$, kaj se $C$ estas vera, tiam ankaŭ veras $C\vee D$, do $A$ entenas $C\vee D$.

Por $B$, kion ni scias ne rilatas ĝin al $C$ sed al $D$. Oni volas $C\vee D$. Ŝajnas malfacilege ke $C\vee D$ certas pro $C$, do oni provos certigi nur $D$. Por tio, oni uzu redukton al absurdo: supozu $D$ falsa, tiam certas $\neg B$ pro formulo el linio 3. Sed oni estas supozinte la certecon de $B$, do nia hipotezo $\neg D$ ne estu certa. Do $D$ ja certas, kaj konsekvence ankaŭ $C\vee D$.

Ĉar $A\vee B$ ja certas, kaj ambaŭ vojoj kondukas al $C\vee D$, oni fine vidas ke $C\vee D$ ĉiam estas certa.

Se vi estas lerta laboristo de logikaj formuloj, eble vi eksciiĝis ke $\neg D\Rightarrow\neg B$ estas $B\Rightarrow D$. Tio tre simpligas la problemon kaj helpas ĝin kompreni pli frue. Tamen, vi ne rajtas ŝanĝi $\neg D\Rightarrow\neg B$ per $B\Rightarrow D$ direkte; vi faru tion paŝon post paŝo por pli ĝui la logikon.