Methode 'Praktische Logica':



Bewijsmethode II voor Propositielogica

:

De convergente reductie bewijsmethode.



Inhoudsopgave


1. Inleiding.


2. Herleiding tot geldig - via parafrase reductie.


(a) In Implicatie.
(b) In Equivalentie.

3. Herleiding tot geldig - via degressief reductie.


(a)

Via Disjunctieve expansie.


(b)

Via Conjunctieve reductie.

.

4. Bewijzen van elementaire wetten - via convergente reductie



1. Inleiding.



Voor alle stellingen in de propositielogica (

PPL

) is het validiteitsprobleem beslisbaar. In principe zal de tabelmethode voor de vraag de geldigheid van formules in de

PPL

altijd een definiet antwoord opleveren.

Wel wordt de tabelmethode bij formules met veel variabelen (atomaire proposities) steeds lastiger. Het aantal unieke mogelijke logische relaties is hyperexponentieel in het aantal items. Daarmee zitten we midden in de combinatorische explosie.
{Zie voor meer details: Informatie, Combinatorische explosie en Logica - korte inleiding.}

De schema's worden daarmee astronomisch groot, de uitwerking wordt snel ondoenlijker en de foutkansen nemen steeds meer toe. Ook bij een geautomatiseerde uitvoering stuiten we al snel op harde grenzen van geheugencapaciteit en rekentijd. Kortom, bij toename van het aantal proposities wordt de tabelmethode al snel praktisch onuitvoerbaar.

Daarom nu de volgende bewijsmethode: de 'convergente reductie methode'.
Hierbij gebruik je een aantal - reeds bewezen - wetten om formules via een kortere route te bewijzen.

Voor dat doel bevat het overzicht van logische wetten een aantal aanvullende, expliciete regels voor convergente reductie bewijsmethode.
{Zie: Inleiding Propositielogica; X. Wetten tbv. convergente reductie bewijsvoering (in

PPL

).}

2. Herleiding tot geldig - via parafrase reductie.



Het idee achter de convergente reductie bewijsmethode is om na te gaan of de te bewijzen formule of redenering via herleiding uiteindelijk equivalent blijkt aan 'waar', dat wil zeggen altijd-waar, oftewel logisch geldig. De manier van aanpak is afhankelijk van het hoofdconnectief. Er zijn twee mogelijke routes:

(a)

In Implicatie.


Het hoofdconnectief van de te bewijzen formule staat in implicatie.
Pas alleen transformaties toe met behoud van logische kracht, dus met equivalent resultaat (d.i. parafrase ).
Stappen:
(a1) Pas

CNV

conversie toe op de gehele formule.
De

CNV

conversie-operatie beginnen met het hoofdconnectief, en daarna de volgende niveau's van inbedding c.q. nestingdiepte.
(a2) Pas daarna indien nodig en mogelijk, andere transformaties en/of reducties toe op de gehele formule, met behoud van equivalentie (parafrase).
(a3) Kijk of het resultaat identiek wordt aan '

$

1' (verum): de stelling blijkt geldig, en is daarmee bewezen.
(a4) Bij een meer complexe formule kun je ook

CNV

conversie, transformaties en/of reducties afzonderlijk toepassen op premisse en op conclusie. Voor de premisse dient dit te gebeuren met behoud van equivalentie, (parafrase ), voor de conclusie mag eventueel verlies van logische kracht plaatsvinden (degressie).
Kijk dan of de premisse wat betreft consequenties uitkomt op de conclusie: ook dan blijkt de stelling geldig.

Nb. In sommige gevallen levert

DNV

conversie hetzelfde resultaat op via een kortere route.

(b)

In Equivalentie.


Het hoofdconnectief van de te bewijzen formule staat in equivalentie.
Stappen:
(b1) Pas

CNV

conversie toe op de antecedens.
Kijk of het resultaat identiek wordt aan de conclusie.
Zo niet:
(b2) Pas

CNV

conversie toe op de consequens.
(b3) Kijk dan of b1 wat betreft consequenties uitkomt op b2.
M.a.w. toets de geldigheid van de implicatierelatie 'b1 b2'.
(b4) Kijk vervolgens of b2 wat betreft consequenties uitkomt op b1.
M.a.w. toets de geldigheid van de implicatierelatie 'b2 b1'.

3. Herleiding tot geldig - via degressief reductie.



Een geldige conclusie is in

PPL

globaal langs twee wegen afleidbaar uit premissen.
(Zie Logische wetten in

PPL

, Afleiden van 'zwakkere' beweringen [I]: degressie.
Via uitbreiding of reductie van bewering of conclusie(s).
(a)

Via Disjunctieve expansie.


Onbeperkte disjunctieve uitbreiding van bewering of conclusie(s).
Disjunct introductie.
Disjunct introductie regel ('v in').
{A}   (A X).
In conclusie:
{A B}   (A (B X)).

(b)

Via Conjunctieve reductie.

.
(Beperkte) Conjunctieve beperking van bewering of conclusie(s).
Conjunct selectie, destillatie.
Conjunct eliminatie regel ('& el').
{A X}   A.
{A X}   A;   (A X).
In conclusie:
{A (B C)}   (A B).

4. Bewijzen van elementaire wetten - via convergente reductie



Voorbeelden.



(9.2a)
{A} (X A).
 

CNV

conversie:
  ≡ (¬A (¬X A));
  ≡ (¬A ¬X A);
  ≡ (¬A A ¬X);
  ≡ ((¬A A) X);
  Reductie:
  ≡ ((

$

1) ¬X);
  ≡ (

$

1 ¬X);
  ≡

$

1 (d.i. geldig).

(9.2b)
{A} (¬A X).
 

CNV

conversie:
  ≡ (¬A (¬¬A X));
  ≡ (¬A A X);
  Reductie:
  ≡ (

$

1 X);
  ≡

$

1 (d.i. geldig).

(9.2c)
{A B} (A (X B)).
Route (a)

CNV

van gehele formule:
  ≡ (¬(A B) (A (X B)));
  ≡ (¬(¬A B) (¬A (X B)));
  ≡ (¬(¬A B) (¬A (¬X B)));
  ≡ (¬(¬A B) ¬A ¬X B);
  ≡ ((A ¬B) ¬A ¬X B) (

DNV

);
  ≡ ((A ¬B) (¬A ¬X B));
  Distributie:
  ≡ ((A (¬A ¬X B)) (¬B (¬A ¬X B)));
  ≡ ((A ¬A B ¬X) (¬B ¬A B ¬X)) (

CNV

);
  ≡ ((A ¬A) B ¬X) ((¬B B) ¬A ¬X));
  Reductie:
  ≡ (((

$

1) B ¬X) ((

$

1) ¬A ¬X));
  ≡ ((

$

1) (

$

1));
  ≡

$

1 (d.i. geldig).
Route (b)

CNV

van premisse resp. conclusie:
  (1) ≡ (¬A B);
  (2) ≡ (¬A ¬X B);
  (3) ((1) (2));
  (4) ≡

$

1 (d.i. geldig).

(9.3)
{A X}   ≡ (¬x ¬A).
Wet van de Contrapositie.
1.

CNV

van premisse:
  ≡ (¬A X);
2.

CNV

van conclusie:
  ≡ (¬(¬X) ¬A));
  ≡ (X ¬A).
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(9.4)
{(A B) A} B.
Modus ponens.
Implicatie Eliminatie regel '> el'.
(a)

CNV

van gehele formule:
  ≡ ((¬(A B) A) B);
  ≡ (¬((¬A B) A) B);
  [Wet: ¬(X Y) ≡ (¬X ¬Y) ]
  ≡ ((¬(¬A B) ¬A) B);
  [Wet: ¬(¬X Y) ≡ (X ¬Y) ]
  ≡ (((A ¬B) ¬A) B);
  ≡ (((A ¬B) ¬A B) (

DNV

);
  Distributie:
  ≡ ((A ¬A B) (¬B ¬A B)) (

CNV

);
  ≡ (((A ¬A) B) (¬B ( B) ¬A));
  Reductie:
  ≡ (((

$

1) B) ((

$

1) ¬A));
  ≡ ((

$

1) (

$

1));
  ≡

$

1 (d.i. geldig).
(b)

CNV

van premisse resp. conclusie:
(b1)

CNV

van premisse:
  ≡ ((¬A B) A);
  Distributie:
  ≡ ((¬A A) (B A));
  ≡ (

$

0 (B A));
  Reductie:
  ≡ (A B);
  Conjunct destillatie:
  B
(b2)

CNV

van conclusie:
  ≡ B;
  (3) ((1) (2));
  (4) ≡

$

1 (d.i. geldig).

(9.5)
{(x A), ¬A} ¬X.
Modus Tollens.
 

CNV

van premisse:
  ≡ ((¬X A), ¬A);
  Distributie:
  ≡ ((¬X ¬A) (A ¬A));
  ≡ ((¬X ¬A)

$

0);
  Reductie:
  ≡ (¬X ¬A).
  Conjunct destillatie:
  ¬X (conclusie).

(9.6a)
{A, X, (A (X C))} C.
Regel van Algemeen sylogisme.
 

CNV

van premisse:
  ≡ (A, X, (¬A (¬X C)));
  ≡ (A, X, (¬A ¬X C));
  Reductie:
  ≡ (A, X, (¬X C));
  ≡ (A, X, C);
  Conjunct destillatie:
  C (conclusie).

(9.6b)
{(A B) (B C)} (A C).
Regel van keten redenering.
 

CNV

van premisse:
  ≡ ((¬A B) (¬B C));
  Reductie:
  (¬A C);
  ≡ (A C) (conclusie).

(9.7)
{(A B) ( B C)} (A C).
'Disjunct-implicatieregel' (via transitiviteit).
 

CNV

van premisse:
  ≡ ((A B) (¬B C));
  Reductie:
  (A C);
  ≡ (A C) (conclusie).

(9.8)
{(X Y), (X A), (Y A)} A.
Disjunctie Eliminatie regel 'v el' ('officieel').
 

CNV

van premisse:
  ≡ ((X Y), (¬X A), (¬Y A));
Route 1a:
  Conjunct-disjunct reductie:
  ((X Y) (¬X A) (¬Y A));
  ≡ (X Y ¬X A ¬Y A);
  ≡ ((

$

0) (

$

0) A);
  ≡ A;
  ≡ A (conclusie).
Route 1b:
  Distributie:
  ≡ ((X (¬X A) (¬Y A)) (Y (¬X A) (¬Y A))) (

DNV

);
  Reductie:
  ≡ ((X A (¬Y A)) ((Y (¬ X A) A));
  Conjunct eliminatie:
  ≡ ((X A) (Y A));
  Comprimatie:
  ≡ ((X Y) A);
  Conjunct destillatie:
  A;
  ≡ A (conclusie).

(9.9)
{A (A B)} (A B).
 

CNV

conversie:
  ≡ (¬(A (A B)) (A B));
  ≡ (¬(¬A (A B)) (A B));
  ≡ (¬(¬A (¬A B)) (¬A B));
  ≡ ((A ¬(¬A B)) (¬A B));
  ≡ ((A (A ¬B)) (¬A B));
  ≡ ((A A ¬B) ¬A B);
  ≡ (((A A) ¬B) ¬A B);
  Reductie:
  ≡ (((A) ¬B) ¬A B);
  ≡ ((A ¬B) ¬A B);
  ≡ ((¬B) ¬A B);
  ≡ (¬B B ¬A);
  ≡ ((¬B B) ¬A);
  ≡ ((

$

1) ¬A);
  ≡

$

1 (d.i. geldig).

(10.1)
{A (A X)} ≡ A.
(

DNV

Conjunctie eliminatie regel).
 

CNV

conversie van premisse:
  ≡ ((A A) (A X));
  Reductie:
  ≡ ((A) (A X));
  ≡ (A (A X));
  ≡ (A). (conclusie).

(10.2)
{A (¬A X))} ≡ (A X).
(

DNV

conjunct eliminatie regel).
 

CNV

van premisse:
  ≡ ((A ¬A) (A X));
  ≡ ((

$

1) (A X));
  Reductie:
  ≡ (A X) (conclusie).

(10.3a)
{A X} A.
(

CNV

Conjunct eliminatie regel).
 

CNV

conversie van gehele formule:
  ≡ (¬(A X) A);
  ≡ ((¬A ¬X) A);
  ≡ (¬A ¬X A);
  ≡ (¬A A ¬X);
  ≡ ((¬A A) ¬X);
  Reductie:
  ≡ ((

$

1) ¬X);
  ≡

$

1 (d.i. geldig).

(10.3a)[sub]
{A X} (A X).
 

CNV

conversie:
  ≡ (¬(A X) (A X));
  ≡ ((¬A ¬X) A X);
  ≡ (¬A ¬X A X);
  ≡ ((¬A A) (¬X X));
  Reductie:
  ≡ (

$

1

$

1);
  ≡

$

1 (d.i. geldig).

(10.3b)
{A} (A X).
Disjunctie introductie regel ('v in').
(Onbeperkte disjunctieve uitbreiding).
 

CNV

conversie van de gehele formule:
  ≡ (¬A (A X));
  ≡ (¬A A X);
  ≡ ((¬A A) X);
  Reductie:
  ≡ (

$

1 X);
  ≡

$

1 (d.i. geldig).

(12.1a)
{(A B) C}   ≡ ((A C) (B C)).
Distributie van conjuncte premissen.
1.

CNV

van premisse.
  ≡ (¬(A B) C);
  ≡ (¬A ¬B C).
2.

CNV

van conclusie.
  ≡ ((¬A C) (¬B C));
  ≡ ((¬A ¬C) ¬B C);
  ≡ (¬A ¬B C).
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(12.1b)
{(A B) C}   ≡ ((A C) (B C)).
Distributie van disjuncte premissen.
1.

CNV

van premisse.
  ≡ (¬(A B) C);
  ≡ ((¬A ¬B) C);
  ≡ ((¬A C) (¬B C)).
2.

CNV

van conclusie.
  ≡ ((¬A C) (¬B C)).
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(12.2a)
{A (B C)}   ≡ ((A B) (A C)).
Distributie van conjuncte conclusies.
1.

CNV

van premisse.
  ≡ (¬A (B C));
  ≡ ((¬A B) (¬A C));
2.

CNV

van conclusie.
  ≡ ((¬A B) (¬A C));
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(12.2b)
{A (B C)}   ≡ ((A B) (A C)).
Distributie van disjuncte conclusies.
1.

CNV

van premisse.
  ≡ (¬A B C);
2.

CNV

van conclusie.
  ≡ (¬A B ¬A C);
  ≡ (¬A B C);
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(13.1a)
{A (B C)} ≡ ((A B) C).
Wet van Import en export.
1.

CNV

van premisse.
  ≡ (¬A (¬B C));
  ≡ (¬A ¬B C);
2.

CNV

van conclusie.
  ≡ (¬(A B) C);
  ≡ (¬A ¬B C).
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(13.1b)
{B (A C)} ≡ ((A B) C).
Wet van Import en export.
1.

CNV

van premisse.
  ≡ ((¬B (¬A C));
  ≡ ((¬A ¬B C);
2.

CNV

van conclusie.
  ≡ (¬(A B) C));
  ≡ ((¬A ¬B) C);   ≡ ((¬A ¬B C);
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(14.1a)
{(A B) C} (A (B C)).
 

CNV

conversie:
  ≡ (¬((A B) C) (A (B C)));
  ≡ (¬(¬(A B) C) (¬A (B C)));
  ≡ (¬(¬(¬A B) C) (¬A (¬B C)));
  ≡ (¬(¬(¬A B) C) (¬A (¬B C)));
  ≡ (¬((A ¬B) C) (¬A ¬B C));
  ≡ ((¬(A ¬B) ¬C) ¬A ¬B C);
  ≡ (((¬A B) ¬C) ¬A ¬B C);
  Reductie:
  ≡ (((¬A B)) ¬A ¬B C);
  ≡ (¬A B ¬A ¬B C);
  ≡ ((¬A ¬A) (B ¬B) C);
  ≡ (¬A (

$

1) C);
  ≡

$

1 (d.i. geldig).

(14.1b)
{A (B C)}   ≡ (B (A C)).
Wet van de Commutativiteit.
1.

CNV

van premisse.
  ≡ (¬A (¬B C));
  ≡ (¬A ¬B C);
2.

CNV

van conclusie.
  ≡ (¬B (¬A C));
  ≡ (¬B ¬A C);
  ≡ (¬A ¬B C);
3. Resultaat:
  (1) ≡ (2);
  ≡

$

1 (d.i. geldig).

(14.2)
{(A B) (C D)} ((A C) (B D)).
Regel voor Compositie van deducties.

Route (a):

CNV

van premisse resp. conclusie:


1.

CNV

van premisse.
  ≡ ((¬A B) (¬C D));
2.

CNV

van conclusie:
  ≡ (¬(A C) (B D));
  ≡ (¬A ¬C (B D)) (

DNV

);
  Distributie:
  ≡ ((¬A ¬C B) (¬A ¬C D)) (

CNV

);
  ≡ (((¬A B) ¬C) ((¬C D) ¬A);
3. Resultaat:
  [Wet in

PPL

: {p} (p q).]
  [Wet in

PPL

: {p q} (p q r).]
  [Wet in

PPL

: {p q} ((p r) (q s)) (2 x disjunctieve expansie).]
  (1) (2);
  ≡

$

1 (d.i. geldig).

Route (b):  

CNV

van gehele formule:


  ≡ (¬((¬A B) (¬C D)) (¬(A C) (B D));
  ≡ ((¬(¬A B) ¬(¬C D)) ((¬A ¬C) (B D));
  ≡ ((A ¬B) (C ¬D)) ((¬A ¬C) (B D));
  ≡ ((A ¬B) (C ¬D) ¬A ¬C (B D)) (

DNV

);
  Reductie:
  ≡ ((¬B) (¬D) ¬A ¬C (B D));
  ≡ (¬B ¬D ¬A ¬C (D));
  ≡ (¬B (¬D D) ¬A ¬C);
  ≡ (¬B (

$

1) ¬A ¬C);
  ≡

$

1 (d.i. geldig).

(14.3a)
{A B} ((B A) (A B)).
 

CNV

conversie:
  ≡ (¬(¬A B) (¬(¬B A) (¬A B)));
  ≡ ((A ¬B) ((B ¬A) (¬A B)));
  ≡ ((A ¬B) (B ¬A) ¬A B) (

DNV

);
  Reductie:
  ≡ ((¬B) (B ¬A) ¬A B);
  ≡ (¬B (¬A) ¬A B);
  ≡ (¬B ¬A B);
  ≡ (¬B B ¬A);
  ≡ ((¬B B) ¬A);
  ≡ ((

$

1) ¬A);
  ≡

$

1 (d.i. geldig).

(14.3b)
{A B} ((B C) (A C)).
 

CNV

conversie:
  ≡ (¬(¬A B) (¬(¬B C) (¬A C)));
  ≡ ((A ¬B) ((B ¬C) (¬A C)));
  ≡ ((A ¬B) (B ¬C) ¬A C);
  Reductie:
  ≡ ((¬B) (B ¬C) ¬A C);
  ≡ (¬B (B) ¬A C);
  ≡ ((

$

1) ¬A C);
  ≡

$

1 (d.i. geldig).