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( cs), ¬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( cs), ¬B( c
s)) : geldig.
[ ref {(A1/B1),(A2/B2), ..};]
[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,
ds)}
[ 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,
ds) ) : geldig.
[ ref {(A1,C1.((1/2/ ..).d0))/ (A2,C2.((1/2/ ..).d0))/ ..};]
( 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·[ ds:=
gs( x)]; (degres)
(dj.xpn.) {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/(C1.((1/2/ ..).1),C2.((1/2/ ..).1), ..)),
(A2/(C1.((1/2/ ..).2),C2.((1/2/ ..).2), ..)), ..};]
( 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,
gs( 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·[ gs( x) :=
ds]; (upgrad)
(dj.rdc.) (A( x) C_( x, ds) )
[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:=dd];
(degres)(cj.rdc.:inst.) (A( x) B( d
d)) : geldig.
[ ref {(A1/(B*).d1),(A2/(B*).d1), ..};]
[ ref(compr.) {((A1,A2, ..)/(B*).d1)};]
[2a2] ·[ x:=dd];
(degres)(cj.rdc.:inst.) (A( dd)
B( dd))
[ref {(A*).d1/ (B*).d1};]
: geldig.
[2a3] ·[ dd:= ds
]; (degres)(cj.rdc.;dj.xpn.) (A(
ds) B( ds
)) : geldig.
[ ref {((A1/A2/ ..).d0)/ ((B1/B2/ ..).d0)};]
[ ref(compr.) {(A1/B1)/ (A2/B2)/ ..};]
[ ref {A1/A2/ .. B1/B2/ ..};]
Zie verder: E-kwantor splitsing, in Disjunctie, simpele vorm, [1-2] (geldig).
[2b] Route 2
[2b1] ·[ y:=gd( z)];
(degres)(cj.rdc.:inst.) (A( x)
B( gd( z))) : geldig.
[ ref {(A1/(B*).1), (A1/(B*).2), .., (A2/(B*).1), (A2/(B*).2), ..};]
[ ref(compr.) {(A1,A2, ..)/ ((B*).1,(B*).2, ..)};]
[2b2] ·[ x:=gd( z);
z:=x]; (degres)(cj.rdc.:inst.)
(A( gd( x)) B( gd( x
))) : geldig.
[ 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, ..};]
[2b3] ·[ gd( x) :=g
s( x)]; (degres)
(dj.xpn.) (A( gs( x)) B( g
s( x)))
[ref {((A1/A2/ ..).1/ (B1/B2/ ..).1),
((A1/A2/ ..).2/ (B1/B2/ ..).2), ..};] : geldig.
[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)/ ..};]
[ ref {A1/A2/ .. B1/B2/ ..};]
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,
ds))}
[ 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,
ds) )
[ref {(A1/C1.((1/2/ ..).d0)),
(A2/C2.((1/2/ ..).d0)), ..};] : geldig.
( prenex): ( y
x (A( x) C_( x, y)));
Lokale Disjunctieve expansie:
[2a2] ·[ ds:=
gs( x)]; (degres)(dj.xpn.:Sk+1)
(A( x) C_( x, gs( 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] ·[ ds:=
gs( w)]; (degres)(dj.xpn.:Sk+1)
(A( x) C_( w, gs( w) )
: geldig.
[ 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)), ..) ..};]
{( 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
, gs( 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] ·[ ds:=
gs( x)]; (degres)(dj.xpn.:Sk+1)
(A( x) C_( w, gs( 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
, gs( 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] ·[ ds:=
gs( z)]; (degres)
(dj.xpn.) {A( x) C_( w, gs( z) )}
: geldig.
[ 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)), ..};]
{( 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
, gs( w))} : geldig.
[ 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)), ..) ..};]
{( 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
, gs( 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] ·[ ds:=
hs( w, z)]; (degres
)(dj.xpn.) {A( x) C_( w, gs( w
, z) )} : geldig.
[ 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)), ..};]
{( 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
, hs( w, w))} : geldig.
[ 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)), ..) ..};]
{( 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·[ hs( w
, w) :=gs( w)];
(syn.rdc.:Sk±1,snn.) (A( x) C_( w, g
s( w) ) : geldig.
[ 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)), ..) ..};]
{( 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, gs( 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] ·[ ds:=
gs( dd)]; (syn.rdc.:Sk±1,snn.)
{A( x) C_( w, gs( dd
) )} : geldig.
[ 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)), ..) ..};]
{( 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,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)), ..) ..};]
( 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, gs( 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( cs)
B( y)}
[ref {((A1/A2/ ..).c0/ (B1,B2, ..)) ..};]
[2a] Route 1.
[2a1] Lokale Conjunct-Disjunct reductie:
·[ y:=cs];
(degres)(cj.rdc.:inst.) (A( c
s) B( cs)) : geldig
.
[ ref {((A1/A2/ ..).c0)/ ((B1/B2/ ..).c0)};]
[ ref {(A1/A2/ ..)/ (B1/B2/..)};
[ ref {A1/A2/ .. B1/B2/..};]
[2b] Route 2 (ongeldige uitkomst).
[2b1] Lokale Conjuncte reductie:
·[ y:=dd];
(degres)(cj.rdc.:inst.) (A( cs)
B( dd) : geldig.
[ ref {((A1/A2/ ..)/ (B*).d1)};]
[ ref {(A1/(B*).d1)/ (A2/(B*).d1)/ ..};]
Lokale Disjuncte expansie:
[2b2] ·[ dd:=d
s]; (degres)(dj.xpn.:Sk+1)
(A( cs) B( ds
))
[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:=cs
]; (degres)(cj.-dj.rdc.:inst.) (A( c
s) B( cs) ) : geldig
.
[ ref {((A1/A2/ ..).c0)/ ((B1/B2/ ..).c0)};]
[ ref {(A1/A2/ ..)/ (B1/B2/..)};
[ ref {A1/A2/ .. B1/B2/..};]
[2b] Route 2 (ongeldige uitkomst).
Lokale Conjuncte reductie:
[2b1] ·[ x:=cd];
(degres)(cj.rdc.:inst.) (A( cd)
B( ds)) : 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( 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 Disjunctie, simpele vorm, [1-2] (geldig).
[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))}
[ref {(A1/(B1/B2/ ..).1), (A2/(B1/B2/ ..).2), ..};]
: geldig.
(snn.) ( prenex): { x
y (A( x) B( y))}
[2c2] ·[ x:=cd];
(degres)(cj.rdc.:inst.) (A( cd)
B( gs( cd)))
[ref {(A*).c1/ (B1/B2/ ..).c1};]
: geldig.
Syntactische reductie ( synonymie):
[2c3] ·[ gs( c
d) :=es]; (syn.rdc.:Sk±1,snn.)
(A( cd) B( es
))
[ref {(A*).c1/ (B1/B2/ ..).e0};]
: geldig.
[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 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( cs)
B( ds)}
[ ( 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·[ ds:=c
s]; (ssm.,cj.db.rdc.) (A( cs
) B( cs))
( x (A( x)
B( x) ) ) : geldig.
[ ( 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}};]
Aanvullende bewijsvoering.
Direct bewijs, via minimaal domein.
Bijv.: ( dPDL=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.: ( dPDL=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.: ( dPDL=2):
( dPPL=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( cs)
B( ds) ) , ( x ¬(A( x)
B( x) ) ) );
((A( cs)
B( ds) ) , ( x (¬A( x), ¬B( x
) ) );
((A( cs)
B( ds) ) , ¬A( x), ¬B( x) );
(A( cs) , ¬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( cs))
C_( x, ds)}
[ 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·[ ds:=c
s]; (ssm.,cj.db.rdc.) (A( cs)
C_( x, cs));
( y (A( y)
( x C_( x, y) ) ) );
(snn.) [1] ( prenex): ( y
x (A( y) C_( x, y) ) ) : geldig
.
[ ref {(A1/A2/ ..).c0/ (C1.((1/2/ ..).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.rdc.;cj.xpn.)
( x y (A( y)
C_( x, y) ) ) : ongeldig.
(snn.) ( prenex): { y
x z (A( y) C_( x, z) ) };
(Skl.) [1] {A( cs)
C_( x, gs( 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·[ 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), ..)};]
[3] D1·[ y:=x]
(degres)(cj.rdc.:unif.) (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] D2·[ gs( x) :=f
s( x)]; (upgrad)(dj.rdc.) (A(
fs( x)) C_( x, fs( x
)) );
( x y (A(
y) C_( x, y) ) ) : 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), ..)};]
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.
|
|