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,

f

d(x))}   (

degres

)(v) A(x,

f

d(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,

d

d)) :

ongeldig

.
 [

ref

 {(x1,d1),(x2,d1), ..};]
 [

ref

 {((x1,x2, ..),d1)};]
[2a2]  ·[(x,

d

d)

:=

(x,

d

s

)];   (

degres

)(dj.xpn.) A(x,

d

s

)
 [

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,

g

s

(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]  ·[

g

s

(x )

:=

h

s

(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]  ·[

h

s

(x ,x)

:=

h

s

(w,x)];   (

upgrad

)(cj.xpn.) {C_(x,

g

s

(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,

g

d(y));y

:=

x];   (

degres

)(cj.rdc.:inst.) A(x ,

g

d(x))
 [

ref

 {(x1,(y*).1),(x2,(y*).2), ..};] : geldig.
[2a2]  ·[(x,

g

d(x))

:=

(x,

g

s

(x))];   (

degres

)(dj.xpn.) A(x,

g

s

(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

:=

c

d )];  (

degres

) (cj.rdc.:inst.) A(

c

d,

c

d)  [

ref

 {(c1,c1)};] : geldig.
[2a2]  ·[

c

d

:=

c

s

];  (

degres

)(dj.xpn.) A(

c

s

,

c

s

) : geldig.
 [

ref

 {(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
 [

ref

 {(x1,x1)/(x2,x2)/ ..};]
[2a3]  ·[(

d

s

,

d

s

)

:=

(

c

s

,

d

s

)];  (

upgrad

)(cj.xpn.\dj.rdc.) A(

c

s

,

d

s

) : geldig.
 [

ref

 {((x1/x2/ ..).c0),(x1/x2/ ..).d0))};]
 [

ref

 {(x1,x1)/(x1,x2)/ .. (x2,x1)/(x2,x2)/ ..};]

[2b] Route 2.
[2b1]  ·[x

:=

g

d (y);y

:=

x];  (

degres

)(cj.rdc.:inst.) A(

g

d(x),

g

d(x))
 [

ref

 {((y*).x1,(y*).x1), ((y*).x2,(y*).x2), ..};] : geldig.
[2b2]  ·[

g

d(x)

:=

g

s

(x)];   (

degres

)(dj.xpn.) A(

g

s

(x),

g

s

(x))
 [

ref

 {((y1/y2/ ..).1,(y1/y2/ ..).1), ((y1/y2/ ..).2,(y1/y2/ ..).2), ..};] : geldig.
Syntactische expansie (synonymie):
[2b3]  ·[

g

s

( x)

:=

d

s

];   (syn.xpn.:Sk±1,snn.) A(

d

s

,

d

s

) : geldig.
 [

ref

 {(((x1/x2/ ..).c0),(x1/x2/ ..).c0)))};]
 [

ref

 {(x1,x1)/(x2,x2)/ ..};]
[2b4]  ·[(

d

s

,

d

s

)

:=

(

c

s

,

d

s

)];   (

degres

)(dj.xpn.) A(

c

s

,

d

s

) : 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(

c

s

,

c

s

)}  [

ref

 {(x1,x1)/(x2,x2)/ ..};]
 ·[(

c

s

,

c

s

)

:=

(

c

s

,

d

s

)];
 (

degres

)(dj.xpn.) A(

c

s

,

d

s

) : 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(

c

s

) ¬B(

c

s

));
 [

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(

c

s

) ¬B(

d

s

));
 [

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)

:=

d

s

];  (

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

:=

d

d];  (

degres

) (cj.rdc.:inst.) (A(x), B(

d

d)) : geldig.
 [

ref

 {(A1,B.d1), (A2,B.d1), ..};]
 [

ref

 {A1,A2, .., B.d1};]
[2a2]   C2·[

d

d

:=

d

s

];  (

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};]
[2b] Route 2.
[2b1]  C2·[x

:=

g

d(z);z

:=

x];  (

degres

)(cj.rdc.:inst.) (A(x), B(

g

d( x))) : geldig.
 [

ref

 {(A1,(B*).1), (A2,(B*).2), ..};]
 [

ref

 {A1,A2, .., (B*).1,(B*).2, ..};]
[2b2]  C2·[

g

d(x)

:=

d

s

];   (

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·[

g

s

( w)

:=

d

s

];   (

upgrad

)(dj.rdc.:Sk±1) (A(x), C_(w,

d

s) ) :

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

:=

g

d (y);y

:=

x];  (

degres

)(cj.rdc.:inst.) (A(x), B(

g

d(x ))) : geldig.
 [

ref

 {(A1,(B*).1), (A2,(B*).2), ..};]
 [

ref

 {A1,A2, .., (B*).1,(B*).2, ..};]
[2a2]  ·[

g

d(x)

:=

g

s

(x)];   (

degres

)(dj.xpn.:Sk+1) (A(x ), B(

g

s

(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

:=

c

d )];  (

degres

) (cj.rdc.:inst.) (A(

c

d), B(

c

d))
 [

ref

 {A.c1,B.c1};] : geldig.
[2a2]  ·[

c

d

:=

c

s

];  (

degres

)(dj.xpn.1:Sk+1) (A(

c

s

), B(

c

s

)) : 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

:=

f

d (y);y

:=

x];  (

degres

)(cj.rdc.1:inst.) (A(

f

d(x)), B(

f

d(x)))
 [

ref

 {((A*).1,(B*).1), ((A*).2,(B*).2), ..};] : geldig.
[2b2]  ·[

f

d(x)

:=

f

s

(x)];   (

degres

)(dj.xpn.1:Sk+1) (A(

f

s

(x)), B(

f

s

( x)))
 [

ref

 {((A1/A2/ ..).1,(B1/B2/ ..).1), ((A1/A2/ ..).2,(B1/B2/ ..).2), ..};] : geldig.
[2b3]  ·[x

:=

c

d];  (

degres

) (cj.rdc.:inst.) (A(

f

s

(

c

d )), B(

f

s

(

c

d))
 [

ref

 {(A1/A2/ ..).c1, (B1/B2/ ..).c1)};] : geldig.
[2b4(=2a2)] Syntactische reductie:
 ·[

f

s

(

c

d)

:=

c

s

];   (syn.rdc.:Sk±1,snn.) (A(

c

s

), B(

c

s

)) : 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(

c

s

 ), 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·[

c

s

:=

d

s];  (

degres

) (dj.xpn.) (A(

c

s

), B(

d

s

));
 {(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.: (d

PDL

=

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.: (d

PDL

=

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.: (d

PDL

=

2):
 (d

PPL

=

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(

c

s

), B(

c

s

) ) , (x y ¬(A(x), B(x) ) ) );
 ((A(

c

s

), B(

c

s

) , (x y (¬A(x) ¬B(y ) ) ) );
 (A(

c

s

), B(

c

s

) , (¬A(x) ¬B(y ) ) );
[1] Route 1.
 (A(

c

s

), B(

c

s

) , ¬A(x) );
  : sluit.
[2] Route 2.
 (bas.dist.) ((A(

c

s

), B(

c

s

) , ¬A(x)) (A(

c

s

), B(

c

s

) , ¬B(y) ) );
 (2xlok.cj.rei.) ((A(

c

s

), B(

c

s

) , ¬A(

c

s

) , ¬A(x)) (A(

c

s

), B(

c

s

) , ¬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(

c

s), 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·[

c

s

:=

d

s];  (

degres

) (dj.xpn.) (A(

c

s)), C_(x,

d

s)) : 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(

f

s(x)), C_(x,

f

s(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

:=

c

d ];  (

degres

)(cj.rdc.:inst.)) (A(

f

s(

c

d)), 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·[

f

s(

c

d)

:=

c

s

];   (syn.rdc.:Sk±1,snn.) (A(

c

s

), C_(x,

f

s

(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(

c

s

), ¬B(

c

s

));
 (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(

c

s

), ¬B(

d

s

))
 (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(

c

s

), ¬B(

d

s

));
 [

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,

d

s) ) :

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,

d

s)); :

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·[

d

s

:=

g

s

(w))];   (

degres

)(dj.xpn.) (A(x) C_(w,

g

s

(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·[

d

s

:=

g

s

(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

:=

d

d];  (

upgrad

) (cj.xpn.:diff.) (A(x) B(

d

d))
 [

ref

 {(A1/B.d1), (A2/B.d1), ..};]  [

ref

 {(A1,A2, ..)/ B.d1};] :

ongeldig

.
[2b2a] Route 2.2. Vervolgafleiding, geldig:
[2b2a1]  D2·[

d

d

:=

d

s

];  (

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(

g

d(x)))
 [

ref

 {(A1/(B*).1), (A2/(B*).2), ..};] :

ongeldig

.
[2c2a] Route 3.2. Vervolgafleiding, geldig:
[2b2a1]  D2·[

g

d(x)

:=

g

s

(x)];   (

degres

)(dj.xpn.) (A(x) B(

g

s

(x)))
 [

ref

 {(A1/(B1/B2/..).1), (A2/(B1/B2/..).2), ..};] : geldig.
[2c2a2a] Route 3.2.2. Vervolgafleiding, ongeldig:
[2c2a2a1]  D2·[x:=

d

d];  (

degres

)(cj.rdc.:inst.) (A(x) B(

g

s

(

d

d))) :

ongeldig

.
 [

ref

 {(A1/(B1/B2/..).d1), (A2/(B1/B2/..).d1), ..};]
 [

ref

(compr.1) {(A1,A2, ..)/ (B1/B2/..).d1};]
[2c2a2a2]  D2·[

g

s

(

d

d)

:=

d

s

 ];  (syn.rdc.:Sk±1,snn.) (A(x B(

d

s

)) : 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(

g

s

(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(

g

d(x)))
 [

ref

 {(A1/(B*).1), (A2/(B*).2), ..};] :

ongeldig

.
[2b2a] Route 2.2. Vervolgafleiding, geldig:
[2b2]  ·[

g

d(x)

:=

g

s

(x)];   (

degres

)(dj.xpn.) (A(x) B(

g

s

(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,

g

s

(x))}
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};]
[2]   C2·[x

:=

w];   (

upgrad

)(cj.xpn.) (A(x) C_(w,

g

s

(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

:=

c

d )];  (

degres

)(cj.rdc.:inst.) (A(

c

d) B(

c

d ))
 [

ref

 {A.c1/B.c1};] : geldig.
[2a2]  ·[

c

d

:=

c

s

];  (

degres

)(dj.xpn.1) (A(

c

s

) B(

c

s

)) : geldig.
 [

ref

 {(A1,B1)/(A2,B2)/ ..};]
 [

ref

 {A(1/2/ ..).c0/ B(1/2/ ..).c0};]
Basale Disjunctieve reïteratie:
[2a3]  D2·[

c

s

:=

d

s];  (dj.rei.) (A(

c

s

) B(

d

s

))
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm, [2] : geldig.
Alternatief spoor:
[2b1]  ·[x

:=

f

d (y);y

:=

x];  (

degres

)(cj.rdc.1:inst.) (A(

f

d(x)) B(

f

d(x)))
 [

ref

 {((A*).1/(B*).1),((A*).2/(B*).2), ..};] : geldig.
[2b2]  ·[

f

d(x)

:=

f

s

(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]  ·[

f

d(x)

:=

c

s

];   (

degres

)(cj.rdc.2.) (A(

c

s

) B(

c

s

)) : geldig.
 [

ref

 {(A1/A2/ ..).c0/ (B1/B2/ ..).c0};]
 [

ref

 {(A1/B1)/(A2/B2)/ ..};]
[2b4(=2a3)] Basale Disjunctieve reïteratie:
 D2·[

c

s

:=

d

s];  (dj.rei.) (A(

c

s

) B(

d

s

))
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(

c

s

 ) B(

c

s

)}
 (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·[

c

s

:=

d

s];  (dj.rei.) (A(

c

s

) B(

d

s

))
 [((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(

c

s

) B(

c

s

) ) , ( x y ¬(A(x) B(y) ) ) );
 ((A(

c

s

) B(

c

s

) ) , ( x y (¬A(x), ¬B( y) ) ) );
 ((A(

c

s

) B(

c

s

) ) , ¬A(x), ¬B( y) );
 (trf.ctd.) (A(

c

s

) , ¬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(

c

s) C_(x,

c

s)}
 [

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·[

c

s

:=

d

s];  (Sk+1,dj.rei.) (A(

c

s) C_(x,

d

s))
((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(

f

s(x)) C_(x,

f

s(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·[

f

s(x)

:=

c

s; ];  (

degres

) (dj.rei.) (A(

c

s) C_(x,

f

s(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.