Introductie_Predikatenlogica_PDL_Deel_VIb_H_14_2

Cursus / training:

Methode Formele Logica

^©

14.2.2. Argument-unificatie/ Kwantor-samenvoeging ; In Conjunctie.

LQ14 - UNIF - CJ : (a1a)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabelen, meervoudig, naar variabele.

Via hernoeming (renaming).

U-kwantor samenvoeging, in Conjunctie, simpele vorm.

Met ongelijknamige predikaten.
(a1a-1):

Bijv.: [1] {(

x A(x) ) , (

y B( y) ) }

C2·[y

:=

x];

_(cj.rei.) (

x (A(x), B(x) ) ) : geldig.

U-kwantor buitenplaatsing.
[2]

_(snn.) (prenex): {

y (A(x), B(y ) ) } : geldig.

_(Skl.) {A(x), B(y)}

[

(

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

(

y (¬A(x)

¬B(y)) );]
[

((

x ¬A(x))

(

y ¬B(y)) );]

_(Skl.) (¬A(

c

_s)

¬B(

d

_s))

[

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

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

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

Basale Syntactische reductie.
[3]

C2·[y

:=

x];

_(cj.rei.) (A(x), B(x)) : geldig.

[

(

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

[Bijv.: (d

=

2):
({(A1,A2), (B1,B2)}

{(A1,B1), (A2,B2)} );
Distributie:

({(A1,B1),(A1,B2), (A2,B1),(A2,B2)}

_(cj.db.rdc.)

{(A1,B1), (A2,B2)} )].

Met behoud van Existentiële kwantificatie c.q. 'Skolem' constante.
(a1a-2):

Bijv.: [1] {(

x A(x) ) , (

w C_(w,y) ) }

C2·[w

:=

x];

_{(ren.,cj.db.rdc.)} (

x (A(x), C_(x,y))) : geldig.

_(snn.) (prenex): [1] {

w (A(x), C_(w,y) ) };

_(Skl.) {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.1)} {(A1,(C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..))/ (A2,(C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..))/ ..};]
[

_{ref
(compr.2)} {(A1,A2, ..), (C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]

U-kwantor samenvoeging, waarna E-kwantor Buitenplaatsing, Volgorde-behoudend.
Basale Syntactische doublure-eliminatie:
[2]

·[w

:=

x];

_{(ren.,cj.db.rdc.)} (A(x), C_(x,

d

_s) ) : geldig.

[

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

_ref
(compr.) {(A1,A2, ..), (C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]

(

x (A(x), C_(x,y))).

(a1a-3):

Bijv.: [1] ((

x A(x)), (

y C_(w,y)))

·[w

:=

x];

_{(ren.,cj.db.rdc.)} {

y (A(x), C_(x,y))} : geldig.

_(Skl.) [1] (A(x), C_(w,

g

_s(w)))

[

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

_ref
(compr.) {A1,A2, .., C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..};]

_(snn.) (prenex) (

x (A(x), C_(w,y)));

[2]

D2·[x

:=

w];

_{(ren.,cj.db.rdc.)} {A(x), C_(x,

g

_s(x))} : geldig .

[

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

_ref
(compr.) {A1,A2, .., C1.((1/2/ ..).1),C2.((1/2/ ..).2), ..};]

(a1b)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' constante.

(a1b-1):

Bijv.: {(

x A(x) ) , (

y B(y ) ) }

_(degres
)_{(cj.rdc.;dj.xpn.)} (

x (A(x), B(x) ) ) : geldig.
U-kwantor buitenplaatsing.

_(snn.) (prenex): {

y (A(x), B(y))}

_(degres
)_{(cj.rdc.;dj.xpn.)} (

x (A(x), B(x))) : geldig.

_(Skl.) [1] {A(x), B(y)}

[

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

_{ref
(distr.1)} {(A1,(B1,B2, ..).1)/ (A2,(B1,B2, ..).2)/ ..};]
[

_{ref
(distr.2)} {(A1,B1),(A1,B2), ..(A2,B1),(A2,B2), ..};]

[2a] Route 1.

[2a1]

·[y

:=

d

_d];

_(degres
)_{(cj.rdc.:inst.1)} (A(x), B(

d

_d)) : geldig.

[

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

_{ref
(distr.1)} {(A1,(B*).d1),(A2,(B*).d1), ..};]

[2a2]

·[x

:=

d

_d];

_(degres
)_{(cj.rdc.:inst.2)} (A(

d

_d), B(

d

_d))
[

_ref {(A*).d1, (B*).d1};] : geldig.

[2a3]

·[

d

_d:=

d

_s];

_(degres
)_{(dj.xpn.:Sk+1)} (A(

d

_s), B(

d

_s)) : geldig.

[

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

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

Zie verder: E-kwantor splitsing, in Conjunctie, simpele vorm, [1-2] (geldig).

[2b] Route 2.

[2b1]

·[y

:=

g

_d(z)];

_(degres
)_{(cj.rdc.:inst.1)} (A(x), B(

g

_d(z))) : geldig.

[

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

_{ref
(distr.1)} {(A1,(B*).1), (A1,(B*).2), .., (A2,(B*).1), (A2,(B*).2), ..};]

[2b2]

·[x

:=

g

_d(z); z

:=

x];

_(degres
)_{(cj.rdc.:inst.2)} (A(

g

_d(x)), B(

g

_d(x))) : geldig.

[

_ref {((A*).1,(B*).1), ((A*).2,(B*).2), ..};]
[

_ref {(A*).1,(A*).2, .. (B*).1,(B*).2, ..};]

[2b3]

·[

g

_d(x)

:=

g

_s(x)];

_(degres
)_{(dj.xpn.:Sk+1)} (A(

g

_s(x))

g

_s(x))) : geldig.

[

_ref {((A1/A2/ ..).1, (B1/B2/ ..).1), ((A1/A2/ ..).2, (B1/B2/ ..).2), ..};]

[2b4]

·[x

:=

d

_d];

_(degres
)_{(cj.rdc.:inst.)} (A(

g

_s(

d

_d))

g

_s(

d

_d )) )
[

_ref {((A1/A2/ ..).d1), ((B1/B2/ ..).d1), ..};] : geldig.

[2b5(=2a3)]

·[

g

_s(

d

_d)

:=

d

_s];

_{(syn.rdc.:Sk±1,snn.)} (A(

d

_s), B(

d

_s)) : geldig.

[

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

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

Zie verder: E-kwantor splitsing, in Conjunctie, simpele vorm, [1-2] (geldig).

(a2a)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' functie.

(a2a-1):

Bijv.: [1] {(

x A(x) ) , (

w C_(w,y) ) }

C2·[w

:=

x];

_{(degres
)(dj.xpn.)} (

y (A(x), C_(x,y) ) ) : geldig.

_(snn.) (prenex): [1] (

w (A(x), C_(w,y)));

_(Skl.)

_(Skl.) [1] {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.2x)} {A1,A2, .. C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..};]

De C term (Literaal) is hier wegens Conjunctie onafhankelijk interpreteerbaar.
In dit geval althans omdat de conjuncte predicaties geen gemeenschappelijke existentële variabelen hebben.

[2a] Route 1.
Met basale 'EU-UE' kwantor volgordeverandering.

Basale Syntactische doublure-eliminatie:
[2a1]

C2·[w

:=

x];

_{(cj.db.rdc.:ren.,unif.)} (A(x), C_(x,

d

_s) ) : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..};]

(prenex) (

x (A(x), C_(x,y))).

Lokale Disjunctieve expansie:
[2a2(=2b2;=2c2)]

·[

d

:=

g

_s(x)];

_{(degres
)(dj.xpn.:Sk±1)} (A(x), C_(x,

g

_s(x) ) : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

(prenex) (

y (A(x), C_(x,y))).

[2b] Route 2.
Met lokale 'EU-UE' kwantor volgordeverandering.

Lokale Disjunctieve expansie:
[2b1]

·[

d

:=

g

_s(w)];

_{(degres)(dj.xpn.:Sk±1)} (A(x), C_(w,

g

_s(w) )
[

_ref {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};] : geldig.

{(

x A(x) ) , (

y C_(w,y) ) };

_(snn.) (prenex) (

x (A(x), C_(w,y))).

Basale Conjunctieve reïteratie:
[2b2(=2a2)]

C2·[w

:=

x];

_{(cj.db.rdc.:ren.,unif.)} (A(x), C_(x,

g

_s(x) ) : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

(prenex) (

y (A(x), C_(x,y))).

[2c] Route 3.
Via - volgordebehoudende - prenex vorm.

U-kwantor buitenplaatsing; E-kwantor buitenplaatsing.
Lokale Disjunctieve expansie:
[2c1]

·[

d

:=

g

_s(x)];

_{(degres)(dj.xpn.:Sk±1)} (A(x), C_(w,

g

_s(x) ) : geldig.

[

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

_ref {A1,A2, .. C1.((1/2/ ..).1), C1.((1/2/ ..).2), .. C2.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

{

y (A(x) , (

w C_(w,y) ) ) };

_(snn.) (prenex) {

w (A(x), C_(w,y) ) };

Lokale Conjunctieve reductie:
[2c2(=2a2;2b2)]

C2·[w

:=

x];

_(degres
)_{(cj.rdc.:ren.,unif.)} (A(x), C_(x,

g

_s(x) ) : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

(prenex) (

y (A(x), C_(x,y))).

[2d] Route 4.

Lokale Disjuncte expansie:
[2d1]

·[

d

:=

g

_s(z)];

_(degres
) _(dj.xpn.) {A(x), C_(w,

g

_s(z) )} : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C1.((1/2/ ..).2), ..
C2.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

{(

x A(x) ) , (

w C_(w,y) ) };

_(snn.) (prenex) (

w (A(x), C_(w, y))).

Lokale Conjuncte reductie:
[2d2(=2b1)]

·[z

:=

w];

_(degres
)_{(cj.rdc.:ren.)} {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.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

{(

x A(x) )

(

y C_(w,y) ) };

_(snn.) (prenex) (

x (A(x), C_(w,y))).

Basale Syntactische doublure-eliminatie:
[2d3(=2a2;=2b2;=2c2)]

·[w

:=

x];

_{(cj.rei.;ren.)} {A(x), C_(x,

g

_s(x))} : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

(prenex) (

y (A(x), C_(x,y))).

[2e] Route 5.

Disjuncte expansie:
[2e1]

·[

d

:=

g

_s(w,z)];

_{(degres
)}_(dj.xpn.) {A(x), C_(w,

g

_s(w,z) )} : geldig.

[

_ref {(A1,C1.((1/2/ ..).1.1)), (A1,C1.((1/2/ ..).1.2)), .. (A1,C2.((1/2/ ..).2.1)), (A1,C2.((1/2/ ..).2.2)), ..
(A2,C1.((1/2/ ..).1.1)), (A2,C1.((1/2/ ..).1.2)), .. (A2,C2.((1/2/ ..).2.1)), (A2,C2.((1/2/ ..).2.2)), ..};]
[

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1.1), C1.((1/2/ ..).1.2), ..
C2.((1/2/ ..).2.1), C2.((1/2/ ..).2.2), ..};]

{(

x A(x) )

(

y (A(x), C_(w,y) ) };

_(snn.) (prenex) (

x (A(x),

C_(w,y))).

Conjuncte reductie:
[2e2]

·[z

:=

w];

_(degres
)_{(cj.rdc.:ren.)} {A(x), C_(w,

g

_s(w ,w))} : geldig.

[

_ref {(A1,C1.((1/2/ ..).1.1)), (A1,C2.((1/2/ ..).2.2)), .. (A2,C1.((1/2/ ..).1.1)), (A2,C2.((1/2/ ..).2.2)), ..};]
[

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1.1), C2.((1/2/ ..).2.2), ..};]

{(

x A(x) ) , (

y C_(w,y) ) };

_(snn.) (prenex) (

x (A(x), C_(w,y))).

Lokale Syntactische reductie (synonymie):
[2e3(=2b1;=2d2)]

C2·[

h

_s(w ,w)

:=

g

_s(w)];

_{(syn.rdc.:Sk±1,snn.)} (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.) {A1,A2, .. C1.((1/2/ ..).1.1), C2.((1/2/ ..).2.2), ..};]

{(

x A(x) ) , (

y C_(w,y) ) };

_(snn.) (prenex) (

x (A(x)

C_(w,y))) : geldig.

Basale Syntactische doublure-eliminatie:
[2e4(=2a2;=2b2;=2c2;=2d3)]

·[w

:=

x];

_{(cj.rei.;ren.)} {A(x), C_(x,

g

_s(x))} : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1)), C2.((1/2/ ..).2)), ..};]

(prenex) (

y (A(x), C_(x,y))).

[2f] Route 6 (ongeldige uitkomst).

Lokale Syntactische expansie (synonymie):
[2f1]

·[

d

:=

g

_s(

d

_d)];

_{(syn.rdc.:Sk±1,snn.)} {A(x), C_(w,

g

_s(

d

_d) )} : geldig.

[

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

_ref
(compr.) {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

{(

x A(x) ) , (

w ((z

=

d

_d)

C_(w,y) ) ) }.

_(snn.) (prenex) (

w (A(x), ((z

=

d

_d)

C_(w,y) ) ) ).

Lokale Conjunctieve expansie (generalisatie):
[2f2(=2b1;=2d2;=2e3)]

·[

d

:=

w ];

_(upgrad
)_{(cj.xpn.:gnr.)} {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 {A1,A2, .. C1.((1/2/ ..).1)), C2.((1/2/ ..).2)), ..};]

(prenex)

z (A(x), C_(w,z))).

Basale Conjuncte reïteratie:
[2f3(=2a2;=2b2;=2c2;=2d3;=2e4)]

·[w

:=

x];

_{(degres
)(cj.rei.;snn.)} (A(x), C_(x,

g

_s(x) ) : geldig.

[

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

_ref {A1,A2, .. C1.((1/2/ ..).1), C2.((1/2/ ..).2), ..};]

(prenex) (

y (A(x), C_(x,y))).

(a2b)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, via 'Skolem' functie.

(a2b-1):

Bijv.: [1] {(

x A(x), (

y B(y ))}

_(degres
)_{(cj.rdc.;dj.xpn.)} (

x (A(x), B(x)) : geldig.

_(snn.) (prenex) {

y (A(x), B(y))}

_(degres
)_{(cj.rdc.;dj.xpn.)} (

x (A(x), B(x))) : geldig.

_(Skl.) [1] {A(

c

_s), B(y )}

[

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

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

[2a] Route 1.

Lokale Conjunct-Disjunct reductie:
[2a1]

·[y

:=

c

_s ];

_(degres
)_{(cj.rdc.:inst.)} (A(

c

_s), B(

c

_s) : geldig.

[

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

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

[2b] Route 2 (ongeldige uitkomst).

Lokale Conjuncte reductie:
[2b1]

·[y

:=

d

_d];

_(degres
)_{(cj.rdc.:inst.)} (A(

c

_s), B(

d

_d)) : geldig.

[

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

_ref {(A1/A2/ ..).c0, (B*).d1};]

Lokale Disjuncte expansie:
[2b2]

·[

d

:=

d

_s];

_(degres
)_{(dj.xpn.:Sk+1)} (A(

c

_s), B(

d

_s)) : geldig.

[

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

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

Zie verder: E-kwantor samenvoeging, in Conjunctie, simpele vorm, [1-2] (

ongeldig

(a3)

Argument-unificatie/ Kwantor-samenvoeging; vanuit variabele, meervoudig, naar 'Skolem' constanten.

(a3-1):

Bijv.: {(

x A(x), (

y B(y))}

_(degres
)_{(cj.rdc.;dj.xpn.;dj.rdc.)} (

y (A(y), B(y)) : geldig.

_(snn.) (prenex) [1] {

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

_(Skl.) [1] {A(x), B(

d

_s )}

[

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

[2a] Route 1.

Lokale Conjunct-Disjunct reductie:
[2a1]

·[x

:=

c

_s ];

_(degres
)_{(cj.-dj.rdc.:inst.)} (A(

c

_s), B(

c

_s)) : geldig.

[

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

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

[2b] Route 2 (ongeldige uitkomst).

Lokale Conjuncte reductie:
[2b1]

·[x

:=

c

_d];

_(degres
)_{(cj.rdc.:inst.)} (A(

c

_d), B(

d

_s)) : geldig.

[

_ref {(A*).c1, (B1/B2/ ..).d0};] [

_ref {(((A*).c1/B1), ((A*).c1/B2), ..).d0};]

Lokale Disjuncte expansie:
[2b2]

·[

c

:=

c

_s];

_(degres
)_{(cj.rdc.;dj.xpn.)} (A(

c

_s), B(

d

_s)) : geldig.

[

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

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

Zie verder: E-kwantor samenvoeging, in Conjunctie, simpele vorm, [1-2] (

ongeldig

[2c] Route 3 (ongeldige uitkomst).
Via directe prenex vorm (werkt niet).

[2c1]

·[

d

:=

g

_s(x)];

_(degres
) _{(dj.xpn.:Sk+1)} {A(x), B(

g

_s(x))} : geldig.

[

_ref {(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};]

_(snn.) (prenex) {

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

[2c2]

·[x

:=

c

_d];

_(degres
)_{(cj.rdc.:inst.)} (A(

c

_d), B(

g

_s(

c

_d)))
: geldig.

[

_ref {(A*).c1, (B1/B2/ ..).c1};]

Syntactische reductie (synonymie):
[2c3]

·[

g

_s(

c

_d)

:=

e

_s];

_{(,syn.rdc.:Sk±1,snn.
)} (A(

c

_d), B(

e

_s)) : geldig.

[

_ref {(A*).c1, (B1/B2/ ..).e0};]

[2c4]

·[

c

:=

c

_s];

_(degres
)_(dj.xpn.) (A(

c

_s), B(

e

_s)) : geldig.

[

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

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

Zie verder: E-kwantor samenvoeging, in Conjunctie, simpele vorm, [1-2] (

ongeldig

E-kwantor samenvoeging, in Conjunctie, simpele vorm.

Met ongelijknamige predikaten.
(a3-2):
'Er is een ding A, èn er is een ding B', wordt: 'Er is een ding dat A èn (tegelijk) B is'.

Bijv.: [1] {(

x A(x) ) , (

y B( y) ) }

C2·[y

:=

x];

(

x (A(x), B(x) ) ) :

ongeldig

_(snn.) (prenex) {

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

_(Skl.) {A(

c

_s), B(

d

_s)}

[

(

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

(

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/..)};]

[Bijv.: {{A1,B2}, {A2,B3}};]

[2]

C2·[

d

:=

c

_s];

_(upgrad
)_(dj.rdc.) (A(

c

_s), B(

c

_s));
[

(

x (A(x), B(x) ) ) :

ongeldig

[

(

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}};]

Aanvullende bewijsvoering.

Zie verder elders.

(a3-3):

Bijv.: [1] {(

y A(y)) , (

x C_(x,z))}

C2·[z

:=

y];

_(upgrad
)_(dj.rdc.) (

y (A(y) , (

x C_(x,y))) ) :

ongeldig

.
E-kwantor buitenplaatsing; U-kwantor buitenplaatsing.

_(snn.) (prenex) [1] {

x (A(y), C_(x,z)) }

C2·[z

:=

y];

_(upgrad
)_(dj.rdc.) (

x (A(y), C_(x,y))) :

ongeldig

_(Skl.) [1] {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/ ..), ..};]

[2]

C2·[

d

:=

c

_s];

_(upgrad
)_(dj.rdc.) (A(

c

_s), C_(x,

c

_s)) :

ongeldig

[

_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, ..))/ ..};]

(a3-4):

Bijv.: [1] {(

y A(y) ) , (

z C_(x,z) ) }

C2·[z

:=

y];

_(degres
)_{(dj.xpn.;dj.rdc.)} (

y (A(y), C_(x,y))) :

ongeldig

_(snn.) (prenex) [1] {

z (A(y), C_(x,z)) };

_(Skl.) [1] {A(

c

_s), C_(x,

g

_s(x))}

[

_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), ..};]

De A term (Literaal) is hier wegens Conjunctie onafhankelijk interpreteerbaar.
In dit geval althans omdat de conjuncte predicaties geen gemeenschappelijke existentële variabelen hebben.
Een Skolem constante, zeg

c

_s, in een éénplaatsige (conjuncte) predicatie is substitueerbaar - onder parafrase - door een nieuw ingevoerde Skolem functie, zeg

f

_s(y ), met een argumentlijst van willekeurige lengte met uitsluitend (universele) variabele(n) als argument (en).
Deze substitueerbaarheid (afleidingsrelatie) is dus wederkerig.

Lokale Syntactische reductie (synonymie):
[2]

C1·[

c

:=

f

_s(y)];

_{(syn.xpn.:Sk±1,snn.)} (A(

f

_s(y)), C_(x,

g

_s(x))) : geldig.

[

_ref {((A1/A2/..).1f,C1.(1/2/ ..)).1g, ((A1/A2/..).1f,C2.(1/2/ ..)).2g, ..
((A1/A2/..).2f,C1.(1/2/ ..)).1g, ((A1/A2/..).2f,C2.(1/2/ ..)).2g, ..};]
[

_ref {(A1/A2/..).1f, (A1/A2/..).2f, .. C1.((1/2/ ..).1g), C2.((1/2/ ..).2g), ..};]

Basale Syntactische reductie (synonymie):
[3]

C1·[y

:=

_{(syn.rdc.:ren.,snn.)} (A(

f

_s(x)), C_(x,

g

_s( x))) : geldig.

[

_ref {((A1/A2/..).1f,C1.(1/2/ ..)).1g, ((A1/A2/..).2f,C2.(1/2/ ..)).2g, ..};]
[

_ref {(A1/A2/..).1f, (A1/A2/..).2f, .. C1.((1/2/ ..).1g), C2.((1/2/ ..).2g), ..};]

[4]

C2·[

g

_s(x)

:=

f

_s(x)];

_(upgrad
)_(dj.rdc.) (A(

f

_s(x)), C_(x,

f

_s(x))) :

ongeldig

[

_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, ..};]

Bewijs via minimaal domein.

Bijv.: (d

=

2):
(((A1/A2).1f, (A1/A2).2f)/ ((C1.1/C1.2).1g, (C2.1/C2.2).2g));
[Bijv.: {((A1).1f, ((A2).2f)/, ((C1.2).1g, (C2.1).2g)};]

_(snn.) (((A1/A2).1f, (A1/A2).2f)/ ((C1.1/C1.2).1f, (C2.1/C2.2).2f)) :

ongeldig

.
[Bijv.: {((A1).1f, (A2).2f)/ ((C1.2).1f, (C2.1).2f)};]