3.3 Agmaniero

Oni estas demandita pruvi la validecon de $\Gamma\vdash S$, kie $\Gamma$ (legata gamma) estas aro da formuloj disrompitaj per komoj, kaj $S$ estas simpla formulo.

Komencante, oni akceptos ĉiujn formulojn el $\Gamma$ kiel certaj, kaj, per 9 precizaj reguloj, eltrovos kiuj aliaj aĵoj estas ankaŭ certaj. Nia intenco estas trovi ke $S$ ja certas; do ĉi tio ĵus atingite, oni haltiĝos.

Iam estos trovebla neniun veraĵon, do oni supozados: ``nu, mi ne scias se $A\wedge B$ ĉiam estas certa, sed se $C$ certas, tiam ĝi estas vera sendube''. Tiel oni ektrovis iun novan veraĵon: $C\Rightarrow A\wedge B$.

Kompreneble, oni ĉiam devas memori kion oni volas atingi, ĉar alie, oni divenus multajn veraĵojn kiuj ja estas veraj, sed estus tute malbezonataj por la nuna ekzerco. Ekzemple, por $A\vee B,\ \neg A\vdash B$ oni devas atingi la verecon de $B$. Eble ni eltrovos ke $\neg(A\wedge B)$, $A\vee B\vee C$, $(A\vee B)\Rightarrow\neg A$, kaj tiel plu; sed ni nur bezonas $B$, ne aliaj. Do, se vi devojiĝas de la simpla solvo, vi eble konfuziĝos.