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)
[ref
{(x1,(y1,y2, ..).1)/ (x2,(y1,y2, ..).2)/ ..};]
[ref
{(x1,y1),(x1,y2), ..(x2,y1),(x2,y2), ..};] : ongeldig.
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, d
d)]; (upgrad)(cj.rdc.,diff.:inst.)
A( x, dd))
[ref
{(x1,d1),(x2,d1), ..};] [ref
{((x1,x2, ..),d1)};] : ongeldig.
[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, hs( 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, g
s( w, x))}
[ref
{(x1,(y1/y2/..).w1.x1), (x1,(y1/y2/..).w2.x1), ..
(x2,(y1/y2/..).w1.x2), (x2,(y1/y2/..).w2.x2), ..};] : ongeldig.
(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, g
d( 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( c
d, cd) [
ref {(c1,c1)};] : geldig.
[2a2] ·[ cd:=c
s]; (degres)(dj.xpn.)
A( cs, cs)
[ref
{(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
[ref {(x1,x1)/(x2,x2)/ ..};]
: geldig.
[2a3] ·[( ds, d
s) :=( cs, d
s)]; (upgrad)
(cj.xpn.\dj.rdc.) A( cs, ds)
[ref
{((x1/x2/ ..).c0),(x1/x2/ ..).d0))};]
[ref {(x1,x1)/(x1,x2)/ ..
(x2,x1)/(x2,x2)/ ..};] : geldig.
[2b] Route 2.
[2b1] ·[ x:=gd( y);
y:=x]; (degres)
(cj.rdc.:inst.) A( gd( x), gd( x))
[ref
{((y*).x1,(y*).x1), ((y*).x2,(y*).x2), ..};] : geldig.
[2b2] ·[ gd( x) :=g
s( x)]; (degres)
(dj.xpn.) A( gs( 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( ds, ds
)
[ref
{(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
[ref {(x1,x1)/(x2,x2)/ ..};]
: geldig.
[2b4] ·[( ds, d
s) :=( cs, d
s)]; (degres)(dj.xpn.)
A( cs, ds)
[ref
{(((x1/x2/ ..).c0),((x1/x2/ ..).d0))};]
[ref {(x1,x1)/(x1,x2)/ ..
(x2,x1)/(x2,x2)/ ..};] : geldig.
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, c
s)} [
ref {(x1,x1)/(x2,x2)/ ..};]
·[( cs, c
s) :=( cs, ds
)]; (degres)(dj.xpn.) A(
cs, ds)
[ref
{(x1,(y1/y2/ ..).1)/ (x2,(y1/y2/ ..).2)/ ..};] [ref
{(x1,y1)/(x2,y2)/ .. (x2,y1)/(x2,y2), ..};]
: geldig.
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))
[(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, ..};]
: is geldig.
(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, ds
)}
[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, ds
))
[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, gs
( 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)))
[ref
{(A1,C1.((1/2/ ..).1)), (A2,C2.((1/2/ ..).2)), ..};]
[ref
{A1,A2, .., C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..};] : geldig.
(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, fs
( 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; fs
( w) :=ds];
(upgrad)(dj.rdc.) (A( x), C_( w, d
s))
[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:=dd];
(degres)(cj.rdc.:inst.) (A( x), B(
dd))
[ref
{(A1,B.d1), (A2,B.d1), ..};] [ref
{A1,A2, .., B.d1};] : geldig.
[2a2] C2·[ dd:=d
s]; (degres)
(dj.xpn.:Sk+1) (A( x), B( ds))
[ref
{(A1,(B1/B2/ ..).d0), (A2,(B1/B2/ ..).d0), ..};] [ref
(compr.) {A1,A2, .., (B1/B2/ ..).d0};] : geldig.
[2b] Route 2.
[2b1] C2·[ x:=gd( z
); z:=x]; (degres)
(cj.rdc.:inst.) (A( x), B( gd( x)))
[ref
{(A1,(B*).1), (A2,(B*).2), ..};] [ref
{A1,A2, .., (B*).1,(B*).2, ..};] : geldig.
[2b2] C2·[ gd( x) :=
ds]; (degres)
(dj.xpn.:Sk+1) (A( x, B( ds))
[ref
{(A1,(B1/B2/ ..).d0), (A2,(B1/B2/ ..).d0), ..};] [ref
(compr.) {A1,A2, .., (B1/B2/ ..).d0};] : geldig.
(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, gs(
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, gs
( 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) )
[ref
{(A1,C1.((1/2/ ..).d0)), (A2,C2.((1/2/ ..).d0)), ..};]
[ref(compr.) {A1,A2, .. C1.((1/2/ ..).d0),
C2.((1/2/ ..).d0), ..};] : ongeldig.
(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)))
[ref
{(A1,(B*).1), (A2,(B*).2), ..};]
[ref {A1,A2, .., (B*).1,(B*).2, ..};]
: geldig.
[2a2] ·[ gd( x) :=g
s( x)]; (degres)
(dj.xpn.:Sk+1) (A( x), B( gs( x)))
[ref
{(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};]
[ref
{A1,A2, .., (B1/B2/ ..).1,(B1/B2/ ..).2, ..};] : geldig.
(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( c
d), B( cd))
[ref {A.c1,B.c1};]
: geldig.
[2a2] ·[ cd:=c
s]; (degres)
(dj.xpn.1:Sk+1) (A( cs), B( cs
))
[ref
{A(1/2/ ..).c0, B(1/2/ ..).c0};]
[ref {(A1,B1)/ (A2,B2)/ ..};]
: geldig.
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) :=f
s( x)]; (degres)
(dj.xpn.1:Sk+1) (A( fs( x)), B( f
s( x)))
[ref
{((A1/A2/ ..).1,(B1/B2/ ..).1), ((A1/A2/ ..).2,(B1/B2/ ..).2), ..};] : geldig.
[2b3] ·[ x:=cd];
(degres)(cj.rdc.:inst.) (A( f
s( cd)), B( fs( c
d))
[ref
{(A1/A2/ ..).c1, (B1/B2/ ..).c1)};] : geldig.
[2b4(=2a2)] Syntactische reductie:
·[ gs( cd
) :=cs];
(syn.rdc.:Sk±1,snn.) (A( cs), B( cs
))
[ref
{(A1/A2/ ..).c0, (B1/B2/ ..).c0)};] [ref
{(A1,B1)/ (A2,B2)/ ..};] : geldig.
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'.
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( c
s))}
[(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:=d
s]; (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) ) );
[(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/ ..};]
: geldig.
[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( c
s), B( cs) , ¬B( y) ) );
(2xlok.cj.rei.) ((A( cs),
B( cs) , ¬A( cs) , ¬A( x))
(A( cs), B( cs
) , ¬B( ds) , ¬B( y) ) );
(2xlok.ctd.) (( $0, B( cs
) , ¬A( x)) (A( cs),
$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, c
s)}
[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:=d
s]; (degres)(dj.xpn.) (A(
cs)), C_( x, ds))
[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/ ..), ..};] : geldig.
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( f
s( cd)), C_( x, fs( x)))
[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), ..};] : geldig.
Lokale Syntactische expansie ( synonymie):
[3] C1·[ fs( cd)
:=cs];
(syn.rdc.:Sk±1,snn.) (A( cs), C_( x, f
s( x)));
(( y A( y)), (
x z C_( x, z)));
(snn.) ( prenex) ( y
x z (A( y), C_( x, z
)));
[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), ..};] : geldig.
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]
[ref
{(A1/B1),(A1/B2), .. (A2/B1),(A2/B2), ..};] : ongeldig.
[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) )
[ref
{(A1/C1.((1/2/ ..).d0)), (A2/C2.((1/2/ ..).d0)), ..};] : ongeldig.
U-kwantor splitsing; U-kwantor buitenplaatsing.
[2] (Skl.) D2·[ x
:=w]; (upgrad)
(cj.xpn.) (A( x) C_( w, ds));
[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)), ..};] : ongeldig.
(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, 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.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), ..)};] : geldig.
(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:=ds
]; (upgrad)(cj.-dj.cnv.:ssm.)
(A( x) B( ds))
[ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};] : geldig.
[2a2a] Route 1.2. Vervolgafleiding, geldig (triviaal):
[2a2a1] D2·[ ds:=
gs( x)]; (
degres)(dj.xpn.) (A( x) B( g
s( x)))
[ref
{(A1/(B1/B2/..).1), (A2/(B1/B2/..).2), ..};] : geldig.
[2b] Route 2.
[2b1] D2·[ x:=dd];
(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:=d
s]; (degres)
(dj.xpn.) (A( x) B( ds))
[ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};] : geldig.
[2c] Route 3.
[2c1] D2·[ x:=gd( 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)))
[ref
{(A1/(B1/B2/..).d1), (A2/(B1/B2/..).d1), ..};]
[ref(compr.1)
{(A1,A2, ..)/ (B1/B2/..).d1};] : ongeldig.
[2c2a2a2] D2·[ gs( d
d) :=ds];
(syn.rdc.:Sk±1,snn.) (A( x
B( ds))
[ref
{(A1/(B1/B2/ ..).d0), (A2/(B1/B2/ ..).d0), ..};]
[ref(compr.1)
{(A1,A2, ..)/ (B1/B2/ ..).d0};] : geldig.
(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:=gs
( y); y:=x]; (
degres)(ssm.,dj.xpn.) (A( x) B( g
s( x)))
[ref
{(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};] : geldig.
[2b] Route 2. (ongeldige tussenstap).
[2b1] D2·[ x:=gd( 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) :=g
s( 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)))
[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), ..)};] : ongeldig.
(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( c
d) B( cd))
[ref {A.c1/B.c1};]
: geldig.
[2a2] ·[ cd:=c
s]; (degres)
(dj.xpn.1) (A( cs) B( c
s))
[ref
{(A1,B1)/(A2,B2)/ ..};]
[ref {A(1/2/ ..).c0/ B(1/2/ ..).c0};]
: geldig.
Basale Disjunctieve reïteratie:
[2a3] D2·[ cs:=d
s]; (dj.rei.) (A( cs
) 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( f
d( x)))
[ref
{((A*).1/(B*).1),((A*).2/(B*).2), ..};] : geldig.
[2b2] ·[ fd( x) :=f
s( x)]; (degres)
(dj.xpn.1) (A( fs( x))
B( fs( x)))
[ref
{((A1/A2/ ..).1/(B1/B2/ ..).1), ((A1/A2/ ..).2/(B1/B2/ ..).2), ..};] : geldig.
[2b3] ·[ fd( x) :=c
s]; (degres)
(cj.rdc.2.) (A( cs) B( c
s))
[ref
{(A1/A2/ ..).c0/ (B1/B2/ ..).c0};] [ref
{(A1/B1)/(A2/B2)/ ..};]
: geldig.
[2b4(=2a3)] Basale Disjunctieve reïteratie:
D2·[ cs:=ds
]; (dj.rei.) (A( cs)
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:=d
s]; (dj.rei.) (A( cs
) B( ds))
[ (( x A( x) )
( y B( y) ) );
(snn.) ( 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)) );]
[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/ ..};]
: geldig.
[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:=d
s]; (Sk+1,dj.rei.) (A( cs)
C_( x, ds))
(( y A( y))
( z x
C_( x, z)));
(snn.) (ccl. prenex) ( y
z x A( y)
C_( x, z)));
[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), ..)};] : geldig.
[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) :=c
s; ]; (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)));
[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), ..)};] : geldig.
C.P. van der Velde © 2004, 2016, 2019.
|
|
|