Cursus / training: Methode Formele Logica
©
15.
Argument-differentiatie/ Kwantor-splitsing; (QS),
geldig - vanuit term.
15.2.
Vormen van U-/ E- kwantor splitsing
( QJS/ QJS).
Argument-differentiatie/ Kwantor-splitsing: Universeel, Existentieel.
Toepasbaar in Literaal, Conjunctie, Disjunctie.
15.2.1. Argument-differentiatie/
Kwantor-splitsing; Binnen één Literaal.
(a1a) Argument-differentiatie/ Kwantor-splitsing; vanuit gepaarde variabelen,
naar meervoudige variabelen.
Via onevenwichtige renaming.
(a1a-1):
Bijv.: { x A( x, x)}
 ·[( x, x) :=( x, y)];
(degres)(cj.xpn.:ren.) (
x y A( x, y))
: ongeldig.
(Skl.) {A( x, x)}
[ ref
{(x1,x1),(x2,x2), ..};]
 ·[( x, x) :=( x, y
)]; (upgrad)(cj.xpn.:ren.)
A( x, y) : ongeldig.
[  ref
{(x1,(y1,y2, ..).1)/ (x2,(y1,y2, ..).2)/ ..};]
[  ref
{(x1,y1),(x1,y2), ..(x2,y1),(x2,y2), ..};]
Zo ook:
Bijv.: {A( x, fd( x))}
(degres)(v) A( x, fd( y
)) : is ongeldig.
(a1b) Argument-differentiatie/ Kwantor-splitsing; vanuit gepaarde variabelen,
naar 'Skolem' constante.
(a1b-1):
Bijv.: { x A( x, x)}
(upgrad)(cj.xpn.+rdc.;dj.xpn.) (
y x A( x, y))
: ongeldig.
(Skl.) [1] {A( x, x)}
[ ref
{(x1,x1),(x2,x2), ..};]
[2a] Route 1.
[2a1]  ·[( x, x) :=( x,
dd)]; (upgrad)
(cj.rdc.,diff.:inst.) A( x, dd)) : ongeldig
.
[  ref {(x1,d1),(x2,d1), ..};]
[  ref {((x1,x2, ..),d1)};]
[2a2]  ·[( x, dd) :=
( x, ds)];
(degres)(dj.xpn.) A( x,
ds)
[ ref
{(x1,(y1/y2/ ..).d0), (x2,(y1/y2/ ..).d0), ..};] : geldig.
(a2a) Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig,
naar 'Skolem' functie.
(a2a-1):
Bijv.: [1] { x y C_( x
, y))} (upgrad)(cj.xpn.)
( x w
y C_( w, y)) : ongeldig.
(Skl.) [1] C_( x, gs
( x) )
[ ref
{(x1,(y1/y2/..).x1), (x2,(y1/y2/..).x2), ..};] : geldig.
(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek element x.
Syntactische expansie ( synonymie):
[2]  ·[ gs( x
) :=hs( x, y)];
(syn.xpn.:Sk±1,snn.) C_( x, h
s( x, x) )
[ ref
{(x1,(y1/y2/..).x1.x1), (x2,(y1/y2/..).x2.x2), ..};] : geldig.
(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek paar (x,x),
c.q. element x.
Conjunctieve expansie:
[3]  ·[ hs( x
, x) :=hs( w, x)];
(upgrad)(cj.xpn.) {C_( x,
gs( w, x))} : ongeldig.
[  ref {(x1,(y1/y2/..).w1.x1),
(x1,(y1/y2/..).w2.x1), ..
(x2,(y1/y2/..).w1.x2), (x2,(y1/y2/..).w2.x2), ..};]
(D.w.z. steeds een nieuwe, onbepaalde keuze uit y, per uniek paar (x,w)).
(a2b) Argument-differentiatie/ Kwantor-splitsing; vanuit gepaarde variabelen,
naar 'Skolem' functie.
(a2b-1):
Bijv.: { x A( x, x)}
(degres)(cj.rdc.;dj.xpn.) (
x y A( x, y))
: geldig.
(Skl.) [1] {A( x, x)}
[ ref
{(x1,x1),(x2,x2), ..};]
[2a1]  ·[( x, x) :=( x,
gd( y)); y:=x];
(degres)(cj.rdc.:inst.) A( x
, gd( x))
[ ref
{(x1,(y*).1),(x2,(y*).2), ..};] : geldig.
[2a2]  ·[( x, gd( x))
:=( x, gs( x))];
(degres)(dj.xpn.) A( x,
gs( x))
[ ref
{(x1,(y1/y2/ ..).1), (x2,(y1/y2/ ..).2), ..};] : geldig.
(a3) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele, meervoudig,
naar 'Skolem' constanten.
(a3-1):
Bijv.: { x A( x, x)}
(degres)(cj.rdc.;2xdj.xpn.) (
x y A( x, y))
: geldig.
(Skl.) [1] {A( x, x)}
[ ref
{(x1,x1),(x2,x2), ..};]
[2a] Route 1.
[2a1]  ·[ x:=cd
)]; (degres)
(cj.rdc.:inst.) A( cd, cd)
[ ref
{(c1,c1)};] : geldig.
[2a2]  ·[ cd:=
cs]; (degres
)(dj.xpn.) A( cs, c
s) : geldig.
[  ref
{(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
[  ref {(x1,x1)/(x2,x2)/ ..};]
[2a3]  ·[( ds,
ds) :=( cs
, ds)]; (
upgrad)(cj.xpn.\dj.rdc.) A( cs
, ds) : geldig.
[  ref
{((x1/x2/ ..).c0),(x1/x2/ ..).d0))};]
[  ref {(x1,x1)/(x1,x2)/ ..
(x2,x1)/(x2,x2)/ ..};]
[2b] Route 2.
[2b1]  ·[ x:=gd
( y); y:=x]; (
degres)(cj.rdc.:inst.) A( gd( x), g
d( x))
[ ref
{((y*).x1,(y*).x1), ((y*).x2,(y*).x2), ..};] : geldig.
[2b2]  ·[ gd( x) :=
gs( x)];
(degres)(dj.xpn.) A( g
s( x), gs( x))
[ ref
{((y1/y2/ ..).1,(y1/y2/ ..).1), ((y1/y2/ ..).2,(y1/y2/ ..).2), ..};] :
geldig.
Syntactische expansie ( synonymie):
[2b3]  ·[ gs(
x) :=ds];
(syn.xpn.:Sk±1,snn.) A( d
s, ds) : geldig.
[  ref
{(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
[  ref {(x1,x1)/(x2,x2)/ ..};]
[2b4]  ·[( ds,
ds) :=( cs
, ds)];
(degres)(dj.xpn.) A( cs,
ds) : geldig.
[  ref
{(((x1/x2/ ..).c0),((x1/x2/ ..).d0))};]
[  ref {(x1,x1)/(x1,x2)/ ..
(x2,x1)/(x2,x2)/ ..};]
Differentieerbaar is '  , met gepaarde variabelen, bijv. ( x,
x).
(a3-2):
Bijv.: [1] { x A( x, x)}
(degres)(dj.xpn.) (
x y A( x, y))
: geldig.
[2] (Skl.) {A( cs
, cs)} [
 ref {(x1,x1)/(x2,x2)/ ..};]
 ·[( cs, c
s) :=( cs,
ds)];
(degres)(dj.xpn.) A(
cs, ds) : geldig.
[  ref {(x1,(y1/y2/ ..).1)/
(x2,(y1/y2/ ..).2)/ ..};]
[  ref
{(x1,y1)/(x2,y2)/ .. (x2,y1)/(x2,y2), ..};]
15.2.2.
Argument-differentiatie/ Kwantor-splitsing; In Conjunctie.
(a1a) Argument-differentiatie/ Kwantor-splitsing; vanuit gepaarde variabelen,
naar meervoudige variabelen.
Via hernoeming ( renaming).
U-kwantor splitsing, in Conjunctie, simpele vorm.
Met ongelijknamige predikaten.
(a1a-1):
Bijv.: [1] { x (A( x), B( x))}
(ren.,cj.rei.) (( x A(
x)), ( y B( y))) : geldig.
(Skl.) [1] {A( x), B( x)}
[  ( x ¬(A( x), B(
x)))];
[  ( x (¬A( x)
 ¬B( x)))];
(Skl.) (¬A( cs
)  ¬B( cs));
[  ref {(A1,B1),(A2,B2), ..};]
[  ref {A1,A2, .., B1,B2, ..)};]
Basale Conjunctieve reïteratie:
[2]  C2·[ x:=y];
(v) (A( x), B( y)) : is geldig.
[  ( x
y ¬(A( x), B( y)) );]
[  ( x
y (¬A( x)  ¬B( y
)) );]
[  (( x ¬A( x))
 ( y ¬B( y)) );]
(Skl.) (¬A( cs
)  ¬B( ds));
[  ref
{(A1,B1),(A1,B2), ..(A2,B1),(A2,B2), ..};]
[  ref {A1,A2, .., B1,B2, ..};]
(snn.) ( prenex) (
x y (A( x), B( y))).
(a1a-2):
Bijv.: [1] { y x (A( x
), C_( x, y))}  C2·[ x:=
w]; (ren.,cj.rei.) ((
x A( x)), ( y
w C_( w, y))) : geldig.
(Skl.) [1] {A( x), C_( x, d
s)}
[  ref {(A1,C1.(1/2/ ..).d0),
(A2,C2.(1/2/ ..).d0), ..};]
[  ref(compr.) {A1,A2, ..,
C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..};]
Basale Conjunctieve reïteratie:
[2]  C2·[ x:=w];
(ren.,cj.rei.) (A( x)), C_( w, d
s))
[  ref {A1,A2, ..,
C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..};] : geldig.
(snn.) ( prenex) (
x y w (A( x
), C_( w, y))).
(a1a-3):
Bijv.: [1] { x y (A( x
), C_( x, y))} (ren.,cj.rei.) ((
x A( x)), ( w
y C_( w, y))) : geldig.
(Skl.) [1] {A( x), C_( x, g
s( x))}
[  ref {(A1,C1.((1/2/ ..).1)),
(A2,C2.((1/2/ ..).2)), ..};]
[  ref {A1,A2, ..,
C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..};]
Basale Syntactische doublure-eliminatie:
[2]  C2·[ x:=w];
(cj.db.rdc.:ren.,unif.) (A( x), C_( w, g
s( w))) : geldig.
[  ref {(A1,C1.((1/2/ ..).1)),
(A2,C2.((1/2/ ..).2)), ..};]
[  ref
{A1,A2, .., C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..};]
(snn.) ( prenex) (
x w y (A( x
), C_( w, y))).
(a1a-4):
(Inverse van 15.2.2. (a2a)/1)).
Bijv.: [1] { x y (A( x
), C_( x, y))} (degres
)(dj.rdc.) (( x A( x)), (
y w C_( w, y
))) : ongeldig.
(Skl.) [1] {A( x), C_( x, f
s( x))}
[  ref {(A1,C1.((1/2/ ..).1)),
(A2,C2.((1/2/ ..).2)), ..};]
[  ref(compr.) {A1,A2, ..,
C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]
E-kwantor Binnenplaatsing, met Kwantor-volgordeverandering (!).
[2]  C2·[ x:=w; f
s( w) :=ds];
(upgrad)(dj.rdc.) (A( x), C_(
w, ds))
[  ref {(A1,C1.((1/2/ ..).d0)),
(A1,C2.((1/2/ ..).d0)), .. (A2,C1.((1/2/ ..).d0)), (A2,C2.((1/2/ ..).d0)), ..};]
[  ref(compr.)
{A1,A2,.., C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..};]
: ongeldig.
(snn.) ( prenex) (
y w x (A( x
), C_( w, y))).
(a1b) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele,
enkelvoudig, naar 'Skolem' constante.
(a1b-1):
Bijv.: { x (A( x), B( x))}
(degres)(cj.rdc;dj.xpn.) (
y x (A( x), B( y
))) : geldig.
(Skl.) [1] {A( x), B( x)}
[  ref {(A1,B1),(A2,B2), ..};]
[  ref {A1,A2, .., B1,B2, ..};]
[2a] Route 1.
[2a1]  C2·[ x:=d
d]; (degres)
(cj.rdc.:inst.) (A( x), B( dd)) : geldig.
[  ref
{(A1,B.d1), (A2,B.d1), ..};]
[  ref {A1,A2, .., B.d1};]
[2a2]  C2·[ dd:=
ds]; (degres
)(dj.xpn.:Sk+1) (A( x), B( ds
)) : geldig.
[  ref {(A1,(B1/B2/ ..).d0),
(A2,(B1/B2/ ..).d0), ..};]
[  ref(compr.)
{A1,A2, .., (B1/B2/ ..).d0};]
[2b] Route 2.
[2b1]  C2·[ x:=g
d( z); z:=x]; (
degres)(cj.rdc.:inst.) (A( x), B( gd(
x))) : geldig.
[  ref
{(A1,(B*).1), (A2,(B*).2), ..};]
[  ref
{A1,A2, .., (B*).1,(B*).2, ..};]
[2b2]  C2·[ gd( x)
:=ds];
(degres)(dj.xpn.:Sk+1) (A( x, B( d
s)) : geldig.
[  ref {(A1,(B1/B2/ ..).d0),
(A2,(B1/B2/ ..).d0), ..};]
[  ref(compr.)
{A1,A2, .., (B1/B2/ ..).d0};]
(a2a) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele, naar '
Skolem' constante.
(a2a-1):
Bijv.: [1] ( prenex): { x
y (A( x), C_( x, y) ) } (
upgrad)(dj.rdc.) (( x A( x) ) , (
y w C_( w, y
) ) ) : ongeldig.
[1] (Skl.) (A( x), C_( x, g
s( x) )
[  ref {(A1,C1.((1/2/ ..).1)),
(A2,C2.((1/2/ ..).2)), ..};]
[  ref(compr.) {A1,A2, ..
C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]
De C term (Literaal) is hier wegens Conjunctie automatisch onafhankelijk interpreteerbaar.
In dit geval althans omdat de conjuncte predicaties geen gemeenschappelijke existentële
variabelen hebben.
[2a] Route 1.
Met basale 'UE-EU' kwantor volgordeverandering.
Basale Conjunctieve reïteratie:
[2a1]  C2·[ x:=w];
(cj.rei.:ren.,diff.) (A( x), C_( w, g
s( w) )
[  ref {(A1,C1.((1/2/ ..).1)),
(A1,C2.((1/2/ ..).2)), .. (A2,C1.((1/2/ ..).1)), (A2,C2.((1/2/ ..).2)), ..};]
[  ref(compr.) {A1,A2, ..
C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]
(snn.) (( x A(
x) ) , ( w y C_(
w, y) ) );
(snn.) ( prenex): (
w y
x (A( x), C_( w, y) ) );
Lokale Disjunctieve reductie:
[2a2]  C2·[ gs(
w) :=ds];
(upgrad)(dj.rdc.:Sk±1) (A( x),
C_( w, ds) ) : ongeldig.
[  ref {(A1,C1.((1/2/ ..).d0)),
(A2,C2.((1/2/ ..).d0)), ..};]
[  ref(compr.) {A1,A2, ..
C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..};]
(snn.) (( x
A( x) ) , ( y w
C_( w, y) ) );
(snn.) ( prenex): (
y x
w (A( x), C_( w, y))).
(a2b) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele,
enkelvoudig, naar 'Skolem' functie.
(a2b-1):
Bijv.: [1] { x (A( x), B( x))}
(degres)(cj.rdc.;dj.xpn.) (
x y (A( x), B( y
))) : geldig.
(Skl.) [1] {A( x), B( x)}
[  ref {(A1,B1),(A2,B2), ..};]
[  ref {A1,A2, .., B1,B2, ..};]
[2a] Route 1.
[2a1]  ·[ x:=gd
( y); y:=x]; (
degres)(cj.rdc.:inst.) (A( x), B( gd( x
))) : geldig.
[  ref
{(A1,(B*).1), (A2,(B*).2), ..};]
[  ref
{A1,A2, .., (B*).1,(B*).2, ..};]
[2a2]  ·[ gd( x) :=
gs( x)];
(degres)(dj.xpn.:Sk+1) (A( x
), B( gs( x))) : geldig.
[  ref
{(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};]
[  ref
{A1,A2, .., (B1/B2/ ..).1,(B1/B2/ ..).2, ..};]
(a3) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele, enkelvoudig,
naar 'Skolem' constanten.
(a3-1):
Bijv.: { x (A( x), B( x))}
 D2·[ x:=y];
(degres)(cj.rdc.;dj.xpn.2x) ((
x A( x)), ( y B(
y))) : geldig.
(snn.) (ccl. prenex) {
x (A( x), B( x))}
 D2·[ x:=y];
(degres)(cj.rdc.;dj.xpn.2x) (
x y (A( x), B( y
))) : geldig.
(Skl.) [1] {A( x), B( x)}
[  ref {(A1,B1), (A2,B2), ..};]
[  ref {A1,A2, .., B1,B2, ..};]
[2a] Route 1.
[2a1]  ·[ x:=cd
)]; (degres)
(cj.rdc.:inst.) (A( cd), B( cd))
[ ref
{A.c1,B.c1};] : geldig.
[2a2]  ·[ cd:=
cs]; (degres
)(dj.xpn.1:Sk+1) (A( cs), B(
cs)) : geldig.
[  ref
{A(1/2/ ..).c0, B(1/2/ ..).c0};]
[  ref
{(A1,B1)/ (A2,B2)/ ..};]
Zie verder: E-kwantor splitsing, in Conjunctie, simpele vorm, [1-2] (geldig).
[2b] Route 2.
[2b1]  ·[ x:=fd
( y); y:=x]; (
degres)(cj.rdc.1:inst.) (A( fd( x)), B(
fd( x)))
[ ref
{((A*).1,(B*).1), ((A*).2,(B*).2), ..};] : geldig.
[2b2]  ·[ fd( x) :=
fs( x)];
(degres)(dj.xpn.1:Sk+1) (A(
fs( x)), B( fs(
x)))
[ ref
{((A1/A2/ ..).1,(B1/B2/ ..).1), ((A1/A2/ ..).2,(B1/B2/ ..).2), ..};]
: geldig.
[2b3]  ·[ x:=c
d]; (degres)
(cj.rdc.:inst.) (A( fs( cd
)), B( fs( cd))
[ ref
{(A1/A2/ ..).c1, (B1/B2/ ..).c1)};] : geldig.
[2b4(=2a2)] Syntactische reductie:
 ·[ fs(
cd) :=cs];
(syn.rdc.:Sk±1,snn.) (A( c
s), B( cs)) : geldig.
[  ref
{(A1/A2/ ..).c0, (B1/B2/ ..).c0)};]
[  ref
{(A1,B1)/ (A2,B2)/ ..};]
Zie verder: E-kwantor splitsing, in Conjunctie, simpele vorm, [1-2] (geldig).
E-kwantor splitsing, in Conjunctie, simpele vorm.
Met ongelijknamige predikaten.
(a3-2):
'Er is een ding dat A èn (tegelijk) B is', wordt: 'Er is een ding A, en er is een ding B'.
Geldig via disjuncte samples expansie.
Bijv.: [1] { x (A( x), B( x))}
(degres)(dj.xpn.) ((
x A( x)), ( x B(
x))) : geldig.
(snn.) (ccl. prenex) {
x (A( x), B( x))}
(degres)(dj.xpn.) (
x y (A( x), B( y
))) : geldig.
(Skl.) {A( cs
), B( cs))}
[  ( x ¬(A( x), B(
x)))];
[  ( x (¬A( x)
 ¬B( x)))];
[  ref
{(A1/A2/ ..).c0, (B1/B2/ ..).c0};]
[  ref {(A1,B1)/ (A2,B2)/ ..};]
[Bijv.: {{A1,B1}/ {A3,B3}};]
[2]  C2·[ cs:=
ds]; (degres)
(dj.xpn.) (A( cs), B( ds
));
 {( x A( x) ) , (
y B( y) ) } 
C2·[ y:=x];  (
x (A( x), B( x) ) );
(snn.) ( prenex) (
x y (A( x), B(
y) ) ) : geldig.
[  ( x
y ¬(A( x), B( y)) );]
[  ( x
y (¬A( x)  ¬B( y
)) );]
[  (( x ¬A( x))
 ( y ¬B( y)) );]
[  ref
{(A1/A2/ ..).c0, (B1/B2/ ..).d0};]
[  ref
{(A1,B1)/(A1,B2)/ ..(A2,B1)/(A2,B2)/ ..};]
[  ref(compr.) ((A1,(B1/B2/ ..))/
(A2,(B1/B2/ ..)) ..);]
[  ref(compr.)
{(A1/A2/ ..), (B1/B2/..)};]
[  ref {A1/A2/ .. B1/B2/ ..};]
[Bijv.: {{A1,B2}, {A2,B3}};]
Aanvullende bewijsvoering.
Direct bewijs, via minimaal domein.
Bijv.: ( dPDL=2):
{ x (A( x), B( x) ) };
 ref ((A1,B1)/ (A2,B2))};
(degres)(dj.xpn.) ((
x A( x) ) , ( y
B( y) ) )
 ref ((A1,B1)/ (A1,B2)/
(A2,B1)/ (A2,B2));
 ref(2xbas.compr.)
((A1,(B1/B2))/ (A2,(B1/B2)));
 ref(bas.compr.) ((A1/A2),
(B1/B2));
: geldig.
Bijv.: ( dPDL=3):
{ x (A( x), B( x) ) };
 ref
((A1,B1)/ (A2,B2)/ (A3,B3));
(degres)(dj.xpn.) ((
x A( x) ) , ( y
B( y) ) )
 ref ((A1,B1)/(A1,B2)/(A1,B3)/
(A2,B1)/(A2,B2)/(A2,B3)/ (A3,B1)/(A3,B2)/(A3,B3));
 ref(2xlok.compr.)
((A1,(B1/B2/B3))/ (A2,(B1/B2/B3))/ (A3,(B1/B2/B3)));
 ref(bas.compr.) ((A1/B1),
(A2/B2), (A3/B3)) : geldig.
Direct bewijs, via waarheidswaardepatronen.
Bijv.: ( dPDL=2):
 ( dPPL=4):
A1: (1111.1111.0000.0000);
A2: (1111.0000.1111.0000);
B1: (1100.1100.1100.1100);
B2: (1010.1010.1010.1010);
Prm. 1.
( x (A( x), B( x) ) );
 ref ((A1,B1)/ (A2,B2));
= ((C01: (A1,B1): (1100.1100.0000.0000)/
(C04: (A2,B2): (1010.0000.1010.0000));
= (D12: (C01/C04): (1110.1100.1010.0000));
Ccl. 1.
(degres)(dj.xpn.) {(
x A( x) ) , ( y
B( y) ) }
Ccl. 1.1.
 ref ((A1,B1)/ (A1,B2)/
(A2,B1)/ (A2,B2)));
= ((C01: (A1,B1): (1100.1100.0000.0000))/
(C02: (A1,B2): (1010.1010.0000.0000))/
(C03: (A2,B1): (1100.0000.1100.0000))/
(C04: (A2,B2): (1010.0000.1010.0000)));
= ((D09: (C01/C02): (1110.1110.0000.0000)/
(D10: (C03/C04): (1110.0000.1110.0000));
= (D11: (D09/D10): (1110.1110.1110.0000));
Ccl. 1.2.
 ref(2xcompr.)
((A1/A2), (B1/B2));
= ((D05: (A1/A2): (1111.1111.1111.0000)),
(D06: (B1/B2): (1110.1110.1110.1110)));
= (C13: (D05,D06): (1110.1110.1110.0000));
Rel.1.
= ((C22:=¬D12 ... : (0001.0011.0101.1111))/
(C13: (D05,D06): (1110.1110.1110.0000)));
= (D23: (C22/C13): (1111.1111.1111.1111)) : geldig.
Indirect bewijs, via resolutie.
Met 'nieuwe' Skolem constanten:
{ x (A( x), B( x) ) }
 ¬(( x A( x) ) , (
y B( y) ) );
 ((A( cs), B( c
s) ) , ( x
y ¬(A( x), B( x) ) ) );
 ((A( cs), B( c
s) , ( x
y (¬A( x)  ¬B( y
) ) ) );
 (A( cs), B( c
s) , (¬A( x)  ¬B( y
) ) );
[1] Route 1.
 (A( cs), B( c
s) , ¬A( x) );
 : sluit.
[2] Route 2.
(bas.dist.) ((A( cs
), B( cs) , ¬A( x))
 (A( cs), B( c
s) , ¬B( y) ) );
(2xlok.cj.rei.) ((A( c
s), B( cs) , ¬A( c
s) , ¬A( x))  (A( cs
), B( cs) , ¬B( d
s) , ¬B( y) ) );
(2xlok.ctd.) (( $0, B( c
s) , ¬A( x))  (A( c
s), $0 , ¬B( y) ) );
(2xlok.ctd.) (( $0)
 ( $0) );
 : sluit.
(a3-3):
Bijv.: [1] { y (A( y), (
x C_( x, y)))}  C2·[ y:=
z]; (degres)(dj.xpn.) ((
y A( y)), ( z
x C_( x, z))) : geldig.
(snn.) ( prenex) [1] {
y x (A( y), C_( x, y))}
 C2·[ y:=z];
(degres)(dj.xpn.) (
y z
x (A( y), C_( x, z))) : geldig.
(Skl.) [1] {A( cs), C_( x
, cs)}
[  ref
{(A1/A2/ ..).c0,C1.((1/2/ ..).c0)), (A1/A2/ ..).c0,C2.((1/2/ ..).c0)), ..};]
[  ref {(A1,(C1.1,C2.1, ..))/
(A2,(C2.2,C2.2, ..))/ ..};]
[2]  C2·[ cs:=
ds]; (degres)
(dj.xpn.) (A( cs)), C_( x, ds)) : geldig.
[  ref
{(A1/A2/ ..).c0,C1.((1/2/ ..).d0)), (A1/A2/ ..).c0,C2.((1/2/ ..).d0)), ..};]
[  ref {(A1/A2/ ..).c0,
C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..};]
[  ref {(A1/A2/ ..),
(C1.1/C1.2/ ..), (C2.1/C2.2/ ..), ..};]
Tweede term, met over-all Kwantor volgorde verandering.
(a3-4):
Bijv.: [1] { x y (A( y
), C_( x, y))};  C2·[ y:=
z]; (degres)(dj.rdc.)) ((
y A( y)), ( x
z C_( x, z))) : ongeldig.
(snn.) (ccl. prenex) [1] {
x y (A( y), C_(
x, y))};
(Skl.) [1] {A( fs( x)),
C_( x, fs( x))};
[  ref
{((A1/A2/..).1f,C1.(1/2/ ..)).1f), ((A1/A2/..).2f,C2.(1/2/ ..)).2f), ..};]
[  ref {(A1/A2/..).1f,
(A1/A2/..).2f, .. C1.((1/2/ ..).1f), C2.((1/2/ ..).2f), ..};]
[  ref {(A1,C1.1)/
(A2,C1.2)/ ..).1f, (A1,C2.1)/ (A2,C2.2)/ ..).2f, ..};]
[2]  C1·[ x:=cd
]; (degres)(cj.rdc.:inst.))
(A( fs( cd)), C_( x, f
s( x))) : geldig.
[  ref
{((A1/A2/..).c1f,C1.((1/2/ ..).1f)), ((A1/A2/..).c1f,C2.((1/2/ ..).2f)), ..};]
[  ref {(A1/A2/..).c1f,
C1.((1/2/ ..).1f), C2.((1/2/ ..).2f), ..};]
Lokale Syntactische expansie ( synonymie):
[3]  C1·[ fs( c
d) :=cs];
(syn.rdc.:Sk±1,snn.) (A( c
s), C_( x, fs( x)));
 (( y A( y)), (
x z C_( x, z
)));
(snn.) ( prenex) (
y x z (A( y
), C_( x, z))) : geldig.
[  ref
{((A1/A2/..).c0,C1.((1/2/ ..).1f)), ((A1/A2/..).c0,C2.((1/2/ ..).2f)), ..};]
[  ref {(A1/A2/..).c0,
C1.((1/2/ ..).1f), C2.((1/2/ ..).2f), ..};]
15.2.3.
Argument-differentiatie/ Kwantor-splitsing; In Disjunctie.
(a1a) Argument-differentiatie/ Kwantor-splitsing; vanuit gepaarde variabelen,
(meervoudig), naar enkelvoudige variabele.
Via hernoeming ( renaming).
U-kwantor splitsing, in Disjunctie, simpele vorm.
Met ongelijknamige predikaten.
(a1a-1)
Bijv.: [1] ( x (A( x)  B(
x)))
[  ( x ¬(A( x)
 B( x)))];
[  ( x (¬A( x), ¬B(
x)))];
(Skl.) (¬A( cs
), ¬B( cs));
(Skl.) {A( x)  B(
x)} [1]
[  ref {(A1/B1),(A2/B2), ..};]
(D.w.z. voor elke x uit het domein afzonderlijk
is er een bijbehorende, nieuwe keuze/selectie uit {A,B}).
D.w.z. voor elke eigenschap uit {A,B} geldt dat als ze voor één x geldt,
ze niet noodzakelijk voor alle x geldt.)
[Bijv.: {A1,B2,(A3,B3), ..};]
Conjunctieve expansie.
[2]  D2·[ x:=y];
(upgrad)(cj.xpn.:diff.) (
prenex) { x y (A(
x)  B( y))}
[  ( x
y ¬(A( x)  B( y
)) );]
[  ( x
y (¬A( x), ¬B( y)) );]
[  (( x ¬A( x)), (
y ¬B( y)) );]
(Skl.) (¬A( cs
), ¬B( ds))
(Skl.) {A( x) 
B( y)} [2] : ongeldig.
[  ref {(A1/B1),(A1/B2), ..
(A2/B1),(A2/B2), ..};]
[Bijv.: {A2,B1,B3,..};]
U-kwantor binnenplaatsing.
[3]  {( x A( x))
 ( y B( y))}
(Skl.) {A( x) 
B( y)} [3]
[  (( x ¬A( x)), (
y ¬B( y)));]
(Skl.) (¬A( cs
), ¬B( ds));
[  ref
{(A1,A2, ..)/ (B1,B2, ..)};]
[  ref(dist.1)
{(A1/(B1,B2, ..).1), (A2/(B1,B2, ..).2), ..};]
[  ref(dist.2)
{((A1/B1),(A1/B2), ..), ((A2/B1),(A2/B2), ..), ..};]
[  ref {(A1/B1),(A1/B2), ..
(A2/B1),(A2/B2), .., ..};]
(D.w.z. voor alle x uit het domein tezamen is er één zelfde keuze/selectie uit {A,B}).
D.w.z. voor elke eigenschap uit {A,B} geldt dat als ze voor één x geldt,
ze dan ook noodzakelijk voor alle x geldt.)
[Bijv.: {A1,A2,..};]
Bijv.: ( d=2):
({(A1/B1), (A2/B2)}  {(A1,A2)/ (B1,B2)} );
Distributie:
 ({(A1/B1), (A2/B2)}
(upgrad)(cj.xpn.) {(A1/B1), (A1/B2), (A2/B1), (A2/B2)} ) :
ongeldig.
Met behoud van Existentiële kwantificatie c.q. 'Skolem' constante.
U-kwantor splitsing, waarna E-kwantor Binnenplaatsing, Volgorde-behoudend.
(a1a-2)
Bijv.: [1] { y x (A( x
)  C_( x, y))} 
D2·[ x:=w]; (
upgrad)(cj.xpn.) (( x A( x) )
 ( y
w C_( w, y) ) );
(Skl.) (A( x)  C_(
x, ds) ) : ongeldig.
[  ref {(A1/C1.((1/2/ ..).d0)),
(A2/C2.((1/2/ ..).d0)), ..};]
U-kwantor splitsing; U-kwantor buitenplaatsing.
[2] (Skl.) 
D2·[ x:=w]; (
upgrad)(cj.xpn.) (A( x)  C_( w,
ds)); : ongeldig.
[  ref {(A1,A2, ..)/
(C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]
[  ref(dist.1)
{(A1/(C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..)),
(A2/(C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..)), ..};]
[  ref(dist.1)
{(A1/C1.((1/2/ ..).d0)), (A1/C2.((1/2/ ..).d0)), ..,
(A2/C1.((1/2/ ..).d0)), (A2/C2.((1/2/ ..).d0)), ..};]
(snn.) (ccl. prenex) (
x y
w (A( x)  C_( w,
y) ) );
Lokale Disjunctieve expansie:
[3]  D2·[ ds
:=gs( w))];
(degres)(dj.xpn.) (A( x)
 C_( w, gs( w))) :
geldig.
[  ref {(A1/C1.((1/2/ ..).1)),
(A1/C2.((1/2/ ..).2)), .. (A2/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};]
[  ref(compr.1)
{(A1/(C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)),
(A2/(C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)), ..};]
[  ref(compr.2)
{(A1,A2,..)/ (C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)};]
(snn.) ( prenex) (
x w y (A( x
)  C_( w, y) ) )
(a1b) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele,
enkelvoudig, naar 'Skolem' constante.
(a1b-1):
Bijv.: { x (A( x)  B( x
))} (upgrad)(cj.rdc.;dj.xpn.)
( y x (A( x)
 B( y))) : geldig.
(Skl.) [1] {A( x)
 B( x)} [
 ref {(A1/B1), (A2/B2), ..};]
[2a] Route 1.
[2a1]  D2·[ x:=d
s]; (upgrad)
(cj.-dj.cnv.:ssm.) (A( x)  B( d
s)) : geldig.
[  ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[  ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};]
[2a2a] Route 1.2. Vervolgafleiding, geldig (triviaal):
[2a2a1]  D2·[ ds
:=gs( x)];
(degres)(dj.xpn.) (A( x)
 B( gs( x)))
[ ref
{(A1/(B1/B2/..).1), (A2/(B1/B2/..).2), ..};] : geldig.
[2b] Route 2.
[2b1]  D2·[ x:=d
d]; (upgrad)
(cj.xpn.:diff.) (A( x)  B( dd))
[ ref
{(A1/B.d1), (A2/B.d1), ..};] [ ref
{(A1,A2, ..)/ B.d1};] : ongeldig.
[2b2a] Route 2.2. Vervolgafleiding, geldig:
[2b2a1]  D2·[ dd:=
ds]; (degres
)(dj.xpn.) (A( x)  B( d
s)) : geldig.
[  ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[  ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};]
[2c] Route 3.
[2c1]  D2·[ x:=g
d( z); z:=x]; (
upgrad)(cj.xpn.:diff.) (A( x)  B(
gd( x)))
[ ref
{(A1/(B*).1), (A2/(B*).2), ..};] : ongeldig.
[2c2a] Route 3.2. Vervolgafleiding, geldig:
[2b2a1]  D2·[ gd( x)
:=gs( x)];
(degres)(dj.xpn.) (A( x)
 B( gs( x)))
[ ref
{(A1/(B1/B2/..).1), (A2/(B1/B2/..).2), ..};] : geldig.
[2c2a2a] Route 3.2.2. Vervolgafleiding, ongeldig:
[2c2a2a1]  D2·[ x:= dd];
(degres)(cj.rdc.:inst.)
(A( x)  B( gs(
dd))) : ongeldig.
[  ref
{(A1/(B1/B2/..).d1), (A2/(B1/B2/..).d1), ..};]
[  ref(compr.1)
{(A1,A2, ..)/ (B1/B2/..).d1};]
[2c2a2a2]  D2·[ gs
( dd) :=ds
]; (syn.rdc.:Sk±1,snn.) (A( x
 B( ds)) : geldig.
[  ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[  ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};]
(a2b) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele,
enkelvoudig, naar 'Skolem' functie.
(a2b-1):
Bijv.: [1] { x (A( x)  B(
x))} (degres)
(cj.rdc.;dj.xpn.) ( x y
(A( x)  B( y))) : geldig.
(Skl.) [1] {A( x)
 B( x)} [
 ref {(A1/B1),(A2/B2), ..};]
[2a] Route 1.
[2a1]  D2·[ x:=g
s( y); y:=x];
(degres)(ssm.,dj.xpn.) (A( x
)  B( gs( x)))
[ ref
{(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};] : geldig.
[2b] Route 2. (ongeldige tussenstap).
[2b1]  D2·[ x:=g
d( y); y:=x]; (
upgrad)(cj.xpn.:diff.) (A( x)  B(
gd( x)))
[ ref
{(A1/(B*).1), (A2/(B*).2), ..};] : ongeldig.
[2b2a] Route 2.2. Vervolgafleiding, geldig:
[2b2]  ·[ gd( x) :=
gs( x)];
(degres)(dj.xpn.) (A( x)
 B( gs( x)))
[ ref
{(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};] : geldig.
(a2b-2):
Bijv.: { x y (A( x)
 C_( x, y))} (
upgrad)(cj.xpn.) (( x A( x))
 ( w
y C_( w, y))) : ongeldig.
(snn.) (ccl. prenex) {
x y (A( x)
 C_( x, y))} (
upgrad)(cj.xpn.) ( x
w y (A( x)
 C_( w, y))) : ongeldig.
(Skl.) [1] {A( x)
 C_( x, gs( x))}
[ ref {(A1/C1.((1/2/ ..).1)),
(A2/C2.((1/2/ ..).2)), ..};]
[2]  C2·[ x:=w];
(upgrad)(cj.xpn.) (A( x)
 C_( w, gs( w))) :
ongeldig.
[  ref {(A1/C1.((1/2/ ..).1)),
(A1/C2.((1/2/ ..).2)), .. (A2/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};]
[  ref(compr.1)
{(A1/(C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)),
(A2/(C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)), ..};]
[  ref(compr.2)
{(A1,A2,..)/ (C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..)};]
(a3) Argument-differentiatie/ Kwantor-splitsing; vanuit variabele, meervoudig,
naar 'Skolem' constanten.
(a3-1):
Bijv.: { x (A( x)  B( x
))} (degres)
(cj.rdc.;dj.xpn.2x) ( x
y (A( x)  B( y))) : geldig.
(Skl.) [1] {A( x)
 B( x)} [
 ref {(A1/B1),(A2/B2), ..};]
[2a1]  ·[ x:=cd
)]; (degres)(cj.rdc.:inst.)
(A( cd)  B( cd
))
[ ref
{A.c1/B.c1};] : geldig.
[2a2]  ·[ cd:=
cs]; (degres
)(dj.xpn.1) (A( cs)
 B( cs)) : geldig.
[  ref {(A1,B1)/(A2,B2)/ ..};]
[  ref
{A(1/2/ ..).c0/ B(1/2/ ..).c0};]
Basale Disjunctieve reïteratie:
[2a3]  D2·[ cs:=
ds]; (dj.rei.) (A( c
s)  B( ds
))
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm, [2] : geldig.
Alternatief spoor:
[2b1]  ·[ x:=fd
( y); y:=x]; (
degres)(cj.rdc.1:inst.) (A( fd( x))
 B( fd( x)))
[ ref
{((A*).1/(B*).1),((A*).2/(B*).2), ..};] : geldig.
[2b2]  ·[ fd( x) :=
fs( x)];
(degres)(dj.xpn.1) (A( f
s( x))  B( f
s( x)))
[ ref
{((A1/A2/ ..).1/(B1/B2/ ..).1), ((A1/A2/ ..).2/(B1/B2/ ..).2), ..};] :
geldig.
[2b3]  ·[ fd( x) :=
cs];
(degres)(cj.rdc.2.) (A( cs)
 B( cs)) : geldig.
[  ref
{(A1/A2/ ..).c0/ (B1/B2/ ..).c0};]
[  ref {(A1/B1)/(A2/B2)/ ..};]
[2b4(=2a3)] Basale Disjunctieve reïteratie:
 D2·[ cs:=
ds]; (dj.rei.) (A( c
s)  B( ds
))
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm., [2] : geldig.
E-kwantor splitsing, in Disjunctie, simpele vorm.
Met ongelijknamige predikaten.
(a3-2):
Bijv.: [1] { x (A( x)  B(
x))} (dj.rei.) ((
x A( x))  (
y B( y))) : geldig.
(snn.) (ccl. prenex) {
x (A( x)  B( x))}
(dj.rei.) ( x
y (A( x)  B( y))) :
geldig.
(Skl.) {A( cs
)  B( cs)}
 ( x (A( x)
 B( x) ) );
[  ( x ¬(A( x)
 B( x)))];
[  ( x (¬A( x), ¬B(
x)))];
[  ref
{(A1/A2/ ..).c0/ (B1/B2/ ..).c0};]
[  ref {(A1/B1)/ (A2/B2)/ ..};]
[  ref {A1/A2/ .. B1/B2/..};]
[Bijv.: {{A1/B1}/ {A3/B3}};]
Basale Disjunctieve reïteratie:
[2]  D2·[ cs:=
ds]; (dj.rei.) (A( c
s)  B( ds
))
[  (( x A( x) )
 ( y B( y) ) );
(snn.) ( prenex) {
x y (A( x)  B( y
) ) } : geldig.
[  ( x
y ¬(A( x)  B( y
)) );]
[  ( x
y (¬A( x), ¬B( y)) );]
[  (( x ¬A( x)), (
y ¬B( y)) );]
[  ref
{(A1/A2/ ..).c0/ (B1/B2/ ..).d0};]
[  ref
{(A1/B1)/(A1/B2)/ ..(A2/B1)/(A2/B2)/ ..};]
[  ref(compr.) ((A1/(B1/B2/ ..))/
(A2/(B1/B2/ ..)) ..);]
[  ref(compr.)
{(A1/A2/ ..)/ (B1/B2/..)};]
[  ref {A1/A2/ .. B1/B2/ ..};]
[Bijv.: {{A1/A3}/ {B2}};]
Aanvullende bewijsvoering.
Bewijs via resolutie.
{ x (A( x)  B( x) ) }
 (( x A( x) )
 ( y B( y) ) ) ;
 ((A( cs)
 B( cs) ) , (
x y ¬(A( x)
 B( y) ) ) );
 ((A( cs)
 B( cs) ) , (
x y (¬A( x), ¬B(
y) ) ) );
 ((A( cs)
 B( cs) ) , ¬A( x), ¬B(
y) );
(trf.ctd.) (A( cs
) , ¬A( x), ¬B( y) );
 : sluit.
(a3-3):
Bijv.: [1] {( y A( y))  (
x C_( x, y))}
(dj.rei.) (( y A( y))
 ( z
x C_( x, z))) : geldig.
(snn.) (ccl. prenex) {
y x (A( y)
 C_( x, y))}
(dj.rei.) ( y z
x A( y)  C_( x, z
))) : geldig.
(Skl.) {A( cs)
 C_( x, cs)}
[  ref
{(A(1/2/ ..).c0/ C1.((1/2/ ..).c0)), (A(1/2/ ..).c0/ C2.((1/2/ ..).c0))/ ..};]
[  ref(compr.)
{(A1/A2/ ..).c0/ (C1.((1/2/ ..).c0), C2.((1/2/ ..).c0), ..)};]
[Bijv.: {{A1}, {A1,(C1.1,C2.1, ..)}, {A1,(C1.2,C2.2, ..)}, {(C1.3,C2.3, ..)}, ..};]
Basale Disjunctieve reïteratie:
[2]  D2·[ cs:=
ds]; (Sk+1,dj.rei.) (A( c
s)  C_( x, ds))
 (( y A( y))
 ( z
x C_( x, z)));
(snn.) (ccl. prenex) (
y z
x A( y)  C_( x, z
))) : geldig.
[  ref {(A1/A2/ ..).c0/
(C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]
[  ref {(A1/(C1.((1/2/ ..).d0))/
(A1/(C2.((1/2/ ..).d0))/ .. (A2/(C1.((1/2/ ..).d0))/ (A2/(C2.((1/2/ ..).d0))/ ..};]
[  ref {A1/A2/ ..
(C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]
[Bijv.: {{A1}, {(C1.3,C2.3, ..)}, {A2,(C1.3,C2.3, ..)}, ..};]
(a3-4):
Tweede term, met over-all Kwantor volgorde verandering.
Bijv.: [1] { x y (A( y
)  C_( x, y))};
(degres)(dj.rei.) (( y A(
y))  ( x
z C_( x, z))) : geldig.
(snn.) ( prenex) {
x y (A( y)  C_( x
, y))};
(Skl.) {A( fs( x))
 C_( x, fs( x))};
[  ref
{((A1/A2/..).1f/(C1.(1/2/ ..).1f)), ((A1/A2/..).2f/(C2.(1/2/ ..).2f)), ..};]
[  ref {((A1/A2/..).1f,
(A1/A2/..).2f, ..)/ (C1.((1/2/ ..).1f), C2.((1/2/ ..).2f), ..)};]
[2]  D1·[ fs( x) :=
cs; ]; (degres)
(dj.rei.) (A( cs)  C_( x,
fs( x)));
 (( y A( y))
 ( x
z C_( x, z)));
(snn.) ( prenex) (
y x z (A( y
)  C_( x, z))) : geldig.
[  ref {(A1/A2/ ..).c0/
(C1.((1/2/ ..).1f), C2.((1/2/ ..).2f), ..)};]
[  ref(bas.dist.:dj.-cj.)
{((A1/A2/..).c0/C1.(1/2/ ..).1f), ((A1/A2/..).c0/C2.(1/2/ ..).2f), ..};]
[  ref
{((A1/A2/..).c0/C1.((1/2/ ..).1g)), ((A1/A2/..).c0/C2.((1/2/ ..).2g)), ..};]
[  ref {(A1/A2/ ..).c0/
(C1.((1/2/ ..).1g), C2.((1/2/ ..).2g), ..)};]
C.P. van der Velde © 2004, 2016, 2019.
|
|