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): { x
y (A( x), B( y ) ) } : geldig.
(Skl.) {A( x), B( y)}
[  ( x
y ¬(A( x), B( y)) );]
[  ( x
y (¬A( x)  ¬B( y)) );]
[  (( x ¬A( x)) 
( y ¬B( y)) );]
(Skl.) (¬A( cs) 
¬B( ds))
[  ref {(A1,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( cs) 
¬B( cs))
[  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) ) , ( y
w C_( w, y) ) }  C2·[ w:=x];
(ren.,cj.db.rdc.) ( y
x (A( x), C_( x, y))) : geldig.
(snn.) ( prenex): [1] { y
x w (A( x), C_( w, y) ) };
(Skl.) {A( x), C_( w, ds)}
[  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, ds) ) : geldig.
[  ref {(A1,C1.((1/2/ ..).d0)), (A2,C2.((1/2/ ..).d0)), ..};]
[  ref(compr.) {(A1,A2, ..), (C1.((1/2/ ..).d0), C2.((1/2/ ..).d0), ..)};]
 ( y
x (A( x), C_( x, y))).
(a1a-3):
Bijv.: [1] (( x A( x)), ( w
y C_( w, y)))  ·[ w:=x];
(ren.,cj.db.rdc.) { x
y (A( x), C_( x, y))} : geldig.
(Skl.) [1] (A( x), C_( w, gs
( 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) ( w
y x (A( x), C_( w, y)));
[2]  D2·[ x:=w];
(ren.,cj.db.rdc.) {A( x), C_( x, gs( 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): { 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:=dd];
(degres)(cj.rdc.:inst.1) (A( x), B( dd)) : geldig.
[  ref {((A1,A2, ..),(B*).d1)};]
[  ref(distr.1) {(A1,(B*).d1),(A2,(B*).d1), ..};]
[2a2]  ·[ x:=dd];
(degres)(cj.rdc.:inst.2) (A( dd), B( d
d))
[ ref {(A*).d1, (B*).d1};]
: geldig.
[2a3]  ·[ dd:= ds
]; (degres)(dj.xpn.:Sk+1) (A( d
s), B( ds)) : 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:=gd( z)];
(degres)(cj.rdc.:inst.1) (A( x), B(
gd( 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:=gd( z);
z:=x]; (degres)(cj.rdc.:inst.2)
(A( gd( x)), B( gd( x))) : geldig.
[  ref {((A*).1,(B*).1), ((A*).2,(B*).2), ..};]
[  ref {(A*).1,(A*).2, .. (B*).1,(B*).2, ..};]
[2b3]  ·[ gd( x) :=g
s( x)]; (degres)
(dj.xpn.:Sk+1) (A( gs( x))  B(
gs( x))) : geldig.
[  ref {((A1/A2/ ..).1, (B1/B2/ ..).1), ((A1/A2/ ..).2, (B1/B2/ ..).2), ..};]
[2b4]  ·[ x:=dd];
(degres)(cj.rdc.:inst.) (A( gs( d
d))  B( gs( dd
)) )
[ ref {((A1/A2/ ..).d1), ((B1/B2/ ..).d1), ..};]
: geldig.
[2b5(=2a3)]  ·[ gs( d
d) :=ds];
(syn.rdc.:Sk±1,snn.) (A( ds), B( ds
)) : 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) ) , ( 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.) (Skl.) [1] {A(
x), C_( w, ds))}
[  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, ds) ) : 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) ( y
x (A( x), C_( x, y))).
Lokale Disjunctieve expansie:
[2a2(=2b2;=2c2)]  ·[ ds:=
gs( x)]; (degres
)(dj.xpn.:Sk±1) (A( x), C_( x, gs( 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) ( x
y (A( x), C_( x, y))).
[2b] Route 2.
Met lokale 'EU-UE' kwantor volgordeverandering.
Lokale Disjunctieve expansie:
[2b1]  ·[ ds:=
gs( w)]; (degres)(dj.xpn.:Sk±1)
(A( x), C_( w, gs( w) )
[ ref {A1,A2, .. C1.((1/2/ ..).1),
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 reïteratie:
[2b2(=2a2)]  C2·[ w:=x];
(cj.db.rdc.:ren.,unif.) (A( x), C_( x, gs( 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) ( x
y (A( x), C_( x, y))).
[2c] Route 3.
Via - volgordebehoudende - prenex vorm.
U-kwantor buitenplaatsing; E-kwantor buitenplaatsing.
Lokale Disjunctieve expansie:
[2c1]  ·[ ds:=
gs( x)]; (degres)(dj.xpn.:Sk±1)
(A( x), C_( w, gs( 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), ..};]
 { 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) ) : 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) ( x
y (A( x), C_( x, y))).
[2d] Route 4.
Lokale Disjuncte expansie:
[2d1]  ·[ ds:=
gs( z)]; (degres)
(dj.xpn.) {A( x), C_( w, gs( 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) ) , (
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.) {A( x), C_( w, gs( 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) ) 
( w y C_( w, y) ) };
(snn.) ( prenex) ( w
y x (A( x), C_( w, y))).
Basale Syntactische doublure-eliminatie:
[2d3(=2a2;=2b2;=2c2)]  ·[ w:=x];
(cj.rei.;ren.) {A( x), C_( x, gs( 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) ( x
y (A( x), C_( x, y))).
[2e] Route 5.
Disjuncte expansie:
[2e1]  ·[ ds:=
gs( w, z)]; (degres
)(dj.xpn.) {A( x), C_( w, gs( 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) ) 
( w z
y (A( x), C_( w, y) ) };
(snn.) ( prenex) ( w
z y x (A( x), 
C_( w, y))).
Conjuncte reductie:
[2e2]  ·[ z:=w];
(degres)(cj.rdc.:ren.) {A( x), C_( w, gs( 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) ) , (
w y C_( w, y) ) };
(snn.) ( prenex) ( w
y x (A( x), C_( w, y))).
Lokale Syntactische reductie ( synonymie):
[2e3(=2b1;=2d2)]  C2·[ hs( w
, w) :=gs( w)];
(syn.rdc.:Sk±1,snn.) (A( x), C_( w, gs( 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) ) , (
w y C_( w, y) ) };
(snn.) ( prenex) ( w
y 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, gs( 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) ( x
y (A( x), C_( x, y))).
[2f] Route 6 (ongeldige uitkomst).
Lokale Syntactische expansie ( synonymie):
[2f1]  ·[ ds:=
gs( dd)]; (syn.rdc.:Sk±1,snn.)
{A( x), C_( w, gs( dd) )} : 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) ) , (
z y w (( z=
dd)  C_( w, y) ) ) }.
(snn.) ( prenex) ( z
y x w (A( x), (( z
=dd)  C_( w, y) ) ) ).
Lokale Conjunctieve expansie ( generalisatie):
[2f2(=2b1;=2d2;=2e3)]  ·[ dd:=w
]; (upgrad)(cj.xpn.:gnr.) {A( x),
C_( w, gs( 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) x
w 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) ( x
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) { x
y (A( x), B( y))} (degres)(cj.rdc.;dj.xpn.)
( x (A( x), B( x))) : geldig.
(Skl.) [1] {A( cs), 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:=cs
]; (degres)(cj.rdc.:inst.) (A( c
s), B( cs) : geldig.
[  ref {((A1/A2/ ..).c0), ((B1/B2/ ..).c0)};] [
 ref {(A1,B1)/ (A2,B2)/ ..};]
[2b] Route 2 (ongeldige uitkomst).
Lokale Conjuncte reductie:
[2b1]  ·[ y:=dd];
(degres)(cj.rdc.:inst.) (A( cs), B(
dd)) : geldig.
[  ref {((A1,(B*).d1)/(A2,(B*).d1)/ ..).c0};] [
 ref {(A1/A2/ ..).c0, (B*).d1};]
Lokale Disjuncte expansie:
[2b2]  ·[ dd:=d
s]; (degres)(dj.xpn.:Sk+1)
(A( cs), B( ds)) : 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] { x
y (A( x, B( y))};
(Skl.) [1] {A( x), B( ds
)}
[  ref {A1,A2, .., (B1/B2/ ..).d0)};]
[2a] Route 1.
Lokale Conjunct-Disjunct reductie:
[2a1]  ·[ x:=cs
]; (degres)(cj.-dj.rdc.:inst.) (A( c
s), B( cs)) : geldig.
[  ref {((A1/A2/ ..).c0), ((B1/B2/ ..).c0)};]
[  ref {(A1,B1)/ (A2,B2)/ ..};]
[2b] Route 2 (ongeldige uitkomst).
Lokale Conjuncte reductie:
[2b1]  ·[ x:=cd];
(degres)(cj.rdc.:inst.) (A( cd), B( d
s)) : geldig.
[  ref {(A*).c1, (B1/B2/ ..).d0};] [
ref {(((A*).c1/B1), ((A*).c1/B2), ..).d0};]
Lokale Disjuncte expansie:
[2b2]  ·[ cd:=c
s]; (degres)(cj.rdc.;dj.xpn.)
(A( cs), B( ds)) : 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]  ·[ ds:=
gs( x)]; (degres)
(dj.xpn.:Sk+1) {A( x), B( gs( x))} : geldig.
[  ref {(A1,(B1/B2/ ..).1), (A2,(B1/B2/ ..).2), ..};]
(snn.) ( prenex) { x
y (A( x), B( y))};
[2c2]  ·[ x:=cd];
(degres)(cj.rdc.:inst.) (A( cd), B( g
s( cd)))
: geldig.
[  ref {(A*).c1, (B1/B2/ ..).c1};]
Syntactische reductie ( synonymie):
[2c3]  ·[ gs( c
d) :=es]; (,syn.rdc.:Sk±1,snn.
) (A( cd), B( es)) : geldig.
[  ref {(A*).c1, (B1/B2/ ..).e0};]
[2c4]  ·[ cd:=c
s]; (degres)(dj.xpn.)
(A( cs), B( es)) : 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) { x
y (A( x), B( y) ) };
(Skl.) {A( cs), 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/..)};]
[Bijv.: {{A1,B2}, {A2,B3}};]
[2]  C2·[ ds:=c
s]; (upgrad)(dj.rdc.) (A( c
s), B( cs));
[  ( 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)) , ( z
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] { y
z x (A( y), C_( x, z)) }
 C2·[ z:=y];
(upgrad)(dj.rdc.) ( y
x (A( y), C_( x, y))) : ongeldig.
(Skl.) [1] {A( cs), 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·[ ds:=c
s]; (upgrad)(dj.rdc.) (A( c
s), C_( x, cs)) : 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) ) , ( x
z C_( x, z) ) }  C2·[ z:=y];
(degres)(dj.xpn.;dj.rdc.) (
x y (A( y), C_( x, y))) : ongeldig.
(snn.) ( prenex) [1] { y
x z (A( y), C_( x, z)) };
(Skl.) [1] {A( cs), 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 cs, in een éénplaatsige (conjuncte) predicatie is substitueerbaar
- onder parafrase - door een nieuw ingevoerde Skolem functie, zeg fs(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·[ cs:=f
s( y)]; (syn.xpn.:Sk±1,snn.) (A( f
s( y)), C_( x, gs( 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:=x]
(syn.rdc.:ren.,snn.) (A( fs( x)), C_( x, gs(
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·[ gs( x) :=f
s( x)]; (upgrad)(dj.rdc.) (A(
fs( x)), C_( x, fs( 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)};]
C.P. van der Velde © 2004, 2016, 2019.
|
|