Methode:Formele Logica©InleidingLogische bewijsvoeringBewijsmethoden in de logica |
Analyse in conjunctief normaal vorm (CNF
).
Bij 'negatieve' bewijsvoering is het doel om tenminste één voldoende voorwaarde te vinden voor de onwaarheid c.q. ongeldigheid van een verzameling van te weerleggen beweringen of redeneringen (die zoals gezegd het tegendeel c.q. complement vormt van de verzameling van te bewijzen beweringen, c.q. de theorie). We zoeken daarom in deze verzameling minstens twee deelverzamelingen die in conjunctie een contradictie vormen, waardoor de gehele complementaire verzameling weerlegd wordt. Voor dat doel is het handig om de gehele complementaire verzameling eerst om te zetten in een conjunctie van disjuncties, oftewel een conjunctief normaal vorm (
CNF
).3. Bewijsmethoden naar inhoud en structuur
3.1. Semantisch bewijs.
Bewijs van algemene logische geldigheid van een relatie tussen elementen.
Bijv. volgens de waarheidswaardentabellenmethode (positief bewijs), de boommethode (negatief bewijs), enz..
Bijv. volgens de waarheidswaardentabellenmethode (positief bewijs), de boommethode (negatief bewijs), enz..
3.2. Syntactisch bewijs.
Bewijs van logische afleidbaarheid van een ordeningspatroon.
Bijv. volgens de methode van natuurlijke deductie (positief bewijs), de resolutiemethode (negatief bewijs), enz..
Bijv. volgens de methode van natuurlijke deductie (positief bewijs), de resolutiemethode (negatief bewijs), enz..
4. Bewijsmethoden met toenemende reikwijdte
4.1. Bewijsmethoden - voor de propositielogica (PPL
).
(4.1a)
Oftewel de methode Schröder-Peirce.
We beschouwen elke elementaire bewering of propositie als logische variabele, en gaan uit van het bereik van mogelijke waarden voor die variabele (het meest efficiënt is binair, bijvoorbeeld {waar, onwaar}, {ja, nee}, {aan, uit}, {intern, extern}, (0, 1}, enz.). We hanteren een aantal regels voor de waarden die samengestelde propositie s, op basis van logische voegwoorden (operatoren, connectieven), met die combinaties van proposities aannemen. Dan bekijken we de verzameling van alle propositienamen in de formule, en deze ordenen we lexicografisch (naar lengte resp. alfabet). We maken een tabel met in de kolommen eerst de enkelvoudige (atomaire) propositienamen en als rijen alle mogelijke combinaties van waarheidswaarden die de proposities kunnen hebben. In de rechterkolommen vullen we de samengestelde (complexe) proposities in, tot en met de gehele formule. Uiteindelijk blijkt in deze laatste kolom op wat voor waarheidswaardepatroon de formule uitkomt: geldig, contingent of onvervulbaar.
Conjunctief normaal vorm van Implicatie.
{(A
B)} ≡ (¬A 
B).
(9.4c) Regel van Algemeen modus ponens.
Substitutie via Implicatie.
(9.4c.1) Bewijs via 'bevestigende wijs'.
Sluitrede, Modus ponens (MP), 'Material detachment'.
{(A B), A} B.
(4.1b)
Oftewel Convergente reductiemethode.
Dit is een variant van de axiomatische methode. Hierbij vindt herleiding plaats van een formule tot haar waarheidswaarde, of als dit niet lukt tot de meest eenvoudige, equivalente, niet verder reduceerbare variant ervan. Dit door omzetting via parafrasetransformatie naar een conjunctie van disjuncties (conjunctief normaal vorm, CNV), en vervolgens vereenvoudiging daarvan (parafrasereductie). De bedoeling is dat de CNV formule wordt teruggebracht (gereduceerd) tot de meest eenvoudige vorm die direct afleidbaar is uit de premisse (n): met volledig behoud van logische kracht, oftewel parafrase van de conclusie.
In
Methode van Waarheidswaardentabellen.
Oftewel de methode Schröder-Peirce.
We beschouwen elke elementaire bewering of propositie als logische variabele, en gaan uit van het bereik van mogelijke waarden voor die variabele (het meest efficiënt is binair, bijvoorbeeld {waar, onwaar}, {ja, nee}, {aan, uit}, {intern, extern}, (0, 1}, enz.). We hanteren een aantal regels voor de waarden die samengestelde propositie s, op basis van logische voegwoorden (operatoren, connectieven), met die combinaties van proposities aannemen. Dan bekijken we de verzameling van alle propositienamen in de formule, en deze ordenen we lexicografisch (naar lengte resp. alfabet). We maken een tabel met in de kolommen eerst de enkelvoudige (atomaire) propositienamen en als rijen alle mogelijke combinaties van waarheidswaarden die de proposities kunnen hebben. In de rechterkolommen vullen we de samengestelde (complexe) proposities in, tot en met de gehele formule. Uiteindelijk blijkt in deze laatste kolom op wat voor waarheidswaardepatroon de formule uitkomt: geldig, contingent of onvervulbaar.
{Naar: Benjamin Peirce (1809-1880), Friedrich Wilheml Karl Ernst Schröder (1841-1902), e.a..}
Voorbeelden.
Conjunctief normaal vorm van Implicatie.
{(A
B)} ≡ (¬A B).| (1) | (2) | (3) | (4) | (5) | (6) |
| A | B | ¬(1) | (3
2) | (1
2) | (4
 5) |
| 1 | 1 | 0 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 0 | 1 |
| 0 | 1 | 1 | 1 | 1 | 1 |
| 0 | 0 | 1 | 1 | 1 | 1 |
Substitutie via Implicatie.
(9.4c.1) Bewijs via 'bevestigende wijs'.
Sluitrede, Modus ponens (MP), 'Material detachment'.
{(A
B), A} B.| (1) | (2) | (3) | (4) | (5) | (6) | (7) |
| A | B | (1 2)
| (1  3) |
(1 2) |
(4 5) |
(6 2) |
| 1 | 1 | 1 | 1 | 1 | 1 | 1 |
| 1 | 0 | 0 | 0 | 0 | 0 | 1 |
| 0 | 1 | 1 | 0 | 0 | 0 | 1 |
| 0 | 0 | 1 | 0 | 0 | 0 | 1 |
(4.1b)
Methode van Parafrasereductie naar waarheidswaarde.
Oftewel Convergente reductiemethode.
Dit is een variant van de axiomatische methode. Hierbij vindt herleiding plaats van een formule tot haar waarheidswaarde, of als dit niet lukt tot de meest eenvoudige, equivalente, niet verder reduceerbare variant ervan. Dit door omzetting via parafrasetransformatie naar een conjunctie van disjuncties (conjunctief normaal vorm, CNV), en vervolgens vereenvoudiging daarvan (parafrasereductie). De bedoeling is dat de CNV formule wordt teruggebracht (gereduceerd) tot de meest eenvoudige vorm die direct afleidbaar is uit de premisse (n): met volledig behoud van logische kracht, oftewel parafrase van de conclusie.
In
PDL
-I zijn vaak 'ad hoc' interpretaties nodig van variabelen (d.i. instantiaties) om kwantoren weg te werken - via Skolem normalisatie - en om de laatste stap van de premisse(n) naar de conclusie te kunnen maken.Voorbeelden.
(9.4) {(A B) A}
B.
Modus ponens.
Implicatie Eliminatie regel, '> el'.
B) A}
B.Modus ponens.
Implicatie Eliminatie regel, '> el'.
(a)
≡ ((¬(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) (
Distributie:
≡ ((A ¬A B)
(¬B ¬A B)) (
≡ (((A ¬A) B)
(¬B ( B) ¬A));
Reductie:
≡ ((( B) (( ¬A));
≡ (( (
≡
(b)
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)
≡ ((¬A B) A);
Distributie:
≡ ((¬A A) (B
A));
≡ ( (B A));
Reductie:
≡ (A B);
Conjunct destillatie:
B
(b2)
≡ B;
(3) ((1) (2));
(4) ≡
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).4.2. Bewijsmethoden - voor de predikatenlogica, van de eerste orde (PDL
-I).
(D.w.z. ook voor
PPL
)
(4.2a)
Herleiding, of axiomatische methode.
Herleiding van een aantal formules tot een bepaalde conclusie, via een aaneenschakeling van tussenstappen. Dit met behulp van een beperkte verzameling van hulpstellingen in de vorm van logische wetten (axioma 's, d.i. bewezen theorema's). De verbindingen tussen 'schakels' en hulpstellingen berusten typisch op substitutie wetten (m.n. modus ponens).
[D3] (MP)
(4.2b)
Oftewel Natural deduction. Doelgerichte afleiding van een formule uit een gegeven verzameling formules. (naar G. Gentzen, 1934; F.B. Fitch, 1952).
De structuur van het bewijs bestaat uit een hoofdlijn van redenering, waarop elementaire conjuncten (unit clauses ) en eventuele disjuncties worden geplaatst, de laatste in de vorm van geneste redeneerlijnen (subderivaties).
Afleiding vindt plaats met behulp van een beperkte, vaste verzameling van afleidingsregels (per connectief één regel voor introductie en één regel voor eliminatie).
Implicatie eliminatie regel, '> el' (volgens modus ponens).
(4.2c)
Een klassieke variant van de reductiemethode is 'Herbrand logica' (J. Herbrand, 1931). Hierbij wordt uitsluitend van domeininterpretaties gebruik gemaakt waarbij alle variabelen worden vervangen door object constanten, zgn. ' grondsubstituties'.
Zie hieronder, (4.2d) 'Methode van Minimaal domein definitie'.
(4.2d)
Een praktische combinatie van Convergente reductiemethode en Herbrand interpretatie, die geschikt is voor predikatenlogica, vind je in de Minimaal domein definitie bewijsmethode.
Modus ponens (MP), in
D.w.z. met factieve premisse (referent) existentieel.
(4.2e)
Oftewel Tableaumethode, boomdiagram-methode.
Toetsing van de geldigheid van een redenering door weerlegging van de onvervulbaarheid van het tegendeel.
Met name wordt onderzocht of er contradictie schuilt tussen de premisse(n) en het tegendeel van de conclusie. Voor dit doel worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht, waarna de disjuncties worden uitgesplitst in hun disjuncten, een 'tak' per disjunct. De bedoeling is om in de complementaire conclusie minstens één conjunct te vinden waarvan elke disjuncte 'tak' strijdig is met elke disjuncte 'tak' van minstens één conjunct in de premisse(n). In dat geval blijkt contradictie tussen conjuncten van complementaire conclusie en van premisse(n). Daarmee is onvervulbaarheid van het tegendeel aangetoond, dus geldigheid van de te toetsen bewering.
(4.2f)
Deze methode is gebaseerd op het principe van toetsing van de te bewijzen redenering via weerlegging van het tegendeel, door het afleiden van een uitzondering of tegenvoorbeeld van het tegendeel. (reductio ad absurdum). Ook hier worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht. Hieruit wordt vervolgens een verzameling van kwantor-vrije, Skolem-normaal conjuncten afgeleid (de clause set). Doel is afleiding van minstens één lege verzameling conjuncten op de hoofdlijn van redenering, uit complementair e conjuncten in conclusie en in premisse(n). Van elk van die conjuncten is minstens één consequentie, afgeleide of interpretatie nodig. Hierbij kan gebruik worden gemaakt van regels voor reductie, resolutie en (in
Bewijs via resolutie (in
Methode van Axiomatische bewijs voering.
Herleiding, of axiomatische methode.
Herleiding van een aantal formules tot een bepaalde conclusie, via een aaneenschakeling van tussenstappen. Dit met behulp van een beperkte verzameling van hulpstellingen in de vorm van logische wetten (axioma 's, d.i. bewezen theorema's). De verbindingen tussen 'schakels' en hulpstellingen berusten typisch op substitutie wetten (m.n. modus ponens).
{Zie o.a.: Bertrand Russell (1903): 'Principles of mathematics', London: Norton, 1903.
Bertrand Russel & Alfred North Whitehead (1910, 1912, 1913): 'Principia Mathematica', 3 volumes, 1910 (Vol. 1), 1912 (Vol. 2), 1913 (Vol. 3). England, Cambridge: Cambridge University Press. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Cambridge: Cambridge University Press.}
Bertrand Russel & Alfred North Whitehead (1910, 1912, 1913): 'Principia Mathematica', 3 volumes, 1910 (Vol. 1), 1912 (Vol. 2), 1913 (Vol. 3). England, Cambridge: Cambridge University Press. Second edition, 1925 (Vol. 1), 1927 (Vols 2, 3). Cambridge: Cambridge University Press.}
Voorbeelden.
[D3] (MP)
Modus ponens.
{ (K* 
F )
(Ks* 
K* )
( (Ks* (F
G ) );
( (Ks* G )
(F G ) );
( (Ks* G ) )
(K* G ) );
((K* 
Ks*)
G ) ) ) ) }.
{ ( (F G )
F )
G }.
F )(Ks* K* ) ( (Ks* (F
G ) ); ( (Ks* G )
(F G ) ); ( (Ks* G ) )
(K* G ) );((K* Ks*)
G ) ) ) ) }.{ ( (F G )F )G }.(4.2b)
Methode van Natuurlijke deductie
Oftewel Natural deduction. Doelgerichte afleiding van een formule uit een gegeven verzameling formules. (naar G. Gentzen, 1934; F.B. Fitch, 1952).
De structuur van het bewijs bestaat uit een hoofdlijn van redenering, waarop elementaire conjuncten (unit clauses ) en eventuele disjuncties worden geplaatst, de laatste in de vorm van geneste redeneerlijnen (subderivaties).
Afleiding vindt plaats met behulp van een beperkte, vaste verzameling van afleidingsregels (per connectief één regel voor introductie en één regel voor eliminatie).
{Zie o.a.: G. Gentzen (1934): 'Untersüchungen uber das logische Schließßen',
Mathematische Zeitschrift 39: pp.176-210, 405-431. In the French translation:
'Récherches sur la déduction logique, 1955.
F.B. Fitch (1952): 'Symbolic Logic. An Introduction'. New York, Ronald Press.}
F.B. Fitch (1952): 'Symbolic Logic. An Introduction'. New York, Ronald Press.}
Voorbeelden.
Implicatie eliminatie regel, '> el' (volgens modus ponens).
{X, (X A)} A.
Voorbeeld ' el': (basisvorm):
(1) | A B;
(2) | A;
(3) | {* (1),(2), ' el' } B.
A)} A.Voorbeeld '
el': (basisvorm):(1) | A
B;(2) | A;
(3) | {* (1),(2), '
el' } B.(4.2c)
Methode volgens Herbrand interpretatie.
Een klassieke variant van de reductiemethode is 'Herbrand logica' (J. Herbrand, 1931). Hierbij wordt uitsluitend van domeininterpretaties gebruik gemaakt waarbij alle variabelen worden vervangen door object constanten, zgn. ' grondsubstituties'.
{Zie o.a.:
Jacques Herbrand (1931): 'Sur la non-contradiction de l'arithmétique', Journal für die reine und angewandte Mathematik 166: pp.1-8, translated as 'On the consistency of arithmetic' in Van Heijenoort's 'From Frege to Godel'.}
Jacques Herbrand (1931): 'Sur la non-contradiction de l'arithmétique', Journal für die reine und angewandte Mathematik 166: pp.1-8, translated as 'On the consistency of arithmetic' in Van Heijenoort's 'From Frege to Godel'.}
Voorbeelden.
Zie hieronder, (4.2d) 'Methode van Minimaal domein definitie'.
(4.2d)
Methode van Minimaal domein definitie.
Een praktische combinatie van Convergente reductiemethode en Herbrand interpretatie, die geschikt is voor predikatenlogica, vind je in de Minimaal domein definitie bewijsmethode.
Voorbeelden.
Modus ponens (MP), in PDL
; Existentieel normaal vorm'.
D.w.z. met factieve premisse (referent) existentieel.
F1: {(
x (A[1](x) B[1](x))
x A[1](x) };
F2: (x B[1](x) };
F1 [DNF] ={(x (¬A[1](x) B[1](x
)) x A[1](x) };
F1(M!): [DNF(Intens.)] ={((¬A1
F1(M!): DNF(Extens.)] ={((¬A1
={(¬A1
={((¬A1), (¬A2
={(¬A1, ¬A2, A1)
F1(M!): [DNF(Reduc.)] ={ (B1, ¬A2, A1)
F2(M!): [DNF(Intens.)] ={(By[c])};
F2(M!): [DNF(Extens.)] ={(B1
F1(M!), de premisse,
bestaat uit 8 componenten/disjuncten van elk 3 conjuncten, vier hiervan blijken te elimineren; de resterende vier
impliceren de conclusie, F2(M!).
x (A[1](x) B[1](x))
x A[1](x) };
F2: (x B[1](x) };F1 [DNF] ={(
x (¬A[1](x) B[1](x
)) x A[1](x) };F1(M!): [DNF(Intens.)] ={((¬A1
/
B1), (¬A2/
B2)), (Ax[c]) };F1(M!): DNF(Extens.)] ={((¬A1
/
B1), (¬A2/
B2)), ((A1)/
(A2)) };={(¬A1
/
B1), (¬A2/
B2), (A1))/
(¬A1/
B1), (¬A2/
B2), (A2)) };={((¬A1), (¬A2
/
B2), (A1))/
((B1), (¬A2/
B2), (A1))/
((¬A1), (¬A2/
B2), (A2))/
((B1), (¬A2/
B2), (A2)) };={(¬A1, ¬A2, A1)
/
(¬A1, (B2, A1)/
(B1, ¬A2, A1)/
(B1, B2, A1)/
(¬A1, ¬A2, A2)/
(¬A1, B2, A2)/
(B1, ¬A2, A2)/
(B1, B2, A2) };F1(M!): [DNF(Reduc.)] ={ (B1, ¬A2, A1)
/
(B1, B2, A1)/
(¬A1, B2, A2)/
(B1, B2, A2) };F2(M!): [DNF(Intens.)] ={(By[c])};
F2(M!): [DNF(Extens.)] ={(B1
/
B2) };F1(M!), de premisse,
bestaat uit 8 componenten/disjuncten van elk 3 conjuncten, vier hiervan blijken te elimineren; de resterende vier
impliceren de conclusie, F2(M!).(4.2e)
Methode van Semantische tableaux
Oftewel Tableaumethode, boomdiagram-methode.
Toetsing van de geldigheid van een redenering door weerlegging van de onvervulbaarheid van het tegendeel.
Met name wordt onderzocht of er contradictie schuilt tussen de premisse(n) en het tegendeel van de conclusie. Voor dit doel worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht, waarna de disjuncties worden uitgesplitst in hun disjuncten, een 'tak' per disjunct. De bedoeling is om in de complementaire conclusie minstens één conjunct te vinden waarvan elke disjuncte 'tak' strijdig is met elke disjuncte 'tak' van minstens één conjunct in de premisse(n). In dat geval blijkt contradictie tussen conjuncten van complementaire conclusie en van premisse(n). Daarmee is onvervulbaarheid van het tegendeel aangetoond, dus geldigheid van de te toetsen bewering.
{Zie o.a.:
Evert W. Beth, 1959, 'The foundations of mathematics. A study in the philosophy of science'. Ophelders, Willy (W.M.J.), 'Automated theorem proving based upon a tableau-method with unification under restrictions. Theory, implementation and results'. Proefschrift (KUB, Tilburg), 5-6-1992: p.14.}
Evert W. Beth, 1959, 'The foundations of mathematics. A study in the philosophy of science'. Ophelders, Willy (W.M.J.), 'Automated theorem proving based upon a tableau-method with unification under restrictions. Theory, implementation and results'. Proefschrift (KUB, Tilburg), 5-6-1992: p.14.}
(4.2f)
Resolutie.
Deze methode is gebaseerd op het principe van toetsing van de te bewijzen redenering via weerlegging van het tegendeel, door het afleiden van een uitzondering of tegenvoorbeeld van het tegendeel. (reductio ad absurdum). Ook hier worden de premisse(n) en de negatie van de conclusie tezamen in een conjunctief normaal vorm gebracht. Hieruit wordt vervolgens een verzameling van kwantor-vrije, Skolem-normaal conjuncten afgeleid (de clause set). Doel is afleiding van minstens één lege verzameling conjuncten op de hoofdlijn van redenering, uit complementair e conjuncten in conclusie en in premisse(n). Van elk van die conjuncten is minstens één consequentie, afgeleide of interpretatie nodig. Hierbij kan gebruik worden gemaakt van regels voor reductie, resolutie en (in
PDL
-I) unificatie.
{Zie o.m. Davis & Putnam (1960), John Alan Robinson (1965), N.J. Nilsson (1980), Alexander A. Leitsch (1997).}
{Zie ook:
Bewijsmethode voor Predikatenlogica: Inleiding Resolutielogica .
En meer daarover: de Resolutiemethode (uitgebreid). }
Bewijsmethode voor Predikatenlogica: Inleiding Resolutielogica .
En meer daarover: de Resolutiemethode (uitgebreid). }
Voorbeelden.
Bewijs via resolutie (in PPL
).
Gegeven formule R:
R = {((A B) A)
B }.
Modus ponens.
Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie:
Formule R is resolutie-beslisbaar geldig.
R = {((A
B) A)
B }.Modus ponens.
Implicatie Eliminatie regel, '> el'.
Bewijs via resolutie:
•
S ≡ ¬R;
S = {¬(((A B) A)
B) }.
Formule S is beslist onvervulbaar.
Aanname van het tegendeel S:
S ≡ ¬R;S = {¬(((A B) A)
B) }.
•
· Negatief normaal vorm;
· Conjunctief normaal vorm:
{((A B) A)
¬B };
{(¬A B) A
¬B }.
· Clausule Normaal Vorm:
{ 1:A, 2:¬B, 3:(¬A B) }.
Sluit (in contradictie).
Normaal vorm conversies:
· Negatief normaal vorm;
· Conjunctief normaal vorm:
{((A B) A)
¬B };{(¬A B) A
¬B }.{ 1:A, 2:¬B, 3:(¬A B) }.
•
Pad (a):
{1,3} 4:B; {2,4} 5:
.
Pad (b):
{1,3} 4:¬A; {1,4} 5:
.
Reductie(s):
Pad (a):
{1,3}
4:B; {2,4} 5:
.Pad (b):
{1,3}
4:¬A; {1,4} 5:
.Sluit (in contradictie).Formule S is beslist onvervulbaar.Formule R is resolutie-beslisbaar geldig.