8.3.2 Teoremo de refuto

Teoremo de refuto diras ke $\Gamma\vDash A\Longleftrightarrow\ \nVdash\Gamma,\neg A$.

Pervorte: aro da formuloj $\Gamma$ (gamma) havas kiel sekvo $A$ se kaj nur se la sistemo formata per $\Gamma$ kune de $\neg A$ estas malplenumebla.

Tio pri kiel pruvi malplenumeblo estas alia temo, iom longa, kiel ĝia nomo sugestas. Unu el la facilaj rimedoj estas uzi arbon de klaŭza rezolucio.