Cursus / training:

Methode Formele Logica

©


14.2.3.

 

Argument-unificatie/ Kwantor-samenvoeging; In Disjunctie.



(a1a)

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


Via hernoeming (renaming).

U-kwantor samenvoeging, in Disjunctie, simpele vorm.


Met ongelijknamige predikaten.
(a1a-1):
Bijv.: [1] {(x A(x)) ( y B(y))}   C2·[y

:=

x];  (

degres

)(cj.rdc.) (x (A(x) B(x))) : geldig .
U-kwantor buitenplaatsing.
[2]  (snn.) (prenex): {x y (A(x) B(y))}
 (Skl.) {A(x) B(y)} [1]
 [(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,A2, ..)/ (B1,B2, ..)};]
 [

ref

(bas.dist.:dj.-cj.) {(A1/(B1,B2, ..).1), (A2/(B1,B2, ..).2), ..};]
 [

ref

(lok.dist.:dj.-cj.) {((A1/B1),(A1/B2), ..), ((A2/B1),(A2/B2), ..), ..};]
 [{(A1/B1),(A1/B2), .., (A2/B1),(A2/B2), .., ..};]
 [Bijv.: {A1/B2/(A1/B3), ..};]
Basale Conjunctieve reductie.
[3]   C2·[y

:=

x];   (

degres

)(cj.rdc.) {A(x) B(x)}
 (x (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), ..};] : geldig.
 [Bijv.: {A1/B2/(A3/B3), ..};]


[Bijv.: (d

=

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

degres

)(cj.rdc.) {(A1/B1), (A2/B2)} )].

Met behoud van Existentiële kwantificatie c.q. 'Skolem' constante.
(a1a-2):
Bijv.: [1] {(x A(x) ) ( y w C_(w,y) ) }   C2·[w

:=

x];   (

degres

)(cj.rdc.) ( y x (A(x) C_(x,y))) : geldig.
 (snn.) (prenex): {y x w (A(x) C_(w,y) ) };
 (Skl.) {A(x) C_(w,

d

s)}
 [

ref

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

ref

 {(A1/(C1.((1/2/ ..).d0),C2.((1/2/ ..).d0), ..))/ (A2/(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)), ..};]
[1a] Route 1.
U-kwantor samenvoeging, waarna E-kwantor Buitenplaatsing, Volgorde-behoudend.
[1a1] Basale Conjunctieve reductie:
  C2·[w

:=

x];   (

degres

)(cj.rdc.) (A(x) C_(x,

d

s) )
 [

ref

 {(A1,C1.((1/2/ ..).d0))/ (A2,C2.((1/2/ ..).d0))/ ..};] : geldig.
 (y x (A(x) C_(x,y))).

[2b] Route 2 (ongeldige uitkomst).
Met 'EU-UE' kwantor volgordeverandering.
E-kwantor buitenplaatsing; U-kwantor buitenplaatsing.
Lokale Disjuntieve expansie:
[2b1]  C2·[

d

s

:=

g

s

(x)];  (

degres

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

g

s

(x))};
 [

ref

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

ref

 {(A1/(C1.((1/2/ ..).1),C2.((1/2/ ..).1), ..)), (A2/(C1.((1/2/ ..).2),C2.((1/2/ ..).2), ..)), ..};] : geldig.
 (snn.) (prenex): {x y w (A(x) C_(w,y) ) }.
Eliminatie van tweede U-kwantor.
Basale Conjunctieve reductie:
[2b2]   C2·[w

:=

x];   (

degres

)(cj.rdc.) (A(x) C_(x,

g

s

(x) ) )
 [

ref

 {(A1/C1.(1/2/ ..).1), (A2/C2.(1/2/ ..).2), ..};] : geldig.
 (x y (A(x) C_(x,y)) ).
[2b3] Lokale Disjunctieve reductie:
  C2·[

g

s

(x)

:=

d

s

];  (

upgrad

)(dj.rdc.) (A(x) C_(x,

d

s ) )
 [

ref

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

ongeldig

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

(a1b)

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



(a1b-1):
Bijv.: {x 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.) (A(x) B(

d

d))
 [

ref

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

ref

(compr.) {((A1,A2, ..)/(B*).d1)};] : geldig.
[2a2]   ·[x

:=

d

d];   (

degres

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

d

d) B(

d

d))
 [

ref

 {(A*).d1/ (B*).d1};] : geldig.
[2a3]  ·[

d

d:=

d

s

];  (

degres

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

d

s

) B(

d

s

))
 [

ref

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

ref

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

ref

 {A1/A2/ .. B1/B2/ ..};] : geldig.
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm, [1-2] (geldig).

[2b] Route 2
[2b1]  ·[y

:=

g

d(z )];  (

degres

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

g

d(z)))
 [

ref

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

ref

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

:=

g

d(z); z

:=

x];  (

degres

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

g

d(x)) B(

g

d(x)))
 [

ref

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

ref

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

ref

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

g

d(x)

:=

g

s

(x)];  (

degres

) (dj.xpn.) (A(

g

s

(x)) B(

g

s

(x)))
 [

ref

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

:=

d

d];   (

degres

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

g

s

(

d

d)) B(

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

))
 [

ref

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

ref

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

ref

 {A1/A2/ .. B1/B2/ ..};] : geldig.
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm, [1-2] (geldig).

(a2a)

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



(a2a-1):
Andere categorie:
Bijv.: [1] {(x A(x) ) ( y w C_(w,y) ) }   C2·[w

:=

x];   (

degres

)(dj.xpn.) (x y (A(x) C_(x,y) ) ) : geldig.
 (snn.) (prenex): [1] (y x w (A(x) C_(w,y)));
 (Skl.) [1] {A(x)) C_(w ,

d

s))}
 [

ref

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).d0)), (A1/C2.((1/2/ ..).d0)), ..), ((A2/C1.((1/2/ ..).d0)), (A2/C2.((1/2/ ..).d0)), ..) ..};]
De C term (Literaal) is hier wegens Disjunctie niet automatisch onafhankelijk interpreteerbaar.
In dit geval echter wel omdat de disjuncte predicaties geen gemeenschappelijke (universele/ existentële) variabelen hebben.
[2a] Route 1.
Met basale 'EU-UE' kwantor volgordeverandering.
Basale Conjunctieve reductie:
[2a1]   C2·[w

:=

x];   (

degres

)(cj.rdc.:ren.,unif.) (A(x) C_(x,

d

s) )
 [

ref

 {(A1/C1.((1/2/ ..).d0)), (A2/C2.((1/2/ ..).d0)), ..};] : geldig.
 (prenex): (y x (A(x) C_(x,y)));
Lokale Disjunctieve expansie:
[2a2]  ·[

d

s

:=

g

s

(x)];  (

degres

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

g

s( x) )
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x) C_(x,y))).

[2b] Route 2.
Met lokale 'EU-UE' kwantor volgordeverandering.
Lokale Disjunctieve expansie:
[2b1]  ·[

d

s

:=

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).1)), (A1/C2.((1/2/ ..).2)), ..), ((A2/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..) ..};] : geldig.
 {(x A(x) ) (w y C_(w,y) ) };
 (snn.) (prenex): (w y x (A(x) C_(w,y))).
Basale Conjunctieve reductie:
[2b2(=2a2)]   C2·[w

:=

x];   (

degres

)(cj.rdc.:ren.,unif.) (A(x) C_(x,

g

s

(x) )
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x) C_(x,y))).

[2c] Route 3.
Via - volgordebehoudende - prenex vorm
U-kwantor buitenplaatsing; E-kwantor buitenplaatsing.
Lokale Disjunctieve expansie:
[2c1]  ·[

d

s

:=

g

s

(x)];  (

degres

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

g

s( x) )
 [

ref

 {((A1/C1.((1/2/ ..).1)), (A1/C2.((1/2/ ..).1)), ..), ((A2/C1.((1/2/ ..).2)), (A2/C2.((1/2/ ..).2)), ..) ..};] : geldig.
 {x y (A(x) (w C_(w,y ) ) ) };
 (snn.) (prenex): {x y 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) )
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x) C_(x,y))).

[2d] Route 4.
Lokale Disjuncte expansie:
[2d1]  ·[

d

s

:=

g

s

(z)];  (

degres

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

g

s (z) )}
 [

ref

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

ref

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

ref

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

ref

(distr.3) {(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)), ..};] : geldig.
 {(x A(x) ) (z y w C_(w,y) ) };
 (snn.) (prenex): (z y x w (A(x) C_(w,y))).
Lokale Conjuncte reductie:
[2d2(=2b1)]  ·[z

:=

w];   (

degres

)(cj.rdc.:ren.,unif.) {A(x) C_(w,

g

s(w))}
 [

ref

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).1)), (A1/C2.((1/2/ ..).2)), ..), ((A2/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..) ..};] : geldig.
 {(x A(x) ) (w y C_(w,y) ) };
 (snn.) (prenex): (w y x (A(x) C_(w,y))).
Basale Conjuncte reductie:
[2d3(=2a2;=2b2;=2c2)]  ·[w

:=

x];   (

degres

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

g

s(x))}
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x) C_(x,y))).

[2e] Route 5.
Lokale Disjuncte expansie:
[2e1]  ·[

d

s

:=

h

s

(w,z)];  (

degres

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

g

s(w,z) )}
 [

ref

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

ref

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

ref

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

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)), ..};] : geldig.
 {(x A(x) ) (w z y (A(x) C_(w,y) ) };
 (snn.) (prenex): (w z y x (A(x) C_(w,y))).
Lokale Conjuncte reductie:
[2e2]  ·[z

:=

w];   (

degres

)(cj.rdc.:ren.,unif.) {A(x) C_(w,

h

s(w,w))}
 [

ref

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).1.1)), (A1/C2.((1/2/ ..).2.2)), ..), ((A2/C1.((1/2/ ..).1.1)), (A2/C2.((1/2/ ..).2.2)), ..) ..};] : geldig.
 {(x A(x) ) (w y C_(w,y) ) };
 (snn.) (prenex): (w y x (A(x) C_(w,y))).
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) )
 [

ref

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).1)), (A1/C2.((1/2/ ..).2)), ..), ((A2/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..) ..};] : geldig.
 {(x A(x) ) (w y C_(w,y) ) };
 (snn.) (prenex): (w y x (A(x) C_(w,y))).
Basale Syntactische doublure-eliminatie:
[2e4(=2a2;=2b2;=2c2;=2d3)]  ·[w

:=

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

g

s(x))}
 [

ref

 {(A1/C1.((1/2/ ..).1)), (A2/C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x), C_(x,y))).

[2f] Route 6 (ongeldige uitkomst).
Lokale Syntactische expansie (synonymie):
[2f1]  ·[

d

s

:=

g

s

(

d

d)];   (syn.rdc.:Sk±1,snn.) {A(x) C_(w,

g

s (

d

d) )}
 [

ref

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

ref

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

ref

(distr.2) {((A1/C1.((1/2/ ..).d1)), (A1/C2.((1/2/ ..).d1)), ..), ((A2/C1.((1/2/ ..).d1)), (A2/C2.((1/2/ ..).d1)), ..) ..};] : geldig.
 {(x A(x) ) (z y w ((z

=

d

d) C_(w,y) ) ) }.
 (snn.) (prenex): (z y x w (A(x) ((z

=

d

d) C_(w,y) ) ) ).
Lokale Conjunctieve expansie (generalisatie):
[2f2(=2b1;=2d2;=2e3)]  ·[

d

d

:=

w];  (

upgrad

)(cj.xpn.:gnr.) {A(x ), C_(w,

g

s(w))}
 [

ref

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

ref

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

ref

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

ongeldig

.
 (prenex): x w z (A(x), C_(w,z ))).
Basale Conjuncte reïteratie:
[2f3(=2a2;=2b2;=2c2;=2d3;=2e4)]  ·[w

:=

x];  (cj.rei.;snn.) (A(x), C_(x,

g

s (x) )
 [

ref

 {(A1,C1.((1/2/ ..).1)), (A2,C2.((1/2/ ..).2)), ..};] : geldig.
 (prenex): (x y (A(x), C_(x,y))).

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



(a2b-1):
Bijv.: [1] {(x A(x)) ( y B(y))}
 (snn.) [1] (prenex): {x 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,B2, ..)) ..};]
[2a] Route 1.
[2a1] Lokale Conjunct-Disjunct reductie:
 ·[y

:=

c

s

 ];  (

degres

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

c

s

) B(

c

s

)
 [

ref

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

ref

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

ref

 {A1/A2/ .. B1/B2/..};] : geldig.

[2b] Route 2 (ongeldige uitkomst).
[2b1] Lokale Conjuncte reductie:
 ·[y

:=

d

d];   (

degres

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

c

s

) B(

d

d)
 [

ref

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

ref

 {(A1/(B*).d1)/ (A2/(B*).d1)/ ..};] : geldig.
Lokale Disjuncte expansie:
[2b2]  ·[

d

d

:=

d

s

];  (

degres

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

c

s

) B(

d

s

))
 [

ref

 {((A1/A2/ ..).c0)/ ((B1/B2/ ..).d0)};] : geldig.
Zie verder: E-kwantor samenvoeging, in Disjunctie, simpele vorm, [1-2] (geldig).

(a3)

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



(a3-1):
Bijv.: [1] {(x A(x)) ( y B(y))}  (

degres

) (x (A(x) B(x ))) : geldig.
 (snn.) [1] (prenex): {y x (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

) )
 [

ref

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

ref

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

ref

 {A1/A2/ .. B1/B2/..};] : geldig.

[2b] Route 2 (ongeldige uitkomst).
Lokale Conjuncte reductie:
[2b1]  ·[x

:=

c

d];   (

degres

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

c

d) B(

d

s

)
 [

ref

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

ref

 {(((A*).c1/B1), ((A*).c1/B2), ..).d0};] : geldig.
Lokale Disjuncte expansie:
[2b2]  ·[

c

d

:=

c

s

];  (

degres

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

c

s

) B(

d

s

))
 [

ref

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

ref

(distr.) {(A1/B1)/(A1/B2)/ .. (A2/B1)/(A2/B2)/ ..};] : geldig.
Zie verder: E-kwantor samenvoeging, in Disjunctie, simpele vorm, [1-2] (geldig).

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

d

s

:=

g

s

(x)];  (

degres

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

g

s

(x))}
 [

ref

 {(A1/(B1/B2/ ..).1), (A2/(B1/B2/ ..).2), ..};] : geldig.
 (snn.) (prenex): {x y (A(x) B(y))}
[2c2]  ·[x

:=

c

d];   (

degres

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

c

d) B(

g

s

(

c

d )))
 [

ref

 {(A*).c1/ (B1/B2/ ..).c1};] : geldig.
Syntactische reductie (synonymie):
[2c3]  ·[

g

s

(

c

d)

:=

e

s

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

c

d) B(

e

s

))
 [

ref

 {(A*).c1/ (B1/B2/ ..).e0};] : geldig.
[2c4]  ·[

c

d

:=

c

s

];  (

degres

)(dj.xpn.) (A(

c

s

) B(

e

s

))
 [

ref

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

ref

(distr.) {(A1/B1)/(A1/B2)/ .. (A2/B1)/(A2/B2)/ ..};] : geldig.
Zie verder: E-kwantor samenvoeging, in Disjunctie, simpele vorm, [1-2] (geldig).

E-kwantor samenvoeging, in Disjunctie, simpele vorm.



Met ongelijknamige predikaten.
(a3-2):
'Er is een ding A, en/of er is een ding B', wordt: 'Er is een ding dat A en/of B' is.
Bijv.: [1] {(x A(x) ) ( y B(y) ) }  (cj.db.rdc.) (x (A(x) B(x) ) ) : geldig.
 (snn.) (prenex): {x y (A(x) B(y) ) };
 (Skl.) {A(

c

s

) B(

d

s

)}
 [(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}};]
Basale Syntactische doublure-eliminatie:
[2]  C2·[

d

s

:=

c

s];  (ssm.,cj.db.rdc.) (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/ ..};] : geldig.
 [Bijv.: {{A1/B1}/ {A3/B3}};]

Aanvullende bewijsvoering.


Direct bewijs, via minimaal domein.


Bijv.: (d

PDL

=

3):
{(x A(x) ) ( y B(y) ) }
 

ref

 ((A1/B1)/(A1/B2)/ (A2/B1)/(A2/B2));
 (cj.db.rdc.) (x (A(x ) B(x) ) );
 

ref

 ((A1/B1)/(A2/B2)) : geldig.

Bijv.: (d

PDL

=

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

(snn.) (A1/B1/A1/B2/A1/B3/ A2/B1/A2/B2/A2/B3/ A3/B1/A3/B2/A3/B3);
 (cj.db.rdc.) (x (A(x ) B(x) ) );
 

ref

 ((A1/B1)/ (A2/B2)/ (A3/B3))
 

ref

(snn.) (A1/A2/A3/ B1/B2/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) ) ( y B(y) ) }
Prm. 1.1.
 

ref

 ((A1/B1)/ (A1/B2)/ (A2/B1)/ (A2/B2));
 

ref

(snn.) (A1/B1/A1/B2/ A2/B1/A2/B2);

=

((D01: (A1/B1): (1111.1111.1100.1100))/
   (D02: (A1/B2): (1111.1111.1010.1010))/
   (D03: (A2/B1): (1111.1100.1111.1100))/
   (D04: (A2/B2): (1111.1010.1111.1010)));

=

((D09: (C01/C02): (1111.1111.1110.1110))/
   (D10: (C03/C04): (1111.1110.1111.1110)));

=

(D11: (D09/D10): (1111.1111.1111.1110));
Ccl. 1.
 (cj.db.rdc.) (x (A(x ) B(x) ) );
 

ref

 ((A1/B1)/ (A2/B2));
 

ref

(snn.) (A1/A2/ B1/B2);

=

((D05: (A1/A2): (1111.1111.1111.0000))/
   (D06: (B1/B2): (1110.1110.1110.1110)));

=

(D13: (C05/C06): (1111.1111.1111.1110)) : geldig.

Indirect bewijs, via resolutie.


Met 'nieuwe' Skolem constanten:
Levert een correcte uitkomst!
{(x A(x) ) ( y B(y) ) }
 ¬(x (A(x) B(x) ) );
 ((A(

c

s

) B(

d

s

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

c

s

) B(

d

s

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

c

s

) B(

d

s

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

c

s

) , ¬A(x), ¬B(x ) );
  : sluit.

(a3-3):
Bijv.: [1] {(y A(y)) ( z x C_(x,z))}   (ssm.,cj.db.rdc.) (y (A(y) (x C_(x,y) ) ) ) : geldig.
E-kwantor buitenplaatsing; U-kwantor buitenplaatsing.
 (snn.) [1] (prenex): {y z x (A(y) C_(x,z) ) }  ( ssm.,cj.db.rdc.) (y x (A(y ) C_(x,y) ) );
 (Skl.) {A(

c

s)) C_(x,

d

s)}
 [

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, ..)}, ..};]
[2]  C2·[

d

s

:=

c

s];  (ssm.,cj.db.rdc.) (A(

c

s) C_(x,

c

s));
 (y (A(y) (x C_(x,y) ) ) );
 (snn.) [1] (prenex): (y x (A(y) C_(x,y ) ) );
 [

ref

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

ref

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

(a3-4):
Bijv.: [1] {(y A(y) ) ( x z C_(x,z) ) }   C2·[z

:=

y];   (

degres

)(dj.rdc.;cj.xpn.) ( x y (A(y) C_(x,y) ) ) :

ongeldig

.
 (snn.) (prenex): {y x 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), ..)};]
[2]  D1·[

c

s

:=

f

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

f

s(y))/ C_(x,

g

s(x)))
 [

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), ..)};] : geldig.
[3]  D1·[y

:=

x]   (

degres

)(cj.rdc.:unif.) (A(

f

s(x))/ C_(x,

g

s(x)))
 [

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), ..)};] : geldig.
[4]  D2·[

g

s(x)

:=

f

s(x)];  (

upgrad

) (dj.rdc.) (A(

f

s(x)) C_(x,

f

s(x)) );
(x y (A(y) C_(x,y) ) );
 [

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

ongeldig

.

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

C.P. van der Velde © 2004, 2016, 2019.