»
In de predikatenlogica (
In bewijsmethoden voor de
Wat we voor dat laatste eerst nodig hebben voor de - te bewijzen -
Vervolgens kunnen we de minimaal domeindefinitie (MDD) bepalen voor de formule: dat is de minimaal domein selectie die tenminste nodig is, maar ook niet meer dan nodig, om de formule geldig te doen zijn op logische gronden.
Het zal duidelijk zijn dat er meerdere syntactische structuren kunnen zijn die verwijzen naar één unieke semantische structuur. Ook is duidelijk dat logisch welgevormde expressies onderling logisch equivalent zijn als ze verwijzen naar een identieke semantische structuur. Tegelijk is duidelijk dat elke afzonderlijke minimaal domeindefinitie verwijst naar precies één semantische structuur - ongeacht mogelijke syntactische structuren c.q. welgevormde formules die eraan verbonden kunnen worden. Hieruit volgt dat bij elke welgevormde logische expressie precies één minimaal domeindefinitie bestaat. Uiteraard kan een enkele minimaal domeindefinitie weer met allerlei verschillende symbolen en notaties worden uitgedrukt.
De minimaal domein definitiemethode berust op het principe dat formules geldig zijn indien de minimaal domein definitie voor de premisse(n) tenminste de minimaal domeindefinitie voor de conclusie(s) impliceert; en dit op logische gronden (deze geldigheid is dus niet beperkt tot inclusie relaties tussen de bijbehorende verzamelingen: het accepteert ook disjunctieve expansie van de premisse(n)).
Hieronder volgen eerst de elementaire vormen van gekwantificeerde predicaties met hun afgeleide propositievormen, zowel de expliciete als impliciete (Skolem) vormen.
D[m]* : domein (Dmn) m met onbepaalde omvang (kardinaliteit, aantal elementen).
D[m]n1 : domein m met n1 elementen, of elementaire objecten a[m,i], in
D[m]n1 = { a[m,1], a[m,2], .. a[m,n1]
}.
Bijv. D[m]5 = { a,b,c,d,e }.
P[q]n2 : verzameling q met n2 n3[q,r]-plaatsige predikaten A[q,r] n3 in
Notatie:
P[q]n2 = { A[q,1]n3[q,1], A[q,2]
n3[q,2], .. A[q,n2]n3[q,n2] }.
Bijv. P[1]3 = { A(x), B(y,z), C(u,v,w) }.
K[k]n4 : verzameling k met n4 welgevormde formules (WFF) F[k,h] in
Notatie:
K[k]n4 = { F[k,1], F[k,2], .. F[k,n4]
}.
Bijv. K[1]2 = { (A(x)
B(a,z)), C(c,v,e) }.
In dit geval gaan we om het eenvoudig te houden uit van een verzameling K[k]n4 van louter formules
met de volgende eigenschappen:
{ k,q,m | 
h 
r
i ((F[k,h] 
K[k]n4
) 
((A[q,r] P[q]n2
)
((x[m,i] D[m]n1
) (F[k,h] 
A[q,r](x
[m,i])) )i,r,h,m,q,k }.
Bijv. K[k]3 = { (A1(x), A2(x), A3(x) }.
We nemen hiervoor de produktverzameling van D[m]n1 en K[k]n4.
Notatie:
{ m,k | G![m,k]n5 = D[m]n1 X K[k]
n4 }.
Deze verzameling bestaat uit alle mogelijke correcte instantiaties van de n4 formules F[k,h]
uit K[k]n4 onder interpretatie naar domein D[m]n1 in termen van al zijn
n1 grondobjecten a[i]. Het resultaat komt neer op een verzameling van n5 (= n1*n4)
welgevormde grondinstanties, in de vorm van grondatomen oftewel, in
Notatie:
{ m,k,q | G![m,k]n5 = {
{A[q,1](a[1], A[q,1](a[2], .. A[q,1](a[n1] ) },
{A[q,2](a[1], A[q,2](a[2], .. A[q,2](a[n1] ) },
..
{A[q,n2](a[1], A[q,n2](a[2], .. A[q,n2](a[n1] ) } } }.
Bijv. { G![m,k]15 = {
{A1(a),A1(b),A1(c),A1(d),A1(e)},
{A2(a),A2(b),A2(c),A2(d),A2(e)},
{A3(a),A3(b),A3(c),A3(d),A3(e)} } }.
Hebben we eenmaal een domein gekozen - al is het maar arbitrair c.q. per definitie - dan kunnen we gekwantificeerde beweringen in
Als we de geldigheid van een redenering willen bewijzen moeten we in het algemeen aantonen dat de premisse(n) voldoende voorwaarde vormen voor (de vervulling van) de conclusie(s). In de minimaal domein selectiemethode moeten we kijken of de minimaal domein definitie van de premisse(n) voldoende grond vormt voor de minimaal domein definitie van de conclusie(s). Oftewel, de tweede dient (eindig) afleidbaar te zijn uit de eerste.
Dit kunnen we het gemakkelijkste toetsen door de minimaal domein definities van beide componenten in een gestandaardiseerde vorm te zetten: met name een disjunctie van één of meer disjuncten (nl. conjuncties): de Disjunctief Normaal Vorm (DNF). De gezochte afleidingsrelatie geldt dan indien geldt:
Nu eerst wat van het bovenstaande formeel weergeven om te weten wat we zeggen, eigenlijk, dus in logische vorm:
Gegeven twee formules, zeg {F[k,h1], F[k,h2]}; met voor elk een bijbehorende welgevormde minimale domeindefinitie, zeg {MD[m,h1], MD[m,h2]}; geldt:
We kunnen nu de bovenstaande principes en notaties gaan toepassen om logische relaties uit te drukken (of te interpreteren) in termen van domeinselecties, maar ook om de logische relaties tussen logische relaties te toetsen, met name op logische geldigheid.
We stappen daarvoor eerst over naar iets complexere formules, nl. twee- of meerplaatsige predicaties. Het eerste waar we dan goed begrip van moeten krijgen is de exacte interpretatie van inter-kwantorrelaties, dat wil zeggen, hoe combinaties van verschillende kwantoren op uiteenlopende manieren de selectie van objecten kunnen bepalen.
We nemen als eerste de combinatie van één existentiëler en één universele kwantor. Dan hebben we uiteraard twee mogelijke volgordes, elk met een heel eigen betekenis.
De algemene relaties zijn als volgt:
We zullen deze relaties bewijzen via twee stappen: door eerst de minimale domeindefinities te bepalen, en vervolgens de relaties tussen deze definities te specificeren.
We zien aan het bovenstaande dat F1 en F2 op twee belangrijke eigenschappen verschillen:
Hoewel dus de afleidingsrelatie valt te beredeneren op grond van de Skolem-vormen van de formules, wordt de precieze bewijsgrond daarmee niet direct zichtbaar.
De minimaal domeindefinities laten echter onmiddellijk zien hoe de implicatierelaties liggen tussen componenten ( conjuncties in de disjuncten) van F1 en F2. Daaruit wordt duidelijk: elke disjunct in F1 kent een disjuncte afgeleide in F2. Dus F1 levert voldoende voorwaarde voor F2.
Bijvoorbeeld de twee formules:
Vraag is of er een afleidingsrelatie is van F1 naar F2: levert F1 voldoende grond voor F2?
We toetsen dit door de minimaal domeinselecties met elkaar te vergelijken.
Te bewijzen staat dus:
(F1: {((A1,A2), (B1.1,B2.1)) /((A1,A2), (B1.2,B2.2))}
F2: {(A1,A2) /(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2) } ).
F1 en F2 zijn beide met behulp van minimaal domeindefinities te parafraseren in extensieve DNF vorm.
Wat blijkt? Elke disjunct in F1 heeft een afgeleide disjunct in F2.
Daarmee is de stelling bewezen.
Methode 'Praktische Logica':
Bewijsmethode voor Predikatenlogica
:De Minimaal domein definitie-methode.
1.
Inleiding.
In de predikatenlogica (
PDL
) wordt de bewijsvoering, met name van de geldigheid van redeneervormen, een stuk complexer dan in de propositielogica. Dit komt vooral door het gebruik van kwantoren, zoals bekend de universele en de existentiële kwantor, die zowel in expliciete als impliciete (Skolem) vorm kunnen voorkomen.In bewijsmethoden voor de
PDL
worden in het algemeen dan ook strategieën gevolgd en technieken geboden voor de eliminatie van de kwantoren door reductie van gekwantificeerde predicaties tot kwantorvrije expressies, die in wezen dus propositievormen zijn. Het laatste blijkt inPDL
-I mogelijk doordat alle enkelvoudige oftewel atomaire predicaties met kwantoren semantisch kunnen worden geïnterpreteerd als min of meer complexe propositieformules (en vervolgens dus ook weer syntactisch kunnen worden gerepresenteerd in die vormen).Wat we voor dat laatste eerst nodig hebben voor de - te bewijzen -
PDL
formule is een minimaal domein selectie (MDS): d.w.z. een beschrijving van een willekeurig domein dat voldoende omvangrijk en complex is om de logisch-semantische structuur van dePDL
formule volledig te kunnen weergeven.Vervolgens kunnen we de minimaal domeindefinitie (MDD) bepalen voor de formule: dat is de minimaal domein selectie die tenminste nodig is, maar ook niet meer dan nodig, om de formule geldig te doen zijn op logische gronden.
Het zal duidelijk zijn dat er meerdere syntactische structuren kunnen zijn die verwijzen naar één unieke semantische structuur. Ook is duidelijk dat logisch welgevormde expressies onderling logisch equivalent zijn als ze verwijzen naar een identieke semantische structuur. Tegelijk is duidelijk dat elke afzonderlijke minimaal domeindefinitie verwijst naar precies één semantische structuur - ongeacht mogelijke syntactische structuren c.q. welgevormde formules die eraan verbonden kunnen worden. Hieruit volgt dat bij elke welgevormde logische expressie precies één minimaal domeindefinitie bestaat. Uiteraard kan een enkele minimaal domeindefinitie weer met allerlei verschillende symbolen en notaties worden uitgedrukt.
De minimaal domein definitiemethode berust op het principe dat formules geldig zijn indien de minimaal domein definitie voor de premisse(n) tenminste de minimaal domeindefinitie voor de conclusie(s) impliceert; en dit op logische gronden (deze geldigheid is dus niet beperkt tot inclusie relaties tussen de bijbehorende verzamelingen: het accepteert ook disjunctieve expansie van de premisse(n)).
2.
Kwantificatie: syntax en semantiek.
Hieronder volgen eerst de elementaire vormen van gekwantificeerde predicaties met hun afgeleide propositievormen, zowel de expliciete als impliciete (Skolem) vormen.
2.1.
Syntax: formele notaties.
1. Verzameling objecten (Domein):
D[m]* : domein (Dmn) m met onbepaalde omvang (kardinaliteit, aantal elementen).
D[m]n1 : domein m met n1 elementen, of elementaire objecten a[m,i], in
PDL
-I. Notatie:D[m]n1 = { a[m,1], a[m,2], .. a[m,n1]
}.Bijv. D[m]5 = { a,b,c,d,e }.
2. Verzameling predikaten:
P[q]n2 : verzameling q met n2 n3[q,r]-plaatsige predikaten A[q,r] n3 in
PDL
-I.Notatie:
P[q]n2 = { A[q,1]n3[q,1], A[q,2]
n3[q,2], .. A[q,n2]n3[q,n2] }.Bijv. P[1]3 = { A(x), B(y,z), C(u,v,w) }.
3. Verzameling formules (Theorie):
K[k]n4 : verzameling k met n4 welgevormde formules (WFF) F[k,h] in
PDL
-I.Notatie:
K[k]n4 = { F[k,1], F[k,2], .. F[k,n4]
}.Bijv. K[1]2 = { (A(x)
B(a,z)), C(c,v,e) }.
(a)
Deze verzameling K[k]n4 bestaat uit enkelvoudige formules F[k,h]. Dat zijn formules met precies één elementaire bewering c.q. propositie, ook atomen genoemd, oftewel, in
D.w.z. hier geldt
Bovendien nemen we hier voor het gemak aan dat het louter éénplaatsige formules betreft: dus elk bestaande uit precies één predicatie met ariteit één: P1(x). D.w.z. hier geldt
Notatie:Complexiteit.
Deze verzameling K[k]n4 bestaat uit enkelvoudige formules F[k,h]. Dat zijn formules met precies één elementaire bewering c.q. propositie, ook atomen genoemd, oftewel, in
PDL
: predicaties (bestaand uit predikaten toegekend aan een cluster domeinelementen). Atomaire formules bevatten dus geen connectieven.D.w.z. hier geldt
{ k, q | (n4 =n2)q,k }.
(b) Ariteit.
Bovendien nemen we hier voor het gemak aan dat het louter éénplaatsige formules betreft: dus elk bestaande uit precies één predicatie met ariteit één: P1(x). D.w.z. hier geldt
{ q | r (n3[q,r] =1)r,q }.
r (n3[q,r] =1)r,q }.{ k,q,m | h r
i ((F[k,h] K[k]n4
) ((A[q,r] P[q]n2
)((x[m,i] D[m]n1
) (F[k,h] A[q,r](x
[m,i])) )i,r,h,m,q,k }.Bijv. K[k]3 = { (A1(x), A2(x), A3(x) }.
4. Verzameling grondpredikaties:
We nemen hiervoor de produktverzameling van D[m]n1 en K[k]n4.
Notatie:
{ m,k | G![m,k]n5 = D[m]n1 X K[k]
n4 }.PDL
-I, grondpredikaties van K[k]n4 onder D[m]n1.
{Vergelijk zgn. Herbrand interpretatie, binnen de 'Herbrand logica' (J. Herbrand, 1931).
een klassieke variant van de reductiemethode voor de
PDL
. }{ m,k,q | G![m,k]n5 = { {A[q,1](a[1], A[q,1](a[2], .. A[q,1](a[n1] ) },
{A[q,2](a[1], A[q,2](a[2], .. A[q,2](a[n1] ) },
..
{A[q,n2](a[1], A[q,n2](a[2], .. A[q,n2](a[n1] ) } } }.
Bijv. { G![m,k]15 = {
{A1(a),A1(b),A1(c),A1(d),A1(e)},
{A2(a),A2(b),A2(c),A2(d),A2(e)},
{A3(a),A3(b),A3(c),A3(d),A3(e)} } }.
2.2.
Semantiek: domeinverwijzingen.
Universele en existentiële referenties.
Hebben we eenmaal een domein gekozen - al is het maar arbitrair c.q. per definitie - dan kunnen we gekwantificeerde beweringen in
PDL
-I in termen van dat domein interpreteren (d.w.z. aan de syntactische structuur een semantische structuur toekennen). Dit betekent ook dat we de typische elementaire kwantor-expressies inPDL
-I voldoende eenduidig, exact en correct in termen van domeinselecties kunnen definiëren.1. Kwantoren (expliciet).
(1a) '':
Impliceert onder de gerelateerde variabelenaam een selectie van conjuncte domein-objecten.
(
A(x[2]) .. A(x[n])
}.
Of, met prefix notatie:
(
(i:=1,..n) { A(x[i]) } }.
En representeert bij n objecten a[i] een domeinselectie met de datastructuur:
(ref) { A(a[1]) A(a
[2]) .. A(a[n]) }.
Of, met simpele notatie:
(ref) {A(a[1] + a[2] + .. a[n]
) }.
Of, kort en praktisch:
(ref) {A1, A2, .. An}.
(1b) '':
Impliceert onder de gerelateerde variabelenaam een selectie van disjuncte domein-objecten.
(A(x[2]) .. A(x[n])
}.
Of, met prefix notatie:
(
(i:=1,..n) { A(x[i]) } }.
En representeert bij n objecten a[i] een domeinselectie met de structuur:
(ref) {A(a[1]) A(a
[2]) .. A(a[n]) }.
(zgn. Herbrand disjunction).
Of met kortere notatie:
(ref) {A(a[1] / a[2] / .. a[n]
) }.
Of, kort en praktisch:
(ref) {A1/ A2/ .. An}.
': Universele kwantor.
Impliceert onder de gerelateerde variabelenaam een selectie van conjuncte domein-objecten.
Bijv.: { x A(x) };
Betekent voor domeinen met omvang van n individuen:x A(x) };(parafrase
) { A(x[1])A(x[2]) .. A(x[n])
}.(parafrase
) {
(i:=1,..n) { A(x[i]) } }.(ref) { A(a[1]) A(a
[2]) .. A(a[n]) }.(ref) {A(a[1] + a[2] + .. a[n]
) }.(ref) {A1, A2, .. An}.(1b) '
': Existentiële kwantor.
Impliceert onder de gerelateerde variabelenaam een selectie van disjuncte domein-objecten.
Bijv.: { x A(x) } :
Betekent voor domeinen met omvang van n individuen:x A(x) } :(parafrase
) { A(x[1])A(x[2]) .. A(x[n])
}.(parafrase
) {
(i:=1,..n) { A(x[i]) } }.(ref) {A(a[1]) A(a
[2]) .. A(a[n]) }.(zgn. Herbrand disjunction).
(ref) {A(a[1] / a[2] / .. a[n]
) }.(ref) {A1/ A2/ .. An}.2. Constanten en logische functies.
(2a)
Dit wil zeggen: c[k] is altijd over de gehele, maximale verzameling formules een - enkelvoudige - keuze, of selectie, van minstens één ding x[k] uit het totale domein D*x - waarbij die keuze vervolgens volkomen onafhankelijk van elke specifieke x[i] blijft. Dus elke x [i] kan worden gesubstitueerd door c[k].
Met andere woorden geldt:
(2b)
Functies hebben in de logica een iets andere betekenis dan in de wiskunde, fysica of informatietechnologie. Hier verwijzen ze allereerst naar een afhankelijkheidsrelatie. Dit kan een verwijzingsrelatie zijn of een bewerking. In eerste instantie is echter alleen het bereik van de referent belangrijk, niet de inhoudelijke waarde of uitkomst van de bewerking (hoewel die wel later in de redeneerketen een rol kan gaan spelen). Logica gaat immers primair over algemene waarheidsrelaties en waarheidsafhankelijkheidsrelaties (geldigheid), niet over inhoud of waarde.
Het referent van een logische functie bestaat dan ook uit een selectie uit het zelfde domein als waar de argumenten van de functie uit afkomstig of van afgeleid zijn. De 'uitkomst' of het 'resultaat' van een functie kan in voorkomend geval dan ook identiek zijn aan haar 'invoer'.
Bijvoorbeeld, een functie f[j](x[k]) vertegenwoordigt altijd per argument x[k] binnen de (sub)formule, steeds weer een nieuwe keuze, of selectie, van minstens één ding x[k[j]] uit domein of subdomein D*x[k] - waarbij die keuze vervolgens volkomen onafhankelijk van elke specifieke x [k] blijft. Dus elke x[i] kan worden gesubstitueerd door f[j](x[k]).
f[j](x[i]) =(ref) {
{f[j](a[1]): {a[1]/ a[2]/ .. a[n1]}},
{f[j](a[2]): {a[1]/ a[2]/ .. a[n1]}},
..
{f[j](a[n1]): {a[1]/ a[2]/ .. a[n1]} } }.
Of, met kortere notatie:
(ref) {
(a[1]; {a[1]/ a[2]/ .. a[n1]}),
(a[2]; {a[1]/ a[2]/ .. a[n1]}),
..
(a[n1]; {a[1]/ a[2]/ .. a[n1]}) }.
Of, kort en praktisch:
Dit wil zeggen: Met andere woorden geldt:
Skolem-constante (nul-plaatsige functie):
Bijv.: {a[c]};
Betekent voor domeinen met omvang van n1 individuen:
=(ref) {a[1] / a[2] .. / a[n]}.
Of, kort en praktisch:
=(ref) {a1/ a2/ .. an}.
Bijv., stel we hebben een argument-lijst: '(.. x[i], .. c[k] ..)'.Dit wil zeggen: c[k] is altijd over de gehele, maximale verzameling formules een - enkelvoudige - keuze, of selectie, van minstens één ding x[k] uit het totale domein D*x - waarbij die keuze vervolgens volkomen onafhankelijk van elke specifieke x[i] blijft. Dus elke x [i] kan worden gesubstitueerd door c[k].
Met andere woorden geldt:
{ k i ((c[k]
D*)
((x[i] D*
) (c[k] = D*x[k])
(c[i] = D*x[i])
(D*x[k] 
D*
x[i])) )x,k }.
k i ((c[k]
D*)((x[i] D*
) (c[k] = D*x[k])
(c[i] = D*x[i])
(D*x[k] D*
x[i])) )x,k }.(2b)
Skolem functie (n-plaatsige functie):
Functies hebben in de logica een iets andere betekenis dan in de wiskunde, fysica of informatietechnologie. Hier verwijzen ze allereerst naar een afhankelijkheidsrelatie. Dit kan een verwijzingsrelatie zijn of een bewerking. In eerste instantie is echter alleen het bereik van de referent belangrijk, niet de inhoudelijke waarde of uitkomst van de bewerking (hoewel die wel later in de redeneerketen een rol kan gaan spelen). Logica gaat immers primair over algemene waarheidsrelaties en waarheidsafhankelijkheidsrelaties (geldigheid), niet over inhoud of waarde.
Het referent van een logische functie bestaat dan ook uit een selectie uit het zelfde domein als waar de argumenten van de functie uit afkomstig of van afgeleid zijn. De 'uitkomst' of het 'resultaat' van een functie kan in voorkomend geval dan ook identiek zijn aan haar 'invoer'.
Bijvoorbeeld, een functie f[j](x[k]) vertegenwoordigt altijd per argument x[k] binnen de (sub)formule, steeds weer een nieuwe keuze, of selectie, van minstens één ding x[k[j]] uit domein of subdomein D*x[k] - waarbij die keuze vervolgens volkomen onafhankelijk van elke specifieke x [k] blijft. Dus elke x[i] kan worden gesubstitueerd door f[j](x[k]).
Bijv.: {f[j](x[i]) };
Betekent voor domeinen met omvang van n1 individuen:f[j](x[i]) =(ref) { {f[j](a[1]): {a[1]/ a[2]/ .. a[n1]}},
{f[j](a[2]): {a[1]/ a[2]/ .. a[n1]}},
..
{f[j](a[n1]): {a[1]/ a[2]/ .. a[n1]} } }.
(ref) { (a[1]; {a[1]/ a[2]/ .. a[n1]}),
(a[2]; {a[1]/ a[2]/ .. a[n1]}),
..
(a[n1]; {a[1]/ a[2]/ .. a[n1]}) }.
=(ref) { (a1.1 /a1.2, .. a1.n1), (a2.1 /a2.2, .. a
2.n1), (an1.1 /an1.2, .. an1.n1) }.
Bijv., stel we hebben een argument-lijst: '(.. x[i], .. f[j](x[k]) ..)'.Dit wil zeggen: Met andere woorden geldt:
[*CHK:] { j k i ((
x[k] D*)
((f[j](x[k])
D*)
(x[k] = D*
x[k]) (x[i] = D*x[i])
((f[j](x[k])
D*) (D*x[k]
D*x[i])) (D
*f[j](x[k] D*
x[k][i])) )x,k }.
Dus onder een willekeurige x[i] omvat f[j](x[k]) méér keuzes (disjuncten) dan c[k]
. Dus geldt:j k i ((
x[k] D*)((f[j](x[k])
D*) (x[k] = D*
x[k]) (x[i] = D*x[i])((f[j](x[k])
D*) (D*x[k]
D*x[i])) (D
*f[j](x[k] D*
x[k][i])) )x,k }.
{ g h i
j k (
F[g] {P[h](.. x[i], .. {c[k]} ..)}
F[g] {P[h](.. x[i]
, .. {f(x[i])=x[i][j]} ..)} )k,j,i,h,g }.
Maar niet omgekeerd!g h i
j k (F[g] {P[h](.. x[i], .. {c[k]} ..)}
F[g] {P[h](.. x[i]
, .. {f(x[i])=x[i][j]} ..)} )k,j,i,h,g }.3.
Formalismen en interpretaties/validaties.
Als we de geldigheid van een redenering willen bewijzen moeten we in het algemeen aantonen dat de premisse(n) voldoende voorwaarde vormen voor (de vervulling van) de conclusie(s). In de minimaal domein selectiemethode moeten we kijken of de minimaal domein definitie van de premisse(n) voldoende grond vormt voor de minimaal domein definitie van de conclusie(s). Oftewel, de tweede dient (eindig) afleidbaar te zijn uit de eerste.
Dit kunnen we het gemakkelijkste toetsen door de minimaal domein definities van beide componenten in een gestandaardiseerde vorm te zetten: met name een disjunctie van één of meer disjuncten (nl. conjuncties): de Disjunctief Normaal Vorm (DNF). De gezochte afleidingsrelatie geldt dan indien geldt:
(1) èlke disjunct c.q. conjunctie in de minimaal domein definitie van de premisse(n) volledig wordt 'gedekt' door
minstens één disjunct c.q. conjunctie in de minimaal domein definitie van de conclusie(s).
(2) èn: èlke conjunct c.q. grondpredikatie in een disjunct c.q. conjunctie in de minimaal domein definitie van de conclusie(s) volledig wordt 'gedekt' door minstens één conjunct c.q. grondpredikatie in een disjunct c.q. conjunctie in de minimaal domein definitie van de premissie(s).
(2) èn: èlke conjunct c.q. grondpredikatie in een disjunct c.q. conjunctie in de minimaal domein definitie van de conclusie(s) volledig wordt 'gedekt' door minstens één conjunct c.q. grondpredikatie in een disjunct c.q. conjunctie in de minimaal domein definitie van de premissie(s).
Nu eerst wat van het bovenstaande formeel weergeven om te weten wat we zeggen, eigenlijk, dus in logische vorm:
(1)
We gaan uit van de volgende notaties:
DS[m,s] : domein-selectie (DS) s, disjunctieve afgeleide van een deelverzameling van de
produktverzameling G![m,k]n1*n4, ontleend aan een domein m in de taal van
Hierbij is DS[m,s] geformuleerd in DNF vorm, een verzameling disjuncten Dj[m,s,i] (die zelf weer de vorm hebben van conjuncties):
Elke Dj![m,s,i] in een DS![m,s] is zelf deelverzameling van de produktverzameling G! [m,k]n1*n4, ontleend aan hetzelfde domein D![m].
Binnen elke DS[m,s] bestaat elke Dj[m,s,i] uit een conjunctie: een verzameling van minstens één conjunct Cj[m,s,i,l]:
Elke conjunct Cj![m,s,i,j] in de conjunctie c.q. disjunct Dj![m,s,i] van de DNF-vorm van DS! [m,s] bestaat uit één kwantorvrije factieve term; d.i. een (grond)atoom, (grond)literaal, c.q. grondpredikatie A[q,1](a[1]) uit G![m,k]n1*n4.
Een DS![m,s] die geldig is voor een F[h] mag in de regel samengesteld worden uit variabele combinaties van disjuncten met daarbinnen conjuncten bestaande uit grondpredikaties uit G![m,k]n1*n4 , mits en zolang de logisch-semantische structuur van F[h] door DS![m,s] voldoende, dus volledig wordt weergegeven. Er gelden dus een aantal algemene vereisten voor de logisch-semantische structuur van de DS![m,s].
Een disjunctieve afleiding van een deelverzameling uit een verzameling grondpredikaties G![m,k]n1*n4 is een domein-selectie DS[m,s] voor een formule F[h] indien geldt:
MD[m,h] : minimaal domein-definitie (MD) m voor een WFF formule F[h].
Een domein-selectie DS[m,s], disjunctieve afleiding van een deelverzameling uit een verzameling grondpredikaties G![m,k]n1*n4, is een minimaal domein-definitie MD[m,h] voor een formule F[h], indien geldt:
Domein selectie voor één formule.
We gaan uit van de volgende notaties:
DS[m,s]
PDL
-I, met n1 objecten a[i].Hierbij is DS[m,s] geformuleerd in DNF vorm, een verzameling disjuncten Dj[m,s,i] (die zelf weer de vorm hebben van conjuncties):
{ m s t (DS!
[m,s] (Dj[m,s,2] .. Dj[m,s,l])
[t] )t,s,m }.
m s t (DS!
[m,s] (parafrase
) (Dj[m,s,1]Dj[m,s,2] .. Dj[m,s,l])
[t] )t,s,m }.Elke Dj![m,s,i] in een DS![m,s] is zelf deelverzameling van de produktverzameling G! [m,k]n1*n4, ontleend aan hetzelfde domein D![m].
Binnen elke DS[m,s] bestaat elke Dj[m,s,i] uit een conjunctie: een verzameling van minstens één conjunct Cj[m,s,i,l]:
{ m s i
u (Dj![m,s,i] (Cj[m,s,i,2]
.. Cj[m,s,i,n.u])[u] )t,s,m }.
m s i
u (Dj![m,s,i] (parafrase
) (Cj[m,s,i,1]Cj[m,s,i,2]
.. Cj[m,s,i,n.u])[u] )t,s,m }.Elke conjunct Cj![m,s,i,j] in de conjunctie c.q. disjunct Dj![m,s,i] van de DNF-vorm van DS! [m,s] bestaat uit één kwantorvrije factieve term; d.i. een (grond)atoom, (grond)literaal, c.q. grondpredikatie A[q,1](a[1]) uit G![m,k]n1*n4.
Een DS![m,s] die geldig is voor een F[h] mag in de regel samengesteld worden uit variabele combinaties van disjuncten met daarbinnen conjuncten bestaande uit grondpredikaties uit G![m,k]n1*n4 , mits en zolang de logisch-semantische structuur van F[h] door DS![m,s] voldoende, dus volledig wordt weergegeven. Er gelden dus een aantal algemene vereisten voor de logisch-semantische structuur van de DS![m,s].
Een disjunctieve afleiding van een deelverzameling uit een verzameling grondpredikaties G![m,k]n1*n4 is een domein-selectie DS[m,s] voor een formule F[h] indien geldt:
(1a) DS is een deelverzameling van een verzameling grondpredikaties G!.
(1b) DS is een voldoende voorwaarde voor (de vervulling van) de formule F.
(1c) DS staat in disjunctief normaal vorm, en dus geldt: elke disjunct Dj in DS is een voldoende voorwaarde voor (de vervulling van) de formule F.
{m k | s (DS[m,s] G![m,k]
n1*n4) s,k,m }.
s (DS[m,s] G![m,k]
n1*n4) s,k,m }.(1b) DS is een voldoende voorwaarde voor (de vervulling van) de formule F.
{m k | s h (DS
[m,s] 
F[k,h]) h,s,k,m }.
s h (DS
[m,s] F[k,h]) h,s,k,m }.(1c) DS staat in disjunctief normaal vorm, en dus geldt: elke disjunct Dj in DS is een voldoende voorwaarde voor (de vervulling van) de formule F.
{m k | s i h (Dj
[m,s,i] DS[m,s]) (Dj
[m,s,i] F[k,h]) h,i,s,k,m }.
s i h (Dj
[m,s,i] DS[m,s]) (Dj
[m,s,i] F[k,h]) h,i,s,k,m }.(2) Minimaal domein definitie van één formule.
MD[m,h] : minimaal domein-definitie (MD) m voor een WFF formule F[h].
Een domein-selectie DS[m,s], disjunctieve afleiding van een deelverzameling uit een verzameling grondpredikaties G![m,k]n1*n4, is een minimaal domein-definitie MD[m,h] voor een formule F[h], indien geldt:
(2a) Er is geen overtollige predicatie in de domeinselectie:
D.w.z. er zijn geen redundantie-reducties meer mogelijk - bijvoorbeeld:
(·) 'doublure-eliminatie', op grond van identiteit;
(·) 'tautologie-eliminatie', op grond van equivalentie;
(·) voor conjuncties: 'derivaat-eliminatie', wegens subsumptie;
of, voor disjuncten: (·) 'instantie-eliminatie', of condensatie, wegens subsumptie;
enz.
(2b) Het is niet zo dat er een conjunct is in een disjunct die overtollig is voor de vervulling van de formule.
D.w.z. er zijn geen redundantie-reducties meer mogelijk - bijvoorbeeld:
(·) 'doublure-eliminatie', op grond van identiteit;
(·) 'tautologie-eliminatie', op grond van equivalentie;
(·) voor conjuncties: 'derivaat-eliminatie', wegens subsumptie;
of, voor disjuncten: (·) 'instantie-eliminatie', of condensatie, wegens subsumptie;
enz.
(2a1) Er is geen overtollige disjunct in de domeinselectie (die reduceerbaar is):
(2a2) Er is geen overtollige conjunct in een disjunct in de domeinselectie (die reduceerbaar is):
(ORD(x,y) : rangnummer van element y naar plaats binnen syntactische structuur x).
{m k |s i1 i2
h ( (DS[m,s] G![m,k])
( (Dj[m,s,i1] DS[m,s]
) ( (Dj[m,s,i2] DS[m,s]
)
( ¬(ORD(DS[m,s],Dj[m,s,i1]) =ORD(DS[m,s]
,Dj[m,s,i2]))
( ¬(Dj[m,s,i1] =(
¬(Dj[m,s,i1]
(
¬(Dj[m,s,i1]
(
))))h,i2,i1,s,k,m }.
{m k |
s i1 i2
h ( (DS[m,s] G![m,k])( (Dj[m,s,i1] DS[m,s]
) ( (Dj[m,s,i2] DS[m,s]
)( ¬(ORD(DS[m,s],Dj[m,s,i1]) =ORD(DS[m,s]
,Dj[m,s,i2]))( ¬(Dj[m,s,i1] =(syntaxis
) Dj[m,s,i2])¬(Dj[m,s,i1]
(parafrase
) Dj[m,s,i2])¬(Dj[m,s,i1]
(degres
) Dj[m,s,i2]) ) )))))h,i2,i1,s,k,m }.
(2a2) Er is geen overtollige conjunct in een disjunct in de domeinselectie (die reduceerbaar is):
(ORD(x,y) : rangnummer van element y naar plaats binnen syntactische structuur x).
{m k |s i j1
j2 h ( (DS[m,s]
G![m,k]) ( (Dj[m,s,i]
DS[m,s])
( (Cj[m,s,i,j1] Dj[m,s,i]
) ( (Cj[m,s,i,j2] Dj[m,s,i]
)
( ¬(ORD(Dj[m,s,i],Cj[m,s,i,j1]) =ORD(Dj
[m,s,i],Cj[m,s,i,j2]))
( ¬(Cj[m,s,i,j1] =(
¬(Cj[m,s,i,j1]
(
¬(Cj[m,s,i,j1]
(
)))))h,j2,j1,i,s,k,m }.
{m k |
s i j1
j2 h ( (DS[m,s]
G![m,k]) ( (Dj[m,s,i]
DS[m,s])( (Cj[m,s,i,j1] Dj[m,s,i]
) ( (Cj[m,s,i,j2] Dj[m,s,i]
)( ¬(ORD(Dj[m,s,i],Cj[m,s,i,j1]) =ORD(Dj
[m,s,i],Cj[m,s,i,j2]))( ¬(Cj[m,s,i,j1] =(syntaxis
) Cj[m,s,i,j2])¬(Cj[m,s,i,j1]
(parafrase
) Cj[m,s,i,j2])¬(Cj[m,s,i,j1]
(degres
) Cj[m,s,i,j2]) ))))))h,j2,j1,i,s,k,m }.
(2b) Het is niet zo dat er een conjunct is in een disjunct die overtollig is voor de vervulling van de formule.
{m k | s i j
h ( (DS[m,s] G![m,k])
( (Dj[m,s,i] DS[m,s]
)
( (Cj[m,s,i,j] Dj
[m,s,i])
( (Dj[m,s,i] F
[k,h])
¬( {Dj[m,s,i] \Cj[m,s,i,j]}
F[k,h]) )))))h,j2,j1,i,s,k,m }.
s i j
h ( (DS[m,s] G![m,k])( (Dj[m,s,i] DS[m,s]
)( (Cj[m,s,i,j] Dj
[m,s,i])( (Dj[m,s,i] F
[k,h])¬( {Dj[m,s,i] \Cj[m,s,i,j]}
F[k,h]) )))))h,j2,j1,i,s,k,m }.4.
Beslissen over afleidingsrelaties tussen twee formules.
Gegeven twee formules, zeg {F[k,h1], F[k,h2]}; met voor elk een bijbehorende welgevormde minimale domeindefinitie, zeg {MD[m,h1], MD[m,h2]}; geldt:
Voorwaarden voor geldige afleiding:
(1) Als de domeinselectie van de eerste formule die van de tweede vervult, dan impliceert de eerste formule de tweede.
Kort en goed, wat nodig is en te bewijzen staat is dit:
Voor elke disjunct in de premisse(n) F1 is er een afgeleide disjunct in de conclusie(s) F2.
Dit vereist:
De afleiding uit elke disjunct in F1 gebeurt op grond van inclusie relatie, dus via conjunctieve reductie.
Elke disjunct in F2 die níet voorkomt in F1, hetzij als equivalent, hetzij als conjuncte component in een disjunct van F1, is afleidbaar op grond van disjunctieve expansie.
{m k | s i j
h1 h2 (
(MD[m,h1]MD[m,h2])
(F[k,h] F[k,h])
)h,j2,j1,i,s,k,m }.
(2) Elke disjunct Dj[m,h1,i1] in de minimale domeindefinitie MD[m,h1] van de
premisse(n) F[k,h1] moet injectief afgebeeld zijn op minstens één disjunct Dj[m,h2,i2]
in de minimale domeindefinitie MD[m,h2] van de conclusie(s) F[k,h2].s i j
h1 h2 ((MD[m,h1]
MD[m,h2])(F[k,h] F[k,h])
)h,j2,j1,i,s,k,m }.
{m k | h1 h2 i1
i2 ( (Dj[m,h1,i1] MD[m,h1])
( (Dj[m,h2,i2] MD[m,h2]
)
(Dj[m,h1,i1] Dj
[m,h1,i2]) ) )j2,j1,i2,i1,h2,h1,k,m }.
(3) In elke disjunct Dj[m,h2,i2] in de minimale domeindefinitie MD[m,h2] van de
conclusie(s) F[k,h2] die (injectief) een afbeelding vormt van minstens één disjunct Dj
[m,h1,i1] in de minimale domeindefinitie MD[m,h1] van de premisse(n) F[k,h1],
moet èlke conjunct Cj[m,h2,i2,j2] injectief afgebeeld zijn op minstens één conjunct Cj
[m,h1,i1,j1] in dezelfde, bijbehorende Dj[m,h1,i1] in de minimale domeindefinitie MD[m,h1]
van de premisse(n) F[k,h1].h1 h2 i1
i2 ( (Dj[m,h1,i1] MD[m,h1])
( (Dj[m,h2,i2] MD[m,h2]
)(Dj[m,h1,i1] Dj
[m,h1,i2]) ) )j2,j1,i2,i1,h2,h1,k,m }.
{m | h1 h2 i1
i2 j1 j2 ( (Dj
[m,h1,i1] MD[m,h1])
( (Dj[m,h2,i2] MD[m,h2])
( (Cj[m,h1,i1,j1] Dj
[m,h1,i1])
( (Cj[m,h2,i2,j2] Dj
[m,h2,i2])
(Dj[m,h1,i1] Dj
[m,h1,i2]) )
(Cj[m,h2,i2,j2] Cj
[m,h1,i1,j1]) ) )i2,i1,h2,h1,k,m }.
h1 h2 i1
i2 j1 j2 ( (Dj
[m,h1,i1] MD[m,h1])
( (Dj[m,h2,i2] MD[m,h2])( (Cj[m,h1,i1,j1] Dj
[m,h1,i1])( (Cj[m,h2,i2,j2] Dj
[m,h2,i2])(Dj[m,h1,i1] Dj
[m,h1,i2]) )(Cj[m,h2,i2,j2] Cj
[m,h1,i1,j1]) ) )i2,i1,h2,h1,k,m }.Kort en goed, wat nodig is en te bewijzen staat is dit:
Voor elke disjunct in de premisse(n) F1 is er een afgeleide disjunct in de conclusie(s) F2.
Dit vereist:
De afleiding uit elke disjunct in F1 gebeurt op grond van inclusie relatie, dus via conjunctieve reductie.
Elke disjunct in F2 die níet voorkomt in F1, hetzij als equivalent, hetzij als conjuncte component in een disjunct van F1, is afleidbaar op grond van disjunctieve expansie.
Bijv.: {A1 /(B1,B2)} :
{A1} : ongeldig.
{(B1,B2)} : ongeldig.
{B1} : ongeldig.
{A1 /B1} : geldig.
{A1 /B1 /C1} : geldig.
{A1} : ongeldig.{(B1,B2)} : ongeldig.{B1} : ongeldig.{A1 /B1} : geldig.{A1 /B1 /C1} : geldig.5.
Kwantor-volgorde, inter-argumentrelaties en connectief.
We kunnen nu de bovenstaande principes en notaties gaan toepassen om logische relaties uit te drukken (of te interpreteren) in termen van domeinselecties, maar ook om de logische relaties tussen logische relaties te toetsen, met name op logische geldigheid.
We stappen daarvoor eerst over naar iets complexere formules, nl. twee- of meerplaatsige predicaties. Het eerste waar we dan goed begrip van moeten krijgen is de exacte interpretatie van inter-kwantorrelaties, dat wil zeggen, hoe combinaties van verschillende kwantoren op uiteenlopende manieren de selectie van objecten kunnen bepalen.
We nemen als eerste de combinatie van één existentiëler en één universele kwantor. Dan hebben we uiteraard twee mogelijke volgordes, elk met een heel eigen betekenis.
(1)
Of: 'Naast alle x is er een y (zodanig dat ..)'.
(2)
Of: 'Per x is er minstens één y (zodanig dat ..)'.
'y x' :
Betekent: 'Er is een y waarvoor elke x geldt dat ..'.y x' :Of: 'Naast alle x is er een y (zodanig dat ..)'.
(2)
'y x' :
Betekent: 'Voor elke x is er een y (zodanig dat ..)'.y x' :Of: 'Per x is er minstens één y (zodanig dat ..)'.
De algemene relaties zijn als volgt:
(a) ' '
' ' : is geldig.
(b) ' '
' ' : is
'
' ' : is geldig.
(b) '
'
' ' : is ongeldig
voor disjuncties (incl. implicaties).We zullen deze relaties bewijzen via twee stappen: door eerst de minimale domeindefinities te bepalen, en vervolgens de relaties tussen deze definities te specificeren.
(1) F1: {(y x A(x,y))};
(2) F2: {(x y A(x,y))};
y x A(x,y))};
Heeft als onderscheidend kenmerk: Nodig is dat er minstens één y is die voorkomt met elke x in een A-term.
Gegeneraliseerde domein-definitie (met Dn):
Minimaal domein-definitie (met Dn=2):
Minimaal domein-definitie, Dn=2, CNF, intensioneel:
Minimaal domein-definitie, Dn=2, DNF, extensioneel:
Skolem-vorm:
Gegeneraliseerde domein-definitie (met Dn):
{F1} (ref) DDF1:
{A(a[1] +a[2] .. +a[n], {a[1] /a[2] .. /a [n]} )};
= {A(a[1] +a[2] .. +a[n], a[c] =[{a[1] /a[2] .. /a[n]}])};
= {A(a[1] +a[2] .. +a[n], a[c])};
= {A(a[1],a[c]), A(a[2],a[c]), .. A(a[n],a [c]) };
(ref) DDF1:{A(a[1] +a[2] .. +a[n], {a[1] /a[2] .. /a [n]} )};
= {A(a[1] +a[2] .. +a[n], a[c] =[{a[1] /a[2] .. /a[n]}])};
= {A(a[1] +a[2] .. +a[n], a[c])};
= {A(a[1],a[c]), A(a[2],a[c]), .. A(a[n],a [c]) };
Minimaal domein-definitie (met Dn=2):
{F1} (ref) MDF1:
{ {A(a[1],a[1])), A(a[2],a[1]))} / {A(a[1],a[2])), A(a[2],a[2]))} };
Of, kort en praktisch:(ref) MDF1:{ {A(a[1],a[1])), A(a[2],a[1]))} / {A(a[1],a[2])), A(a[2],a[2]))} };
Minimaal domein-definitie, Dn=2, CNF, intensioneel:
={A1.y[c], A2.y[c]};
Minimaal domein-definitie, Dn=2, DNF, extensioneel:
={(A1.1,A2.1) /(A1.2,A2.2)}.
Skolem-vorm:
{F1} (Sk+1) {A(x,c) }.
(Sk+1) {A(x,c) }.(2) F2: {(
x y A(x,y))};
Heeft als onderscheidend kenmerk: Nodig is dat elke x voorkomt met minstens één y in een A-term.
Gegeneraliseerde domein-definitie (met Dn):
Minimaal domein-definitie (met Dn=2):
Minimaal domein-definitie, Dn=2, CNF, intensioneel:
Minimaal domein-definitie, Dn=2, CNF, extensioneel:
Minimaal domein-definitie, Dn=2, DNF, extensioneel:
Skolem-vorm:
Gegeneraliseerde domein-definitie (met Dn):
{F2} (ref) DDF2: (A(a[1] +a[2]
.. +a[n] , {{a[1] /a[2] .. /a[n]}[1] + {a
[1] /a[2] .. /a[n]}[2] .. + {a[1] /a[2] .. /a
[n]}[n]}}) ;
= {A(a[1],{a[1] /a[2] .. /a[n]}[1]),
A(a[2],{a[1] /a[2] .. /a[n]}[2]),
.. A(a[n],{a[1] /a[2] .. /a[n]}[n]) };
= {A(a[1],f(a[1])), A(a[2],f(a[2])), .. A(a[n],f(a [n])) };
(ref) DDF2: (A(a[1] +a[2]
.. +a[n] , {{a[1] /a[2] .. /a[n]}[1] + {a
[1] /a[2] .. /a[n]}[2] .. + {a[1] /a[2] .. /a
[n]}[n]}}) ;= {A(a[1],{a[1] /a[2] .. /a[n]}[1]),
A(a[2],{a[1] /a[2] .. /a[n]}[2]),
.. A(a[n],{a[1] /a[2] .. /a[n]}[n]) };
= {A(a[1],f(a[1])), A(a[2],f(a[2])), .. A(a[n],f(a [n])) };
Minimaal domein-definitie (met Dn=2):
{F2} (ref) MDF2:
{ {A(a[1],a[1]), A(a[2],a[1])} / {A(a[1],a[2]), A(a [2],a[2])}
/ {A(a[1],a[1]), A(a[2],a[2])} / {A(a[1],a[2]), A(a [2],a[1])} };
Of, kort en praktisch:(ref) MDF2:{ {A(a[1],a[1]), A(a[2],a[1])} / {A(a[1],a[2]), A(a [2],a[2])}
/ {A(a[1],a[1]), A(a[2],a[2])} / {A(a[1],a[2]), A(a [2],a[1])} };
Minimaal domein-definitie, Dn=2, CNF, intensioneel:
={A1.y[1], A2.y[2]};
Minimaal domein-definitie, Dn=2, CNF, extensioneel:
={(A1.1/A1.2),(A2.1/A2.2)};
Minimaal domein-definitie, Dn=2, DNF, extensioneel:
={(A1.1,A2.1) /(A1.1,A2.2) /(A1.2,A2.1) /(A1.2,A2.2)}.
Skolem-vorm:
{F2} (Sk+1) A(x,f(x)) }.
(Sk+1) A(x,f(x)) }.We zien aan het bovenstaande dat F1 en F2 op twee belangrijke eigenschappen verschillen:
(a)
Verwijzingspatronen binnen predicaat-argumenten.
Neem de Skolemisatie van F1: {x
y A(x,y)} (Sk+1)
x A(x,f(x)).
Het resultaat houdt de relatie 'per x is er minstens één y' intact.
Neem daarentegen de Skolemisatie van F2: {x
y A(x,y) (Sk+1)
x A(x,c).
De strekking van deze relatie blijkt duidelijk strikter en sterker, nl.: 'naast alle x is er een c'.
Afleiding van F1 naar F2 is dus ongeldig want met eliminatie van disjuncten op de tweede argument-plaats van F1.
(b)
Levert speelruimte voor (latere) unificatie en reductie.
F1(Sk+1): {x A(x,f(x))}
heeft een ruimer disjunctief referentieel bereik, naar het domein dan
F2(Sk+1): {x A(x,c)}.
F1 heeft dus meer contingenties, dus minder logische kracht dan F2.
Semantische verwijzingen
.Verwijzingspatronen binnen predicaat-argumenten.
Neem de Skolemisatie van F1: {
x
y A(x,y)} (Sk+1)
x A(x,f(x)).Het resultaat houdt de relatie 'per x is er minstens één y' intact.
Neem daarentegen de Skolemisatie van F2: {
x
y A(x,y) (Sk+1)
x A(x,c).De strekking van deze relatie blijkt duidelijk strikter en sterker, nl.: 'naast alle x is er een c'.
Afleiding van F1 naar F2 is dus ongeldig want met eliminatie van disjuncten op de tweede argument-plaats van F1.
(b)
Interpretatieruimte
.Levert speelruimte voor (latere) unificatie en reductie.
F1(Sk+1): {
x A(x,f(x))}
heeft een ruimer disjunctief referentieel bereik, naar het domein dan
F2(Sk+1): {x A(x,c)}.
F1 heeft dus meer contingenties, dus minder logische kracht dan F2.
Hoewel dus de afleidingsrelatie valt te beredeneren op grond van de Skolem-vormen van de formules, wordt de precieze bewijsgrond daarmee niet direct zichtbaar.
De minimaal domeindefinities laten echter onmiddellijk zien hoe de implicatierelaties liggen tussen componenten ( conjuncties in de disjuncten) van F1 en F2. Daaruit wordt duidelijk: elke disjunct in F1 kent een disjuncte afgeleide in F2. Dus F1 levert voldoende voorwaarde voor F2.
(MDF1: {(A1.1,A2.1) /(A1.2,A2.2)};
(
(F1 (
(degres
)(dj.lt./arg.xpn.) MDF2 : {(A1.1,A2.1) /(A1.1,A2.2) /(A1.2,A2.1) /(A1.2,A2.2)}.(F1 (degres
)( dj.lt./arg.xpn.) F2).6.
Een iets complexer voorbeeld.
Bijvoorbeeld de twee formules:
F1: {(y x (A(x)
B(x,y)))};
F2: {(x (A(x) (
w y B(w,y))))}.
y x (A(x)
B(x,y)))};F2: {(
x (A(x) (
w y B(w,y))))}.Vraag is of er een afleidingsrelatie is van F1 naar F2: levert F1 voldoende grond voor F2?
We toetsen dit door de minimaal domeinselecties met elkaar te vergelijken.
MDF1:
MDF2:
[CNF(Intens.)] ={(A1,B1.y[c]), (A2,B2.y[c])};
={(A1,A2), (B1.y[c],B2.y[c])};
[DNF(Extens.)] ={((A1,A2), (B1.1,B2.1)) /((A1,A2), (B1.2,B2.2))}.
={(A1,A2), (B1.y[c],B2.y[c])};
[DNF(Extens.)] ={((A1,A2), (B1.1,B2.1)) /((A1,A2), (B1.2,B2.2))}.
MDF2:
[CNF(Intens.)] ={(A1/(B1.y[1.1],B2.y[1.2]), (A2/(B1.y[2.1],B2.y[2.2]) };
[DNF(Intens.)] ={(A1,A2)
/(A1,(B1.y[2.1],B2.y[2.2])) /(A2,(B1.y[1.1],B2.y[1.2]))
/((B1.y[1.1],B2.y[1.2]), (B1.y[2.1],B2.y[2.2])) };
[DNF(Extens.)] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.1,B2.2)) /((B1.1,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.1,B2.2)) /((B1.1,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.2)) };
[DNF(Sort)] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2))
/(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1))
/(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2))
/(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1))
/(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2))
/((B1.1,B2.1), (B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1))
/((B1.2,B2.1), (B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1)) /((B1.1,B2.2), (B1.1,B2.2)) /((B1.2,B2.2), (B1.1,B2.2))
/((B1.2,B2.1), (B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.1)) /((B1.2,B2.2), (B1.2,B2.2))
/((B1.1,B2.1), (B1.2,B2.2)) /((B1.1,B2.1), (B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.1)) /((B1.2,B2.1), (B1.1,B2.2)) };
[DNF(Reduc.1(Doub.))] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.2)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.2))
/(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.2)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.2))
/(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2)
/((B1.1,B2.1), B1.2) /((B1.1,B2.1), B2.2) /((B1.2,B2.2), B1.1) /(B2.1, (B1.2,B2.2))
/((B1.1,B2.1), (B1.2,B2.2)) };
[DNF(Reduc.2(Condens.))] ={(A1,A2) /(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2) }.
[DNF(Intens.)] ={(A1,A2)
/(A1,(B1.y[2.1],B2.y[2.2])) /(A2,(B1.y[1.1],B2.y[1.2]))
/((B1.y[1.1],B2.y[1.2]), (B1.y[2.1],B2.y[2.2])) };
[DNF(Extens.)] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.1,B2.2)) /((B1.1,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.1,B2.2)) /((B1.1,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.2))
/(A1,(B1.1,B2.1)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.2)) };
[DNF(Sort)] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.1))
/(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2)) /(A1,(B1.1,B2.2))
/(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.1))
/(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2)) /(A1,(B1.2,B2.2))
/(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.1))
/(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2)) /(A2,(B1.1,B2.2))
/(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.1))
/(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2)) /(A2,(B1.2,B2.2))
/((B1.1,B2.1), (B1.1,B2.1)) /((B1.1,B2.1), (B1.1,B2.2)) /((B1.1,B2.2), (B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1))
/((B1.2,B2.1), (B1.1,B2.1)) /((B1.1,B2.1), (B1.2,B2.1)) /((B1.1,B2.2), (B1.1,B2.2)) /((B1.2,B2.2), (B1.1,B2.2))
/((B1.2,B2.1), (B1.2,B2.1)) /((B1.2,B2.1), (B1.2,B2.2)) /((B1.2,B2.2), (B1.2,B2.1)) /((B1.2,B2.2), (B1.2,B2.2))
/((B1.1,B2.1), (B1.2,B2.2)) /((B1.1,B2.1), (B1.2,B2.2)) /((B1.2,B2.2), (B1.1,B2.1)) /((B1.2,B2.1), (B1.1,B2.2)) };
[DNF(Reduc.1(Doub.))] ={(A1,A2)
/(A1,(B1.1,B2.1)) /(A1,(B1.1,B2.2)) /(A1,(B1.2,B2.1)) /(A1,(B1.2,B2.2))
/(A2,(B1.1,B2.1)) /(A2,(B1.1,B2.2)) /(A2,(B1.2,B2.1)) /(A2,(B1.2,B2.2))
/(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2)
/((B1.1,B2.1), B1.2) /((B1.1,B2.1), B2.2) /((B1.2,B2.2), B1.1) /(B2.1, (B1.2,B2.2))
/((B1.1,B2.1), (B1.2,B2.2)) };
[DNF(Reduc.2(Condens.))] ={(A1,A2) /(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2) }.
Te bewijzen staat dus:
(F1 F2).
Oftewel, in termen van minimaal domeindefinities:F2).(F1: {((A1,A2), (B1.1,B2.1)) /((A1,A2), (B1.2,B2.2))} F2: {(A1,A2) /(B1.1,B2.1) /(B1.1,B2.2) /(B1.2,B2.1) /(B1.2,B2.2) } ).Wat blijkt? Elke disjunct in F1 heeft een afgeleide disjunct in F2.
Daarmee is de stelling bewezen.