Formele_logica_predikatenlogica_PDL_bewijs_resolutie

Een bijzonder krachtige bewijsmethode voor de formele logica, die behalve de propositielogica (PPL) ook de predikatenlogica (PDL) aankan, is die van resolutie.

{Zie o.m. John Alan Robinson (1965).}

Anders dan de bewijsmethoden van de PPL, zoals die van de waarheidswaardetabellen en de convergente reductie methode, werkt resolutie niet via positieve bewijsvoering maar volgens het principe van negatieve bewijsvoering.

**2. Toetsing via logische falsificatie.**

Het principe van 'negatieve' bewijsvoering is: als we de uitgangspunten van een redenering willen weerleggen, dan hoeven we alleen maar aan te tonen dat de eindconclusie van de redenering onwaar is. Want dan volgt logisch noodzakelijk dat het geheel van alle voorgaande argumenten, of redeneerschakels, althans in de hoofdlijn van de redenering, onwaar is - tot en met de eerste premisse.

Dit principe geldt ook voor een complex samenstel of netwerk van beweringen en redeneringen zoals een theorie of verklaringsmodel met betrekking tot een bepaald gebied in de werkelijkheid (zoals fysisch-empirisch domein of sociaal-empirisch domein).

De algemene redenering achter het principe van logische falsificatie-toetsing is deze. Een theorie of model vormt, samen met al zijn mogelijke implicaties en consequenties, in wezen één complexe ketenredenering met een bepaalde basislijn van premissen en conclusies. In die basislijn hoeven we echter maar één onware schakel te vinden. Zodra de logisch correct afgeleide consequenties van een model ergens uitlopen op een onwaarheid op de hoofdlijn van redenering - bijvoorbeeld vastlopen in een contradictie, hoe miniem ook - dan volgt daaruit dat het model zelf als geheel niet algemeen geldig is. Wanneer de gevonden contradictie steunt op een specifieke interpretatie, dan is bewezen dat het model niet in alle interpretaties consistent is - anders volgt dat het model als geheel zelfs inconsistent is.
Het maakt daarbij niet uit of het model hypothetisch, tentatief en voorlopig bedoeld is.

Met negatieve bewijsvoering kunnen we in principe twee kanten op:

(a)

Controleren van een model.

Meest voor de hand liggende toepassing van negatieve bewijsvoering is uiteraard toetsing van een model op logische vervulbaarheid via het checken van haar consistentie.

(a1)

Weerlegging van algemene geldigheid.

Deze aanpak is allereerst zeer effectief om bijvoorbeeld een bewering of betoog op een geldige manier te weerleggen , bijvoorbeeld van een opponent in een debat.

(a2)

Reparatie en optimalisering.

Het is daarnaast een uitstekende methode voor het controleren en toetsen van de eigen opvattingen en denkbeelden, om mogelijke tekortkomingen op te sporen, en deze waar mogelijk te corrigeren.

{N.b. Dit is bij uitstek nuttig wanneer het onderwerp of verwijzingsgebied behoort tot een 'open systeem', zoals de alledaagse werkelijkheid, fysisch, psychisch of sociaal. Typerend voor zulke domeinen is dat verschijnselen en categorieën niet eenduidig zijn af te bakenen, onbegrensd of 'onafzienbaar' zijn. Daardoor blijven onze gegevens over de werkelijkheid altijd enigszins 'fuzzy': onvolledig, onnauwkeurig en onzeker, blijven begrippen en termen die we ervoor gebruiken wat 'wollig', plooibaar en rekbaar, en blijven modellen en theorieën 'sloppy'. Toch kunnen we behoorlijke zekerheid krijgen over de betrouwbaarheid van kennis, wanneer we niet alleen zoeken naar bevestiging, maar vooral naar weerlegging van onze overtuigingen (het zgn. 'Falsificatie-principe'; vgl. Popper, K.R., 1934). Zie ook: Principes van 'Modelvorming'. De mogelijkheden van kennis, informatie en logica. }

Door falsificatie-toetsing verkrijgen we hoogwaardige informatie waarmee we onze kennis - relatief - kunnen verbeteren.

{N.b. Het is al sinds de oudheid in de filosofie bekend dat volmaakte kennis onbereikbaar is. Toch is het ontegenzeggelijk mogelijk om kennis te vergaren en te verbeteren. Zie ook: Bewijsvoering via falsificatie': In plaats van bevestiging, liever weerlegging zoeken.}

(a3)

Indirect bewijs van vervulbaarheid.

Verder kunnen we een model controleren op tekortkomingen om aan te tonen dat het tenminste niet tot contradicties leidt. Dit is een nuttige eerste stap als onderdeel van positieve bewijsvoering, waarbij we ook naar aanwijzingen en gegevens zoeken die de onderdelen van het model kunnen bevestigen (via verificatie).

(b)

Weerleggen van het tegendeel.

Een andere mogelijkheid die negatieve bewijsvoering biedt is het bewijzen van een model door aan te tonen dat het tegendeel onhoudbaar is.
De bedoeling is hierbij om het bewijs te leveren via negatieve bewijsvoering (falsificatie, refutatie ): door weerlegging van het tegendeel of 'omgekeerde' van de te bewijzen stelling, middels afleiding van een contradictie (reductie ad absurdum).
Hiervoor is met name resolutie geschikt.

**3. Uitgangspunten van Resolutie.**

Strategie van resolutie.

Resolutie is een methode van bewijsvoering door weerlegging van het tegendeel van wat te bewijzen staat.
Bij resolutie proberen we de logische geldigheid van een model te bewijzen door aan te tonen dat het omgekeerde van het model onhoudbaar is, want logisch onvervulbaar c.q. inconsistent. Dit door het aantonen van contradictie op de hoofdlijn van redenering (reductio ad absurdum).

Eigenschappen van resolutie.

(•) De resolutie methode is bij uitstek geschikt in de fase van bewijsvoering, de context of justification.
(•) De resolutiemethode werkt in principe strikt syntactisch, het volgens formele regels combineren van symbolen.
(•) Het (algemene) resolutie principe: is aantoonbaar correct en volledig.

4. Globaal Schema voor Resolutie.

Gegeven een hypothetische stelling, in formule vorm.

R₀.
Bijv.: R₀

=

B ).

De Resolutie procedure :
Dient ten behoeve van bewijs van een theorema R₀,
door middel van weerlegging van het tegendeel van R₀, nl. S₀.

Stappen.

Traject van weerlegging van het tegendeel.

(1)

Negatie van de stelling.

Formuleer het tegendeel van R₀.

(S₀ ≡ ¬R₀).
Bijv.: S₀

=

¬B ).

(2)

Tijdelijke 'pseudo-aanname' van het 'contra-model'.

Aanname van het tegendeel, S₀.

? S₀.

(3)

Ordenen van de zoekruimte.

Beperkt de hoeveelheid benodigde operaties, verkleint de kans op fouten, vergroot de kans op treffers.
Door vereenvoudiging, standaardisatie.
Syntactisch.
Via Normaal vorm conversies.

• Nestingvereenvoudiging (associatief).
• Volgorde standaardisering (commutatief).
• Unificatie(s).
(geldig onder parafrase).

(·) Variabelen-herbenoeming(en).

• (Syntactische) doublure eliminatie.
• Negatief normaal vorm (

NNF

) conversie.
• Connectief normaal vorm conversie.
Met name Conjunctief normaal vorm (

CNF

).
Via Distributie c.q. Comprimatie.
• Kwantor prefix vorm.
Met behoud van kwantor volgorde (d.i. onderlinge verwijzingsrelaties).
• Kwantor eliminatie.

(·) Existentiële kwantor eliminatie.
Skolem Normaal vorm.
(·) Universele kwantor eliminatie.
Universele Instantiatie vorm.

Bijv.:

(S₀

=

(C_[1] ..

C_[n]) ).

(4)

Minimaliseren van de zoekruimte.

Met behoud van syntactische reikwijdte.
Met behoud van referentiële reikwijdte.

Via maximaal mogelijke Syntactische Reductie (geldig onder parafrase).

• Transferente equivalentie eliminatie.
• Basale/ Lokale implicatie eliminatie.
Via Condensatie.
• 'Niet-fatale' ('pseudo') contradictie eliminatie.
Via Subsumptie.
• Transferente contradictie eliminatie.
• (Partiële) Symmetrische contradictie 'type I' eliminatie.
Geldig onder parafrase.

(·) A. Met daarnaast uitsluitend 'Symmetrische equivalentie'.
(·) B. Gecombineerd Symmetrische equivalentie èn contradictie; 'gemengd', d.i. 'kruiselings verdeeld';
met daarnaast géén niet-unificeerbare elementen.

• Clausule Normaal vorm conversie.
Zet CNV(S₀) om in verzameling conjuncten (clause set).

Bijv.:

(S₀^*

=

{C_[1] .., C_[n]} ).

(5)

Aansturen op Reductio ad absurdum.

Vergroot de kans op unit conflict op de hoofdlijn.
Indien nodig via minimaal benodigde Semantische Reductie (geldig onder degressie).
Bijv. t.b.v. unificatie.

• Unificatie(s).
(geldig onder degressie).
Op basis van Most general unifier (mgu).

(·) Variabelen-substitutie(s).
Vervanging door constante namen c.q. functie toepassingen.

• (Partiële) Symmetrische contradictie 'type II' eliminatie.
Geldig onder degressie: Basale conjunctieve reductie, of Contractie.

(·) A. Met daarnaast uitsluitend niet-unificeerbare elementen.
(·) B. Gecombineerd met Symmetrische equivalentie, al dan niet 'kruiselings verdeeld',

(6)

Toets (syntactische) consistentie.

Lever het bewijs dat S₀ inconsistent is (syntactisch).
Via afleiding uit S₀ van minstens één contradictie op de hoofdlijn van redenering.
(reductio ad absurdum).

(•) Hoofdwet: Falsificatie via 'Basale contradictie'.

(·) Expliciet: wegens Exclusief disjunctie.

Bijv.: (

i ((S₀^*

{C_[i],¬C_[i]} ) )_i ).

(·) Impliciet: wegens 'Basale implicatie', wegens Partieel Exclusief disjunctie.

Bijv.: (

j (((S₀^*

{¬C_[i],C_[j]} )

(C_[j]

_(degres) C_[i] )

(C_[i]

C_[j] ) );

(S₀^*

{¬C_[i],C_[i]} ) ) )_i ).

(

i ( (C_[i]

¬C_[i] ) [

(C_[i]

#

_(u) ¬C_[i] ); ]

_(u)

$

0 )_i ).

(•) Hoofdwet: Uit bewijsbaarheid van contradictie volgt inconsistentie.

(

i (((C_[i]

¬C_[i] )

_(u)

$

0 )

({C_[i],¬C_[i]}

) )_i ).

Subset {C_[i],¬C_[i]} is beslisbaar inconsistent.
(•) Hoofdwet: Uit bewijsbaarheid van inconsistentie van een subset volgt inconsistentie van de gehele verzameling.

(S₀

=

(C_[1] ..

C_{[
n]}) );

((S₀^*

=

{C_[1] .., C_[n]} );

( (

i ((S₀^*

{C_[i],¬C_[i]} );

(((C_[i]

¬C_[i] )

_(u)

$

0 );

({C_[i],¬C_[i]}

{} ) ) )_i );

(S₀^*

) ) ).

Verzameling S₀^* is beslisbaar inconsistent.

(7)

Toets (semantische) vervulbaarheid.

Lever het bewijs dat S₀ volledig onvervulbaar is (semantisch).

(•) Hoofdwet: Uit bewijsbaarheid van inconsistentie volgt onvervulbaarheid,

(S₀^*

);

(S₀

);

(

¬S₀ ).

Formule S₀ is beslisbaar onvervulbaar.

(8)

Conclusie over (semantische) validiteit.

(•) Hoofdwet: Falsificatie wegens Afleidbaarheid van directe 'Basale onwaarheid' ( falsum).

(

¬S₀ )

(S₀ ≡

$

0 ).

(•) Hoofdwet: Falsificatie wegens Equivalentie aan directe 'Basale onwaarheid' (falsum).

(S₀ ≡

$

0) ≡ (¬S₀).

(•) Hoofdwet: Dubbele negatie eliminatie.

(¬S₀) ≡ ¬(¬R₀); ≡ (¬¬R₀); ≡ R₀.

(•) Hoofdwet: Uit bewijsbaarheid van contradictie uit het tegendeel volgt geldigheid.

(S₀^*

);

(S₀

)

(

¬S ₀ );

(

¬(¬R₀ );

(

¬¬R₀ );

(R₀

);

(

R₀ ).

Formule R₀ is resolutie-beslisbaar geldig.


*Methode Formele Logica:* Bewijsvoering *de Resolutiemethode.* Inhoudsopgave *1. Inleiding tot Introductie Resolutielogica.* *2. Toetsing via logische falsificatie.* (a) Controleren van een model. (a1) Weerlegging van algemene geldigheid. (a2) Reparatie en optimalisering. (a3) Indirect bewijs van vervulbaarheid. (b) Weerleggen van het tegendeel. *3. Uitgangspunten van Resolutie.* 4. Globaal Schema voor Resolutie. (1) Negatie van de stelling. (2) Tijdelijke 'pseudo-aanname' van het 'contra-model'. (3) Ordenen van de zoekruimte. (4) Minimaliseren van de zoekruimte. (5) Aansturen op Reductio ad absurdum. (6) Toets (syntactische) consistentie. (7) Toets (semantische) vervulbaarheid. (8) Conclusie over (semantische) validiteit. *1. Inleiding tot Introductie Resolutielogica.* Een bijzonder krachtige bewijsmethode voor de formele logica, die behalve de propositielogica (PPL) ook de predikatenlogica (PDL) aankan, is die van resolutie. {Zie o.m. John Alan Robinson (1965).} Anders dan de bewijsmethoden van de PPL, zoals die van de waarheidswaardetabellen en de convergente reductie methode, werkt resolutie niet via positieve bewijsvoering maar volgens het principe van negatieve bewijsvoering. *2. Toetsing via logische falsificatie.* Het principe van 'negatieve' bewijsvoering is: als we de uitgangspunten van een redenering willen weerleggen, dan hoeven we alleen maar aan te tonen dat de eindconclusie van de redenering onwaar is. Want dan volgt logisch noodzakelijk dat het geheel van alle voorgaande argumenten, of redeneerschakels, althans in de hoofdlijn van de redenering, onwaar is - tot en met de eerste premisse. Dit principe geldt ook voor een complex samenstel of netwerk van beweringen en redeneringen zoals een theorie of verklaringsmodel met betrekking tot een bepaald gebied in de werkelijkheid (zoals fysisch-empirisch domein of sociaal-empirisch domein). De algemene redenering achter het principe van logische falsificatie-toetsing is deze. Een theorie of model vormt, samen met al zijn mogelijke implicaties en consequenties, in wezen één complexe ketenredenering met een bepaalde basislijn van premissen en conclusies. In die basislijn hoeven we echter maar één onware schakel te vinden. Zodra de logisch correct afgeleide consequenties van een model ergens uitlopen op een onwaarheid op de hoofdlijn van redenering - bijvoorbeeld vastlopen in een contradictie, hoe miniem ook - dan volgt daaruit dat het model zelf als geheel niet algemeen geldig is. Wanneer de gevonden contradictie steunt op een specifieke interpretatie, dan is bewezen dat het model niet in alle interpretaties consistent is - anders volgt dat het model als geheel zelfs inconsistent is. Het maakt daarbij niet uit of het model hypothetisch, tentatief en voorlopig bedoeld is. Met negatieve bewijsvoering kunnen we in principe twee kanten op: (a) Controleren van een model. Meest voor de hand liggende toepassing van negatieve bewijsvoering is uiteraard toetsing van een model op logische vervulbaarheid via het checken van haar consistentie. (a1) Weerlegging van algemene geldigheid. Deze aanpak is allereerst zeer effectief om bijvoorbeeld een bewering of betoog op een geldige manier te weerleggen , bijvoorbeeld van een opponent in een debat. (a2) Reparatie en optimalisering. Het is daarnaast een uitstekende methode voor het controleren en toetsen van de eigen opvattingen en denkbeelden, om mogelijke tekortkomingen op te sporen, en deze waar mogelijk te corrigeren. {N.b. Dit is bij uitstek nuttig wanneer het onderwerp of verwijzingsgebied behoort tot een 'open systeem', zoals de alledaagse werkelijkheid, fysisch, psychisch of sociaal. Typerend voor zulke domeinen is dat verschijnselen en categorieën niet eenduidig zijn af te bakenen, onbegrensd of 'onafzienbaar' zijn. Daardoor blijven onze gegevens over de werkelijkheid altijd enigszins 'fuzzy': onvolledig, onnauwkeurig en onzeker, blijven begrippen en termen die we ervoor gebruiken wat 'wollig', plooibaar en rekbaar, en blijven modellen en theorieën 'sloppy'. Toch kunnen we behoorlijke zekerheid krijgen over de betrouwbaarheid van kennis, wanneer we niet alleen zoeken naar bevestiging, maar vooral naar weerlegging van onze overtuigingen (het zgn. 'Falsificatie-principe'; vgl. Popper, K.R., 1934). Zie ook: Principes van 'Modelvorming'. De mogelijkheden van kennis, informatie en logica. } Door falsificatie-toetsing verkrijgen we hoogwaardige informatie waarmee we onze kennis - relatief - kunnen verbeteren. {N.b. Het is al sinds de oudheid in de filosofie bekend dat volmaakte kennis onbereikbaar is. Toch is het ontegenzeggelijk mogelijk om kennis te vergaren en te verbeteren. Zie ook: Bewijsvoering via falsificatie': In plaats van bevestiging, liever weerlegging zoeken.} (a3) Indirect bewijs van vervulbaarheid. Verder kunnen we een model controleren op tekortkomingen om aan te tonen dat het tenminste niet tot contradicties leidt. Dit is een nuttige eerste stap als onderdeel van positieve bewijsvoering, waarbij we ook naar aanwijzingen en gegevens zoeken die de onderdelen van het model kunnen bevestigen (via verificatie). (b) Weerleggen van het tegendeel. Een andere mogelijkheid die negatieve bewijsvoering biedt is het bewijzen van een model door aan te tonen dat het tegendeel onhoudbaar is. De bedoeling is hierbij om het bewijs te leveren via negatieve bewijsvoering (falsificatie, refutatie ): door weerlegging van het tegendeel of 'omgekeerde' van de te bewijzen stelling, middels afleiding van een contradictie (reductie ad absurdum). Hiervoor is met name resolutie geschikt. *3. Uitgangspunten van Resolutie.* Strategie van resolutie. Resolutie is een methode van bewijsvoering door weerlegging van het tegendeel van wat te bewijzen staat. Bij resolutie proberen we de logische geldigheid van een model te bewijzen door aan te tonen dat het omgekeerde van het model onhoudbaar is, want logisch onvervulbaar c.q. inconsistent. Dit door het aantonen van contradictie op de hoofdlijn van redenering (reductio ad absurdum). Eigenschappen van resolutie. (•) De resolutie methode is bij uitstek geschikt in de fase van bewijsvoering, de context of justification. (•) De resolutiemethode werkt in principe strikt syntactisch, het volgens formele regels combineren van symbolen. (•) Het (algemene) resolutie principe: is aantoonbaar correct en volledig. 4. Globaal Schema voor Resolutie. Gegeven een hypothetische stelling, in formule vorm. R₀. Bijv.: R₀ = (A B ). De Resolutie procedure : Dient ten behoeve van bewijs van een theorema R₀, door middel van weerlegging van het tegendeel van R₀, nl. S₀. Stappen. Traject van weerlegging van het tegendeel. (1) Negatie van de stelling. Formuleer het tegendeel van R₀. (S₀ ≡ ¬R₀). Bijv.: S₀ = (A ¬B ). (2) Tijdelijke 'pseudo-aanname' van het 'contra-model'. Aanname van het tegendeel, S₀. ? S₀. (3) Ordenen van de zoekruimte. Beperkt de hoeveelheid benodigde operaties, verkleint de kans op fouten, vergroot de kans op treffers. Door vereenvoudiging, standaardisatie. Syntactisch. Via Normaal vorm conversies. • Nestingvereenvoudiging (associatief). • Volgorde standaardisering (commutatief). • Unificatie(s). (geldig onder parafrase). (·) Variabelen-herbenoeming(en). • (Syntactische) doublure eliminatie. • Negatief normaal vorm ( NNF ) conversie. • Connectief normaal vorm conversie. Met name Conjunctief normaal vorm ( CNF ). Via Distributie c.q. Comprimatie. • Kwantor prefix vorm. Met behoud van kwantor volgorde (d.i. onderlinge verwijzingsrelaties). • Kwantor eliminatie. (·) Existentiële kwantor eliminatie. Skolem Normaal vorm. (·) Universele kwantor eliminatie. Universele Instantiatie vorm. Bijv.: (S₀ = (C_[1] .. C_[n]) ). (4) Minimaliseren van de zoekruimte. Met behoud van syntactische reikwijdte. Met behoud van referentiële reikwijdte. Via maximaal mogelijke Syntactische Reductie (geldig onder parafrase). • Transferente equivalentie eliminatie. • Basale/ Lokale implicatie eliminatie. Via Condensatie. • 'Niet-fatale' ('pseudo') contradictie eliminatie. Via Subsumptie. • Transferente contradictie eliminatie. • (Partiële) Symmetrische contradictie 'type I' eliminatie. Geldig onder parafrase. (·) A. Met daarnaast uitsluitend 'Symmetrische equivalentie'. (·) B. Gecombineerd Symmetrische equivalentie èn contradictie; 'gemengd', d.i. 'kruiselings verdeeld'; met daarnaast géén niet-unificeerbare elementen. • Clausule Normaal vorm conversie. Zet CNV(S₀) om in verzameling conjuncten (clause set). Bijv.: (S₀^* = {C_[1] .., C_[n]} ). (5) Aansturen op Reductio ad absurdum. Vergroot de kans op unit conflict op de hoofdlijn. Indien nodig via minimaal benodigde Semantische Reductie (geldig onder degressie). Bijv. t.b.v. unificatie. • Unificatie(s). (geldig onder degressie). Op basis van Most general unifier (mgu). (·) Variabelen-substitutie(s). Vervanging door constante namen c.q. functie toepassingen. • (Partiële) Symmetrische contradictie 'type II' eliminatie. Geldig onder degressie: Basale conjunctieve reductie, of Contractie. (·) A. Met daarnaast uitsluitend niet-unificeerbare elementen. (·) B. Gecombineerd met Symmetrische equivalentie, al dan niet 'kruiselings verdeeld', (6) Toets (syntactische) consistentie. Lever het bewijs dat S₀ inconsistent is (syntactisch). Via afleiding uit S₀ van minstens één contradictie op de hoofdlijn van redenering. (reductio ad absurdum). (•) Hoofdwet: Falsificatie via 'Basale contradictie'. (·) Expliciet: wegens Exclusief disjunctie. Bijv.: (i ((S₀^* {C_[i],¬C_[i]} ) )_i ). (·) Impliciet: wegens 'Basale implicatie', wegens Partieel Exclusief disjunctie. Bijv.: (i j (((S₀^* {¬C_[i],C_[j]} ) (C_[j] _(degres) C_[i] ) (C_[i] C_[j] ) ); (S₀^* {¬C_[i],C_[i]} ) ) )_i ). (i ( (C_[i] ¬C_[i] ) [ (C_[i] # _(u) ¬C_[i] ); ] _(u) $ 0 )_i ). (•) Hoofdwet: Uit bewijsbaarheid van contradictie volgt inconsistentie. (i (((C_[i] ¬C_[i] ) _(u) $ 0 ) ({C_[i],¬C_[i]} ) )_i ). Subset {C_[i],¬C_[i]} is beslisbaar inconsistent. (•) Hoofdwet: Uit bewijsbaarheid van inconsistentie van een subset volgt inconsistentie van de gehele verzameling. (S₀ = (C_[1] .. C_{[ n]}) ); ((S₀^* = {C_[1] .., C_[n]} ); ( (i ((S₀^* {C_[i],¬C_[i]} ); (((C_[i] ¬C_[i] ) _(u) $ 0 ); ({C_[i],¬C_[i]} {} ) ) )_i ); (S₀^* ) ) ). Verzameling S₀^* is beslisbaar inconsistent. (7) Toets (semantische) vervulbaarheid. Lever het bewijs dat S₀ volledig onvervulbaar is (semantisch). (•) Hoofdwet: Uit bewijsbaarheid van inconsistentie volgt onvervulbaarheid, (S₀^* ); (S₀ ); ( ¬S₀ ). Formule S₀ is beslisbaar onvervulbaar. (8) Conclusie over (semantische) validiteit. (•) Hoofdwet: Falsificatie wegens Afleidbaarheid van directe 'Basale onwaarheid' ( falsum). ( ¬S₀ ) (S₀ ≡ $ 0 ). (•) Hoofdwet: Falsificatie wegens Equivalentie aan directe 'Basale onwaarheid' (falsum). (S₀ ≡ $ 0) ≡ (¬S₀). (•) Hoofdwet: Dubbele negatie eliminatie. (¬S₀) ≡ ¬(¬R₀); ≡ (¬¬R₀); ≡ R₀. (•) Hoofdwet: Uit bewijsbaarheid van contradictie uit het tegendeel volgt geldigheid. (S₀^* ); (S₀ ) ( ¬S ₀ ); ( ¬(¬R₀ ); ( ¬¬R₀ ); (R₀ ); ( R₀ ). Formule R₀ is resolutie-beslisbaar geldig.