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,

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

ref

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

ref

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

ongeldig

.
[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))}
 [

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,

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

)
 [

ref

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

ref

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

d

s

,

d

s

)

:=

(

c

s

,

d

s

)];  (

upgrad

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

c

s

,

d

s

)
 [

ref

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

ref

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

[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

)
 [

ref

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

ref

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

d

s

,

d

s

)

:=

(

c

s

,

d

s

)];  (

degres

)
(dj.xpn.) A(

c

s

,

d

s

)
 [

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(

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

)
 [

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(

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))
 [(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, ..};]
: 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,

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

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,

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

ref

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

ref

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

d

d

:=

d

s

];  (

degres

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

d

s

))
 [

ref

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

ref

(compr.)
{A1,A2, .., (B1/B2/ ..).d0};]
: geldig.
[2b] Route 2.
[2b1]  C2·[x

:=

g

d(z );z

:=

x];  (

degres

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

g

d(x)))
 [

ref

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

ref

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

g

d(x)

:=

d

s

];  (

degres

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

d

s

))
 [

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,

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

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

:=

g

d(y); y

:=

x];  (

degres

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

g

d(x)))
 [

ref

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

ref

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

g

d(x)

:=

g

s

(x)];  (

degres

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

g

s

(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

:=

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

))
 [

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

:=

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

g

s

(

c

d )

:=

c

s

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

c

s

), B(

c

s

))
 [

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'.
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) ) );
 [(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.: (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))
 [

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(

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

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

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

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(

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

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(

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

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,

d

s));
 [

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

d

s

:=

g

s

(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

:=

d

s

];  (

upgrad

)
(cj.-dj.cnv.:ssm.) (A(x) B(

d

s

))
 [

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

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

))
 [

ref

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

ref

(compr.1) {(A1,A2, ..)/ (B1/B2/ ..).d0};]
: geldig.

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

ref

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

ref

(compr.1) {(A1,A2, ..)/ (B1/B2/..).d1};]
:

ongeldig

.
[2c2a2a2]  D2·[

g

s

(

d

d)

:=

d

s

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

d

s

))
 [

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

:=

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

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

:=

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

))
 [

ref

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

ref

{A(1/2/ ..).c0/ B(1/2/ ..).c0};]
: geldig.
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

))
 [

ref

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

ref

{(A1/B1)/(A2/B2)/ ..};]
: geldig.
[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) ) };
 [(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(

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

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(

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

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.