5.9 Malplena maldekstra parto. $\vdash P\Rightarrow P$

Pruvi $\vdash P\Rightarrow P$ estas tre facila kaj mallonga:

$$\begin{fitch} \par \fh P & H \\ \par \fa P & IT 1 \\ \par P \Rightarrow P & I$\Rightarrow$\ 1,2 \par \end{fitch}$$

Tia ekzerco ankoraŭ ne aperis: videble, la maldekstra parto de la derivo estas malplena. Tio signifas ke oni estas dirita nenia veraĵo kiun oni povas uzi por pruvi $P\Rightarrow P$. Kial? Nu, ĉar $P\Rightarrow P$ estas ĉiam certa, sendepende de la valoro de $P$ aŭ la aliaj formuloj.

Estas plej komode kaj facile solvi tiajn derivojn, ĉar oni komencas la laboron direkte kun la formulon oni volas atingi. Sed atentu, ĉar kelkaj absolutaj veroj (kiaj ĉiam estas pravaj) estas ege malfacile kaj bezonas longajn pruvojn.

Notu: ĉiam kiam la maldekstra parto estas malplena, oni devas komenci per hipotezo (kion alian oni povus fari?).

Por atingi la pruvon de $P\Rightarrow P$ oni agas kiel antaŭe: supozu $P$ kaj provu atingi la veron de $P$. Ĉar oni ĵus supozis ĝin ĉe la unua linio, oni nur devas uzi la regulon de iteracio por kopii ĝin al interne, kaj finu la subderivon per kunimplikaciigo. Jam estas ĉio farita, per tri linioj.

Rimarku ke $P\Rightarrow P$ estas certa ĉar $\blacksquare\Rightarrow\blacksquare$ kaj $\square\Rightarrow\square$. Mi profitas por memorigi ke ankaŭ $\square\Rightarrow\blacksquare$, sed $\blacksquare\nRightarrow\square$.