Cursus / training: Methode Formele Logica
©
IV. Wetten voor
logische Normaal Vorm conversies [III].
Wetten voor Semantische Parafrase Reductie, in PDL.
Wetten voor reductie via eliminatie van redundante (deel)redenering ( clause) - alle onder parafrase
/ Equivalentie.
Syntactische verandering met (syntactische) termreductie;
met/zonder (semantische) verandering van hoofdconnectief, maar zonder (semantisch) verlies van
logische kracht.
8.
Parafrase reductie via Syntactische doublure eliminatie.
Syntactische verandering -
• met (syntactische) termreductie;
• met/zonder (semantische) verandering van hoofdconnectief;
• maar zonder (semantisch) verlies van logische kracht.
8A.
Directe Syntactische doublure.
8A.1.
Directe Syntactische doublure, in DNF: basale Conjunct Equivalentie.
Conjunct eliminatie; wegens 'basale Conjunct Equivalentie' ( clause equivalence).
Triviaal:
{(  x A( x))  (
y A( y)) }
C2·[ y:=x];  (u) (
x A( x)) : geldig.
Maar:
[CHK:]
{(  x A( x)) (
y A( y)) }
C2·[ y:=x]; (u) (
x A( x)) : ongeldig.
{( x A( x)) (
y A( y)) }
C2·[ y:=x];  (u,
degres) ( x A( x)) : geldig.
(Zie verder: Argument-unificatie).
8B. Indirecte
Syntactische doublure.
8B.1.
Indirecte Syntactische doublure, in CNF: basale Conjunct Implicatie.
Conjunct eliminatie; wegens 'basale Conjunct Implicatie' ( clause implication).
Basale Condensatie - van Conjunctie: Het sterkste element 'overleeft'.
' Clause implication' (zie: A. Leitsch, 1997, pp.199-210).
Algemene regel (in PPL):
' Conjunct Implicatie regel'.
{( p q) p}
(u) p;
{( p q) ( p
q) } (u)
p.
Bijv.: {A( x) A( cd) }
[ PPL {(A1
A2) A1) }
(A1 A2).]
[Indien cd is een (bestaande) ' domein' constante:
[ ( x (({ x}
= {x [1] .., x [i] .., x [n
]} )
 (( cd
 { x} )
(A( x) (
degres) A( cd) ) ) ) x );]
A( x).
Bijv.: {A( x) A( fd( x)) }
[Indien fd( x) is een (bestaande) ' domein' functie:
[ ( x (({ x}
= {x [1] .., x [i] .., x [n
]} )
(( fd( x)
{ x} )
(A( x) (
degres) A( fd( x)) ) ) ) x );]
A( x).
9. Parafrase
reductie via Transferente Equivalentie.
9A.
Indirecte Transferente Equivalentie
: via Basale Implicatie.
Factoriseren ( factoring) (in PDL): Levert een factor.
9A.2.
Indirecte Transferente Equivalentie, in DNF: via
Basale Disjunct Implicatie.
Disjunct eliminatie; wegens 'Basale Disjunct Implicatie' ( clause implication).
Bij ' Lokale redundantie' binnen Complexe Disjunctie.
Basale Condensatie - van Disjunctie: Het zwakste element 'overleeft'.
' Condensing principle' (zie: A. Leitsch, 1997, pp.95-96).
Algemene regel (in PPL):
' Disjunct Implicatie regel'.
{( p q)  q}
(u) q;
{( p q) ( p
q) } (u)
q.
9A.2a) Algemene vorm.
Eliminatie van basale Disjunct.
Bijv.: {A( x) A( cd) }
[ PPL {(A1
A2) A1) };
(u) A1.]
[Indien cd is een (bestaande) ' domein' constante:
[ ( x (( c
d { x} )
(A( x) (degres) A( c
d) ) ) x );]
A( cd).
Bijv.: {A( x) A( fd( x)) }
[Indien fd( x) is een (bestaande) ' domein' functie:
[ ( x (({ x}
= {x [1] .., x [i] .., x [n
]} )
(( fd( x)
{ x} )
(A( x) (
degres) A( fd( x)) ) ) ) x );]
A( fd( x)).
9A.1b) Met tweeplaatsige predicatie.
Bijv.: {(A( x, x) A( cd, c
d)) } (u,C) A( c
d, cd).
Echter:
Bijv.: {(A( x, x) A( x, cd
)) } A( x, cd) : ongeldig
.
(D.i. illegitieme argument-differentiatie, zie elders).
9A.1c) Met drieplaatsige Disjunctie.
General Factoring.
9A.1c.1) General Positive Factoring.
{(A( x) A( cd)
B) } ≡ (u,C) (A( cd)
B).
Maar:
{(A( x) A( cd)
B) } A( c
d) : ongeldig.
{(A( x) A( cd)
B) } (A( x)
B) : ongeldig.
9A.1b.2) General Negative Factoring.
{(¬A( x) ¬A( cd)
B) } ≡ (u,C) (¬A( cd)
B).
9B.
Indirecte Transferente Equivalentie: via Complexe Implicatie.
9B.1. Indirecte Transferente
Equivalentie, in CNF: via Basale Complexe Conjunct Implicatie.
Eliminatie van basale Disjunctie, wegens 'Basale Complexe Conjunct Implicatie' (
clause implication).
Bij (globale) redundantie van basale Disjunctie.
9B.1a) Algemene vorm.
Eliminatie van basale Disjunctie, wegens ' Transferente Implicatie'.
Bijv.: {A( x) (A( cd)
B) }
[ PPL {(A1
A2) (A1
B) } (A1
A2).]
Reïteratie 1.
[ (A( x) A( c
d) (A( cd)
B));
[ {A( x) A( c
d) } : is geldig.]
[ {A( x) (A( c
d) B) } : is geldig.]
Distributie 1:
((A( x) A( c
d)) (A( x) B) );
Lokale Absorptie 1:
(u,C) (A( x)
(A( x) B) );
{A( x) }.
Echter: Conjunct Implicatie - niet reduceerbaar.
Bijv.: {A( cd) (A( x)
B) } A( cd
) : ongeldig.
[ PPL {A1
((A1 A2)
B) };
[ (lok.distr.) {A1
((A1 B) (A2
B)) };
(trf.eqv.) {A1 (A2
B) };
[ {A( x) A( c
d) } : is geldig.]
[ {(A( x) B)
(A( cd)
B) } : is geldig.]
[ {A( x) B)
(A( cd) } : is ongeldig.]
Distributie 1:
((A( cd)
A( x)) (A( c
d) B) );
Lokale Absorptie 1:
(A( x)
(A( cd) B) ) );
Niet verder reduceerbaar.
N.b. Wel geldig is degressie, via Conjunctieve reductie, c.q. instantiatie:
Bijv.: {A( cd) (A( x)
B) } C2·[ x
:=cd]; (i)(
degres) {A( cd) (A(
cd) B);
(u,trf.eqv.) A( cd) : is
geldig.
9B.1b) Met daarnaast symmetrisch equivalente Disjuncten
Eliminatie van basale Disjunctie, Wegens ' Parallelle Implicatie'.
Via Contractie van Disjuncties.
{( A(x) B) (
A(cd) B)
C}
[ {(A( x) B)
(A( cd)
B) } : is geldig.]
Basale Comprimatie 1:
(u) (( A(x)
A(cd))
B ) C);
Lokale Absorptie 1:
(( A(x)
B) C);
{( A(x) B C)
( A(cd)
B C)
D}
[ {(A( x) B
C) (A( cd)
B C) } : is geldig.]
Herordening 1:
(( A(x) (
B C) ) (( A(c
d) (B C) )
D}
Comprimatie 1:
(u) ((( A(x)
A(cd))
(B C))
D);
Lokale Absorptie 1:
(( A(x)
B C)
D).
9B.1c) Met daarnaast symmetrisch niet-equivalente Disjuncten
{( A(x) B) (
A(cd) C) }
[ PPL {((A1
A2) B)
(A1 C) };]
Route 1.
Distributie 1 (splits 1e Disjunctie):
((( A(x)
( A(cd) C))
(B ( A(cd
) C)));
Distributie 2:
(( A(x)
A(cd)) ( A(x)
C) (B
A(cd))
(B C));
Lokale Absorptie 1:
(u,C) ( A(x)
( A(x) C)
(B A(cd
)) (B C));
Globale transferente Equivalentie eliminatie 1:
(u) ( A(x)
(B A(cd
)) (B C));
Globale transferente Implicatie eliminatie 1:
(u) ( A(x)
(B C)).
Route 2.
Distributie 1 (splits 2de Disjunctie):
((( A(x)
B) A(cd))
(( A(x) B)
C)));
Distributie 2:
(( A(x)
A(cd)) (B
A(cd))
( A(x) C)
(B C));
Lokale Absorptie 1:
(u,C) ( A(x)
( A(cd)
B) ( A(x)
C) (B
C));
Globale transferente Implicatie eliminatie 1:
(u) ( A(x)
( A(x) C)
(B C));
Globale transferente Equivalentie eliminatie 1:
( A(x)
(B C)).
Dus ook:
{( A(x) B C)
( A(cd)
B D)
E};
Comprimatie 1:
((B (( A(x)
C) ( A(c
d) D))) E);
Lokale Distributie 1, 2; Lokale Complexe Disjuncties Contractie:
(u,C) ((B ((
A(x) (C D)))
E);
(( A(x)
(C D)) B
E).
9B.2.
Indirecte Transferente Equivalentie, in DNF: via Basale Complexe Disjunct Implicatie.
Eliminatie van basale Conjunctie, wegens 'Basale Complexe Disjunct Implicatie' (
clause implication).
Bij (globale) redundantie van basale Conjunctie.
Algemene regel (in PPL):
{( p q) ( p
q) } (u)
q.
{( p q) p} [
({ p q}
p );] (u)
p.
{( p q r)
p} [ ({ p
q} p );]
(u) p.
(9B.2a) Algemene vorm.
Eliminatie van basale Conjunctie, wegens ' Transferente Implicatie'.
Bijv.: {A( cd) (A( x)
B) }
[ PPL {A1
((A1 A2)
B) }; (u) A1.]
Reïteratie 1.
[ (A( cd)
(A( x) A( c
d) B));
[ {A( x) A( c
d) } : is geldig.]
[ {(A( x) B)
A( cd) } : is geldig.]
Distributie 1:
((A( cd)
A( x)) ) (A( c
d) B) );
Lokale Condensatie 1:
(u,C) (A( cd)
(A( cd)
B) );
Transferente Equivalentie eliminatie 1:
A( cd).
Echter:
Disjunct Implicatie - niet reduceerbaar.
Bijv.: {A( x) (A( cd)
B) }
[ PPL {(A1
A2) (A1
B)) }; (u) (A1
(A2 B)).]
[ {A( x) A( c
d) } : is geldig.]
[ {A( x) (A( c
d) B) } : is ongeldig.]
Distributie 1:
((A( x) A( c
d)) (A( x) B) );
Lokale Condensatie 1:
(A( cd)
(A( x) B) );
Is niet verder reduceerbaar.
N.b. Wel geldig is degressie, via Conjunctieve reductie, c.q. instantiatie:
{A(x) (A( cd)
B) } ·[ y:=x];
(i)(degres) A( c
d) : is geldig.
9B.2b) Met daarnaast symmetrisch equivalente Disjuncten
Eliminatie van basale Conjunctie, Wegens ' Parallelle Implicatie'.
Via Contractie van Conjuncties.
{(A( x) B) (A( c
d) B) C}
Basale Comprimatie 1:
(u) ((A( x) A(
cd)) B )
C);
Lokale Condensatie 1:
((A( cd)
B) C);
{(A( x) B C)
(A( cd) B
C) D}
Herordening 1:
((A( x) (B
C) ) ((A( cd
) (B C) )
D}
Comprimatie 1:
(2u) (((A( x)
A( cd)) (B
C)) D);
Lokale Condensatie 1:
((A( cd)
B C)
D).
9B.2c) Met daarnaast symmetrisch niet-equivalente disjuncten
{(A( x) B) (A( c
d) C) }
[ PPL {((A1
A2) B)
(A1 C) };]
Route 1.
Distributie 1 (splits 1e Conjunctie:
(((A( x) (A( c
d) C)) (B
(A( cd)
C)));
Distributie 2:
((A( x) A( c
d)) (A( x) C)
(B A( cd))
(B C));
Lokale Condensatie 1:
(u,C) (A( cd)
(A( x) C)
(B A( cd))
(B C));
Globale transferente Equivalentie eliminatie 1:
(u) (A( cd)
(A( x) C)
(B C)) : niet verder reduceerbaar.
Route 2.
Distributie 1 (splits 2de Conjunctie:
(((A( x) B)
A( cd)) ((A(
x) B) C)));
Distributie 2:
((A( x) A( c
d)) (B A( c
d)) (A( x) C)
(B C));
Lokale Condensatie 1:
(u,C) (A( cd)
(B A( cd))
(A( x) C)
(B C));
Globale transferente Equivalentie eliminatie 1:
(A( cd)
(A( x) C)
(B C)) : niet verder reduceerbaar.
Dus ook:
{(A( x) B) (A( c
d) C) D};
((A( cd)
(A( x) C)
(B C)))
D) : niet verder reduceerbaar.
{(A( x) B C)
(A( cd) B
D) E};
Comprimatie 1:
(u) ((B ((A( x
) C) (A( cd
) D))) E);
Lokale Distributie 1, 2; Lokale Complexe Disjuncties Contractie:
(u,C) ((B ((A( x
) (C D)))
E);
((A( x) B
(C D))
E).
10. Parafrase
reductie via 'Niet-fatale' ('pseudo') contradictie.
10A.
Directe 'Niet-fatale' ('pseudo
') contradictie.
10A.2. Directe 'Niet-fatale' ('
pseudo') contradictie, in DNF: tussen (basale/ lokale) disjuncten.
Tautologie.
Algemeen: mutatis mutandis als in PPL.
Specifiek in PDL:
Bijv. via argument renaming:
Bijv.: {A( x, x) ¬A( x, y) }
C2·[ y:= x]
(u)(bas.taut.) $1 : is geldig.
10B.
Indirecte 'Niet-fatale' ('pseudo') contradictie.
10B.1. Indirecte 'Niet-fatale' contradictie
, in CNF: via Complexe Conjunct Contradictie.
Indirecte Transferente contradictie reductie.
Met basale Negatieve Literaal.
{( A( x) B)
¬A( cd) }
Route 1.
Reductie via Basale Distributie, naar Disjunctie:
(bas.distr.) (( A( x)
¬A( cd) )
(B ¬A( c
d)) );
(lok.cj.rei.) (( A( x)
A( cd)
¬A( cd) )
(B ¬A( c
d)) );
(u,lok.ctd.) (( A( x)
$0 ) (B
¬A( cd)) );
(lok.ctd.) (( $0)
(B ¬A( c
d)) );
Route 2.
Reductie via Lokale reïteratie, resp. Lokale Distributie:
(lok.cj.rei.) ((( A( x)
A( cd) )
B ) ¬A( c
d) );
(lok.distr.) ((( A( x)
B ) ( A( c
d) B ) ) ¬A
( cd) );
(syn.rdc.) (( A( x)
B ) ( A( c
d) B ) ¬A(
cd) );
(u,trf.ctd) (( A( x)
B ) B
¬A( cd) );
Route 2.1.
Reductie via Basale Transferente Equivalentie, direct.
(bas.trf.eqv.) (B
¬A( cd) );
Route 2.2.
Reductie via Basale Transferente Equivalentie, indirect.
(bas.distr.) (( A( x)
(B ¬A( c
d) ) ) (B (B
¬A( cd) ) ) );
(lok.doub.) (( A( x)
B ¬A( c
d) ) (B ¬A
( cd) ) );
(lok.cj.rei.) (( A( x)
A( cd)
B ¬A( c
d) ) (B ¬A
( cd) ) );
(lok.ctd.) (( A( x)
$0 B )
(B ¬A( c
d) ) );
(lok.ctd.) (( $0)
(B ¬A( c
d) ) );
Route 2.3.
Nutteloos:
(lok.cj.rei.) ((( A( x)
A( cd) )
B ) B
¬A( cd) );
(lok.distr.) ((( A( x)
B) ( A( c
d) B) ) ) B
¬A( cd) );
(syn.rdc.) (( A( x)
B ) ( A( c
d) B ) B
¬A( cd) );
(trf.ctd) (( A( x)
B ) B
B ¬A( c
d) );
(syn.rdc.) (( A( x)
B ) B
¬A( cd) );
etc..
(B ¬A( cd
)).
Idem ditto, met impliciete argument instantiatie.
{( A( x, d) B)
¬A( cd, y) }
(( A( x, d)
¬A( cd, y))
(B ¬A( c
d, y)) );
[ ( x (A( x, d
) ·[ x:=c
d]; (i) A( cd,
d));]
[ ( y (A( c
d, y) ·[ y:=
d]; (i) A( cd,
d));]
(( A( x, d)
¬A( cd, y)
A( cd, d)
¬A( cd, d) )
(B ¬A( c
d, y)) );
(u) (( A( x, d)
¬A( cd, y)
cd0 ) (B
¬A( cd, y)) );
(( $0) (B
¬A( cd, d)) );
(B ¬A( cd
, d)).
{( A( cd) B)
¬A( x) }
Route 1.
Reductie via Basale Distributie, naar Disjunctie:
(bas.distr.) (( A( c
d) ¬A( x) )
(B ¬A( x)) );
(lok.cj.rei.) (( A( c
d) ¬A( cd)
¬A( x) ) (B
¬A( x)) );
(u,lok.ctd.) (( $0
¬A( x)) (B
¬A( x)) );
(lok.ctd.) (( $0)
(B ¬A( x)) );
(B ¬A( x)).
Met lokale Negatieve Literaal.
{ A( x) ( ¬A( cd
) B) };
Route 1.
Basale Distributie:
(bas.distr.) (( A( x)
¬A( cd))
( A( x) B));
Lokale Contradictie:
(lok.ctd.) (( $0)
( A( x) B));
( A( x) B).
{ A( cd) ( ¬A(
x) B) };
Route 1.
Basale Distributie:
(bas.distr.) (( A( c
d) ¬A( x))
( A( cd)
B));
Lokale Contradictie:
(lok.ctd.) (( $0)
( A( cd)
B));
( A( cd)
B).
10B.2.
Indirecte 'Niet-fatale' contradictie, in DNF: via Indirecte Transferente contradictie.
Impliciete relatie van Implicatie.
10B.2.1.
Indirecte 'Niet-fatale' contradictie, in DNF: via Indirecte Transferente contradictie; met '
domein' constanten/ functies.
10B.2.1 (1a).
Bijv.: {A( x) ¬A( cd) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
( x (A( x)
¬A( cd)) );
( x (¬A( c
d) A( x)) );
Connectief conversie: naar Implicatie.
( x (A( c
d) A( x)) );
(A( cd)
( x A( x)) );
(A( cd)
A( x) );
( cd
x ) : ongeldig ( niet (verder) reduceerbaar).
[2] Lezing 2.
Inadequate interpretatie.
Inverse universele instantiatie, naar proximaal vorm.
(( x A( x))
¬A( cd) );
(¬A( cd)
( x A( x)) );
Connectief conversie: naar Implicatie.
(A( cd)
( x A( x)) );
( x (A( c
d) A( x)) );
[1] : ongeldig ( niet verder reduceerbaar
).
10B.2.1 (1b).
Bijv.: {A( x) ¬A( fd( x)) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
( x (A( x)
¬A( fd( x)) );
( x (¬A( f
d( x)) A( x) );
Connectief conversie: naar Implicatie.
( x (A( f
d( x)) A( x) );
(A( fd( x))
A( x) );
( fd( x)
x ) : ongeldig ( niet (verder)
reduceerbaar).
10B.2.1 (2a).
Bijv.: {¬A( x) A( cd) }
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
( x (¬A( x)
A( cd)) );
Connectief conversie: naar Implicatie.
( x (A( x)
A( cd)) );
( x ( x
cd) ) : ongeldig ( niet
(verder) reduceerbaar).
[2] Lezing 2.
Inadequate interpretatie.
Inverse universele instantiatie, naar proximaal vorm.
(( x ¬A( x))
A( cd) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.
((¬ x A( x))
A( cd) );
(¬( x A( x))
A( cd) );
Connectief conversie: naar Implicatie.
(( x A( x))
A( cd) );
( x (A( x)
A( cd) );
[1] : ongeldig ( niet (verder)
reduceerbaar).
10B.2.1 (2b).
Bijv.: {¬A( x) A( fd( x)) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
Inverse NNF conversie: Basale Negatie voorplaatsing.
( x (¬A( x)
A( fd( x)) );
Connectief conversie: naar Implicatie.
( x (A( x)
A( fd( x))) );
(A( x) A( f
d( x)) );
( x f
d( x) ) : ongeldig ( niet (verder) reduceerbaar).
10B.2.2.
Indirecte 'Niet-fatale' contradictie, in DNF: via Indirecte Transferente contradictie; met
Skolem constanten/ functies.
10B.2.2 (1a).
Bijv.: {A( x) ¬A( cs) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
(UI-1) ( x
(A( x) ¬A( cs)) );
Globale Kwantor binnenplaatsing.
[Zie 7.1.2.1. U-Kwantor-verplaatsing: 'binnenplaatsing', volgordebehoudend. (3) In Disjunctie
. Eerste term.]
( x (P( x) Q );
(iso) (P1/Q, P2/Q, ..);
(bas.comp.:cj.-dj.) ((P1,P2, ..)/ Q );
(PDL) (( x P(
x)) Q );
(( x
A( x)) ¬A( cs)) );
Inverse Skolemisatie.
(Sk-1) ( y
x (A( x) ¬A( y
)) );
( y
x (A( y) A( x
)) );
(A( cs)
A( x );
( cs
x ) : ongeldig ( niet (verder) reduceerbaar
).
Idem, genoteerd ( isomorf) in PPL:
(iso) ((A 1, A 2,
A 3, .. ) (¬A 1/ ¬A 2/ ¬A
3/ .. ) );
((A 1, A 2, A 3, ..
) / ¬A 1/ ¬A 2/ ¬A 3/ .. );
(trf.ctd.1) ((A 1, A 2,
.. ) / ¬A 1/ ¬A 2/ ¬A 3/ .. );
(trf.ctd.2) ((A 1, .. ) /
¬A 1/ ¬A 2/ ¬A 3/ .. );
..
(trf.ctd. (n-1))) (A 1 / ¬A 1
/ ¬A 2/ ¬A 3/ .. );
(bas.taut.) ( $1/ ¬A 2/ ¬A
3/ .. );
(bas.cds. 2..n) $1.
[2] Lezing 2. Inadequate interpretatie.
Inverse universele instantiatie, naar proximaal vorm.
(UI-1) (( x
A( x)) ¬A( cs) );
Inverse Skolemisatie.
(Sk-1) (( x
A( x)) ( y ¬A( y
)) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.
(( x A( x))
(¬ y A( y)) );
(( x A( x))
¬( y A( y)) );
Connectief conversie: naar Implicatie.
(( y A( y))
( x A( x)) );
[2.1] Lezing 2.1.
(bas.taut.) $1 : geldig (
Tautologie).
[2.2] Lezing 2.2. Inadequate interpretatie.
Illegitieme universele instantiatie.
( y x );
Inverse universele instantiatie, naar prenex vorm.
Universele kwantor differentiatie.
( y
x (A( y) A( x
)) ) : ongeldig ( niet (verder) reduceerbaar).
10B.2.2 (1b).
Bijv.: {A( x) ¬A( fs( x
)) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
(UI-1) ( x (A(
x) ¬A( fs( x)) );
Inverse Skolemisatie.
(Sk-1) ( x
y (A( x) ¬A( y
)) );
Connectief conversie: naar Implicatie.
( x
y (A( y) A( x
)) );
(A( fs( x))
A( x) );
( fs( x)
x ) : ongeldig ( niet (verder)
reduceerbaar).
[2] Lezing 2. Inadequate interpretatie.
Universele kwantor differentiatie.
(A( x) ¬A( f
s( z)) );
Inverse universele instantiatie, naar proximaal vorm.
(UI-1) (( x
A( x)) ¬A( fs( z
)) );
Inverse Skolemisatie.
(Sk-1) (( x
A( x)) ( y
z ¬A( y)) );
(( x A( x))
(¬ y
z A( y)) );
(( x A( x))
(¬ y [
z] A( y)) );
(( x A( x))
¬( y [
z] A( y)) );
(¬( y [
z] A( y)) (
x A( x)) );
Connectief conversie: naar Implicatie.
(( y [
z] A( y)) (
x A( x)) );
( y (([
z] A( y)) (
x A( x))) );
( y [
z] (A( y) (
x A( x)) );
( y [
z] x (A( y)
A( x)) );
(A( y) A( x) );
( y x ) :
ongeldig ( niet (verder) reduceerbaar).
10B.2.2 (2a).
Bijv.: {¬A( x) A( cs) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
(UI-1) ( x
(¬A( x) A( cs) );
Globale Kwantor binnenplaatsing.
[Zie 7.1.2.1. U-Kwantor-verplaatsing: 'binnenplaatsing', volgordebehoudend. (3) In Disjunctie
. Eerste term.]
(a) [( x (P( x) Q )
(( x P( x))
Q );
(iso) (((P1/ Q ), (P2/ Q ), .. )
(bas.comp.:cj.-dj.) ((P1, P2 )/ Q ) : geldig.]
(b) [( x (¬P( x) Q );
(iso) (¬P1/Q, ¬P2/Q, ..);
(bas.comp.:cj.-dj.) ((¬P1,¬P2, ..)/ Q );
(PDL) (( x
¬P( x)) Q );]
(c) [( x (¬P( x) Q )
(( x ¬P( x))
Q );
(iso) (((¬P1/ Q ), (¬P2/ Q ), .. )
(bas.comp.:cj.-dj.) ((¬P1, ¬P2 )/ Q ) : geldig.]
(( x ¬A( x))
A( cs) );
Inverse NNF conversie.
[(( x ¬P( x)) Q )
(¬( x P( x))
Q );
(iso) ((¬P1, ¬P2 )/ Q )
(lok.cnc.cvs.cj-dj.) (¬(P1/ P2 )/ Q ) : geldig.]
(¬( x A( x))
A( cs) );
Inverse Skolemisatie.
(Sk-1) ( y
x (¬A( x) A( y)) );
(iso) (((¬P1/ (Q1/Q2).c0 ), (¬P2/ (Q1/Q2).c0 ), .. );
[1a] ( y ((
x ¬A( x)) A( y
)) );
(compr.:cj.-dj.) ((¬P1, ¬P2 )/ (Q1/Q2).c0 );
( y (¬(
x A( x)) A( y
)) );
(iso) ((¬P1, ¬P2 )/ (Q1/Q2) )
(lok.cnc.cvs.cj-dj.) (¬(P1/ P2 )/ (Q1/Q2) ) : geldig.]
Inverse NNF conversie.
(Lokale Kwantor binnenplaatsing).
(¬( x A( x))
( y A( y)) );
Connectief conversie: naar Implicatie.
(( x A( x))
( y A( y)) );
[1b] Connectief conversie: naar Implicatie.
( y
x (A( x) A( y
)) );
Kwantor-binnenplaatsing met Universeel-existentieel conversie.
( y ((
x A( x)) A( y
)) );
Verantwoording van het voorgaande:
[( x (P( x) Q )
(( x P( x))
Q );
(iso) (((P1 imp. Q ), (P2 imp. Q ), .. )
(lok.compr.:cj.-dj.) ((P1/ P2 ) imp. Q ) : geldig.]
{( x P( x)) Q }
: Dat er een (minstens één) x een P is, is voldoende voorwaarde voor (waarheid/geldigheid van) Q
.
D.w.z. ' x P( x)' wijst op een Disjunctie
van (alle) x uit X.
Wijst dus (nog) niet op een [? onbekende /onbepaalde] subset ( Conjunctie)
van (sommige) x uit X.
(Is dus (nog) niet een [? onbekend /onbepaald] element uit de power set van X).
Tweede Kwantor-binnenplaatsing (zonder kwantor conversie).
(( x A( x))
( y A( y)) )
(lok.taut.) $1 : sluit
(blijkt geldig);
Verantwoording van het voorgaande:
(iso) ((P1 imp. (P1/P2/..).c0),
(P2 imp. (P1/P2/..).c0), .. );
(lok.compr.:dj.-cj.)
((P1/P2/..) imp. (P1/P2/..).c0 );
{( x P( x)) (
y P( y))} : Dat er een (minstens één) ding x
een P is, betekent : Dat er een (minstens één) ding y een P is.
Als dit geldig is, zou dat betekenen: dat je uit een existentiële predicatie altijd kunt
differentiëren naar een identieke existentiële predicatie
modulo de existentiële variabelenaam/namen.
[1.1] Route 1.1.
Her- Skolemisatie.
(Sk+1) ( x
(¬A( x) A( cs));
(( x ¬A( x))
A( cs));
(¬( x A( x))
A( cs));
[ (¬( x A( x))
A( cs));]
Skolemisatie.
Van lokale existentiële kwantor: Illegitiem.
(Sk+1) (¬A( ds
) A( cs) ) :
open (blijkt ongeldig);
[1.2] Route 1.2.
Vanaf hier is het onzin:
schending vereiste voorbewerkingen voor Skolemisatie;
tevoorschijn toveren van een heel andere UI-Sk formule).
Skolemisatie.
Illegitiem.
(Sk+1) ( y
(A( ds) A( y)) ) :
open (blijkt ongeldig);
(A( ds)
( y A( y)) );
Dit is alleen geldig als ds nieuw is.
[Maar zo Skolemiseer je toch niet, in een niet-NNF, niet-CNF enz. formule?]
Connectief conversie: naar Implicatie.
( y (¬A( d
s) A( y)) );
(¬A( ds)
( y A( y)) );
Her- Skolemisatie.
Is dit alleen geldig als ook cs nieuw is?
(Sk+1) (¬A( ds
) A( cs) );
(A( ds)
A( cs) );
Onder invariantie van predikaatnaam:
( ds
cs ) : Illegitiem
.
Ad [10B.2.2] (2a).
(¬P( x) P( cs))
(UI-1) ( x (¬P(
x) P( cs));
(Sk-1) ( y
x (¬P( x) P( y
)); ( y ((
x ¬P( x)) P( y
)); ( y (¬(
x P( x)) P( y));
( y
x (P( x) P( y
)); ( y (
x P( x)) P( y
)); (( x P( x))
( y P( y)) );
(lok.taut.) $1 : sluit
(blijkt geldig);
(Sk+1) ( x
(¬P( x) P( cs));
(( x ¬P( x))
P( cs));
(¬( x P( x))
P( cs));
(( x P( x))
P( cs));
Idem, genoteerd ( isomorf) in PPL:
(iso) ((¬A 1, ¬A 2
, ¬A 3, .. ) (A 1/ A 2
/ A 3/ .. ) );
((¬A 1, ¬A 2, ¬A 3, ..
) / A 1/ A 2/ A 3/ .. );
(trf.ctd.1) ((¬A 1, ¬A 2,
.. ) / A 1/ A 2/ A 3/ .. );
(trf.ctd.2) ((¬A 1, .. ) /
A 1/ A 2/ A 3/ .. );
..
(trf.ctd. (n-1)) (¬A 1 / A 1
/ A 2/ A 3/ .. );
(bas.taut.) ( $1/ A 2/ A
3/ .. );
(bas.cds. 2..n) $1.
[2] Lezing 2.
Inadequate interpretatie.
Inverse universele instantiatie, naar proximaal vorm.
(UI-1) (( x
¬A( x)) A( cs) );
Inverse Skolemisatie.
(Sk-1) (( x
¬A( x)) ( y A( y
)) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.
((¬ x A( x))
( y A( y)) );
(¬( x A( x))
( y A( y)) );
Connectief conversie: naar Implicatie.
(( x A( x))
( y A( y)) );
(A( ds)
( y A( y)) );
(A( ds)
A( cs) );
( ds
cs );
(vld.) $1 : geldig (
disjuncte expansie).
10B.2.2 (2b).
Bijv.: {¬A( x) A( fs(
x)) };
Interpretaties.
[1] Lezing 1.
Inverse universele instantiatie, naar prenex vorm.
(UI-1) ( x
(¬A( x) A( fs( x
)) );
Globale Kwantor binnenplaatsing.
(( x ¬A( x))
A( fs( x)) );
Inverse NNF conversie.
(¬( x A( x))
A( fs( x)) );
Verantwoording van het voorgaande:
(a) [( x (P( x) Q )
(( x P( x))
Q );
(iso) (((P1/ Q ), (P2/ Q ), .. )
(compr.:cj.-dj.) ((P1, P2 )/ Q ) : geldig.]
(b) [( x (¬P( x) Q )
(( x ¬P( x))
Q ); (¬(
x P( x)) Q );
(iso) (((¬P1/ Q ), (¬P2/ Q ), .. )
(compr.:cj.-dj.) ((¬P1, ¬P2 )/ Q );
(lok.cnc.cvs.cj-dj.) (¬(P1/ P2 )/ Q ) : geldig.]
Inverse Skolemisatie.
(Sk-1) ( x
y (¬A( x) A( y
)) );
(iso)
(((¬P1/ (Q1/Q2).f1 ), (¬P2/ (Q1/Q2).f2 ), .. );
[1.1] Route 1.1.
Connectief conversie: naar Implicatie.
(lok.cnc.cvs.dj-imp.) (
x y (A( x)
A( y)) );
PPL(iso) (((P1
(Q1/Q2).f1 ), (P2
(Q1/Q2).f2 ), .. );
PPL(iso) (((A1
(A1/A2).f1 ), (A2
(A1/A2).f2 ), .. );
PPL(iso) (((A1
(A1/A2).1 ), (A2
(A1/A2).2 ), .. );
Her- Skolemisatie.
(Sk+1) ( x
(A( x) A( fs( x
)));
[1.2] Route 1.2.
Her- Skolemisatie.
(Sk+1) ( x
(¬A( x) A( fs( x
))); Connectief conversie: naar Implicatie.
(lok.cnc.cvs.dj-imp.) (
x (A( x) A( f
s( x)));
$1 : geldig (
disjuncte expansie).
Ad [10B.2.2] (2b).
(¬P( x) P( fs( x
))) (UI-1) (
x (¬P( x) P( fs
( x)));
(Sk-1) ( y
x (¬P( x) P( y
)); ( y ((
x ¬P( x)) P( y
)); ( y (¬(
x P( x)) P( y
));
( y
x (P( x) P( y
)); ( y (
x P( x)) P( y
)); (( x P( x))
( y P( y)) );
(lok.taut.) $1 : sluit
(blijkt geldig);
(Sk+1) ( x
(¬P( x) P( fs( x
))); (( x ¬P( x
)) P( fs( x)));
(¬( x P( x))
P( fs( x)));
(( x P( x))
P( fs( x)));
C.P. van der Velde © 2004, 2016, 2019.
|
|