3.4 Notacio

Eblas diversaj manieroj por skribi naturdeduktajn skemojn. Mi uzos la stilon Fitch, pro esti kiun mi estis instruita, esti facile komprenebla, kaj necesigi malgrandan spacon. Ĝi estas tiel:

$$\begin{fitch} \par P \Rightarrow Q \\ \par Q \Rightarrow R \... ... \Rightarrow Q \wedge R & I$\Rightarrow$\ 3,6 \par \end{fitch}$$

Ĉi tio pruvas validecon de $P\Rightarrow Q,\ Q\Rightarrow R\vdash P\Rightarrow Q\wedge R$.

La skemon oni legas linion post linio, de supre al sube. La maldekstrajn numerojn montras la numeron de ĉiu linio, kaj ĉiam estas laŭorde.

La linioj plej supre enhavas ĉiun el la formuloj kiuj troviĝas en la maldekstra parto de la derivo. Nun oni havas du: $P\Rightarrow Q$ kaj $Q\Rightarrow R$. De tiuj oni devos konkludi $P\Rightarrow Q\wedge R$.

En ĉiu linio estas notata kion aĵon oni trovis certa, kaj dekstre oni klarigas kiel ĝi estas trovita. Tiuj simboloj dekstraj estas mallongigoj de nomoj el la 9 reguloj: $E$ estas pro la angla ``elimination'' kaj $I$ pro ``introduction'' (mi konservas tian notacion, komuna por plej lingvoj). En Esperanto, oni povas uzi ``forigo'' kaj ``enigo'', aŭ prefiksojn ``el-'' kaj ``kun-'' (mi sekve klarigos tion).

Ekzemple, kelkajn regulojn oni vidas tie estas elimplikaciigo ($E\Rightarrow$), kunkajigo ($I\wedge$), kaj kunimplikaciigo ($I\Rightarrow$). Komprenu la vortojn: el-kaj-ig-o estas forigo de konjunkcio (kaj-o), kun-aŭ-ig-o estas enigo de disjunkcio (aŭ-o), el-neg-ig-o estas forigo de negacio (neg-o), ktp. La nomoj de la 9 derivreguloj estas do kunkajigo, elkajigo, kunaŭigo, elaŭigo, kunimplikaciigo, elimplikaciigo, kunnegigo, elnegigo, iteracio. Vi ankaŭ povas legi ilin longe, kvazaŭ la angla (``implication elimination'', ``disjunction introduction'', ktp.).

La numeroj kunigantaj la nomojn de ĉiu regulo klarigas la loko el kie oni prenis la necesajn formulojn por apliki tiun regulon. Ili estas liniajn numerojn, do, por apliki regulon oni devas nur uzi informon el la jam verkitaj supraj linioj.

Fine, tiu vertikala linieto kiu trairas de linio 3 al la 6 estas hipotezo (tial oni skribis $H$ dekstre). Ĉio kio estas enmetita tie ne estas ĉiam certa, sed nur kiam certas $P$ (la komenco de la hipotezo, ĉe linio 3). Tial, formuloj trovitaj ĉe la hipotezo oni ne uzu ekstere, ĉar ili ne estas ĉiam pravaj.

La procedo finiĝas kiam oni eltrovas ke estas prava la formulo verkita dekstre de la derivsimbolo, jen $P\Rightarrow Q\wedge R$ (tio aperas ĉe la lasta linio).