Introductie_Predikatenlogica_PDL_Deel_V_H

Cursus / training:

Methode Formele Logica

^©

V. Deductieregels: Regels voor transformatie onder degressie.

Deductie via Semantische verandering.

• met (semantisch) verlies van logische kracht.

Levert Semantische derivaten.

12. **Semantische argument-reductie, geldig - vanuit term.**

12.1. **Regels voor Argument-reductie; via Kwantor reductie, Substitutie, en/of Subsumptie .**

Hoofdvormen.

(a) Kwantor-bewerkingen, met degressie; via Kwantor reductie (QR).
(b) Substitutie, met degressie; via Instantiatie.
(c) Argument-derivatie, met degressie; via Subsumptie.

Principes per Hoofdvorm.

12.1.1. **Kwantor-bewerkingen; met degressie: via Kwantor reductie (QR).**

M.n. U-kwantor reductie, kwantor down-grading.
Universeel - naar Existentieel gekwantificeerde expressie.
Is een vorm van conjuncte reductie, resp. disjuncte expansie.

12.1.2 **Substitutie, met degressie; via Instantiatie.**

Arbitraire, c.q. 'ad hoc' interpretatie van variabele: domeininterpretatie.
Verlaging van de generaliteit, d.i. kwantiteit van een term.
Oftewel verhoging van specificiteit, c.q. syntactische termdiepte.
Daarmee beperking van referentieel bereik, dus van referentiegebied.
Is dus een vorm van conjuncte reductie. Dus geldig met verlaging van logische kracht: degressie.
Levert een instantie van de oorspronkelijke term.
Een expressie waarvan de argumentenlijst(en) géén variabele meer bevat, èn géén Skolem functie c.q. constante bevat, geldt als grondinstantie.

'·[v₁

:=

t

₂] : instantiatie-operatie.

Vervanging in de voorgaande expressie van elk voorkomen van v₁ door

t

₂.
D.w.z. v₁ subsumeert

t

₂.
(subsumptie: semantische onderschikking).

(

R

^*(

t

₂)

R

^*(v₁).

Notaties.

_(i)' : Implicatie onder argument-instantiatie.

Algemene basisregels t.b.v. instantiatie.

(1)

Regels t.b.v. substitutie via instantiatie.

(1a) Regel t.b.v. substitutie van predicaties/ literalen, via instantiatie.

{

j ((

R

^*(

t

_[j])

R

^*(

t

_[i]))

(

k (F_[h]·[

t

_[k]

:=

t

_[i]]

_(degres
)_(i) F _[h]·[

t

_[k]

:=

t

_[j] ] )_k,_h) )_j,_i}.

(1b) Regel t.b.v. substitutie van termen/ predicaat-argumenten, via instantiatie.

{

j ((

R

^*(

t

_[j])

R

^*(

t

_[i]))

(

k (

R

^*(

t

_[h]·[

t

_[k]

:=

t

_[j]])

R

^* (

t

_[h]·[

t

_[k]

:=

t

_[i]]_ )_k,_h) )_j,_i}.

Bijv.: {A₁(v₁)

C₁(v₁))}

·[v₁

:=

c

₂];

_(v) (A₁(

c

₂)

C₁(

c

₂)) : is geldig.

12.1.3. **Argument-derivatie, met degressie ; via Subsumptie.**

Instantiatie; bijzondere geldige vorm.
Legitiem, maar voorwaardelijk.
Afleidbaar wegens Subsumptie: semantische onderschikking van referentiegebied c.q. domein-selectie) van afgeleide, 'zwakkere' argument.
Verlaging van de zekerheid van een term.
Bijv. afleidbaar via Disjunctieve expansie, via Inverse Skolemisatie, wegens subsumptie.
Dus geldig met verlaging van logische kracht: degressie.
Levert een derivaat van de oorspronkelijke expressie.
Is meer algemeen dan enkel instantiatie.

Bijv.: {A₁(v₁}

·[v ₁

:=

t

₂_s];

_(s) A₁(

t

₂_s) : is geldig.

D.w.z. v₁ subsumeert

t

₂_s.

12.2. **Vormen van Argument-reductie / Instantiatie; via Kwantor reductie, Substitutie, of Subsumptie.**

Instantiatie met Skolem functies.

Instantiatie met nul-plaatsige Skolem functies, cq. constanten.

Verschillende Skolem constanten, bijv. {

c

_s,

d

_s}, hebben in principe geen identieke referentiegebieden.
Dit geldt zeker wanneer ze in de argumentlijsten van predikaties met verschillende predikaatnamen voorkomen.
Bijv.:

{A(

c

_s), B(

d

_s)}

(

c

=

_(r)

d

_s ) :

ongeldig

Oftewel:

({A(

c

_s), B(

d

_s)}

(

c

=

_(r)

d

_s) ).

Ze kunnen echter in sommige gevallen wel tot elkaar herleid worden.
Dit is het geval wanneer ze in de argumentlijsten van predikaties met dezelfde predikaatnamen voorkomen.
Bijv., gegeven: {A(

c

_s), A(

d

_s)};
geldt:

{(A(

c

_s)

_(Sk+1) {A(

c

_s), A(

d

_s)})

({A(

c

_s), A(

d

_s)}

_(degres
)_(cj.rdc.) A(

c

_s))};

derhalve:

{A(

c

_s)

_(Sk+1) {A(

c

_s), A(

d

_s)}};

en dus:

(

c

=

_(r)

d

_s).

Een Skolem constante, bijv.

c

_s, kan in principe onbeperkt transitief 'overerven'.
Bijv. via Modus Ponens:

{A(

c

_s), B(

d

_s), (

x (A(x)

B(x) )}

(A(

c

_s), B(

c

_s), B(

d

_s));

En daaruit volgt:

(

c

=

_(r)

d

_s).

nul-plaatsige Skolem functie, cq. constante.

12.2.1. Argument-reductie/ Instantiatie; Binnen één Literaal.

(a1)

Argument-reductie/ Instantiatie; vanuit variabele, enkelvoudig, naar 'Skolem' constante .

In Literaal, met éénplaatsig predicaat.

Via operatie: conjunct-disjunct conversie (conjuncte reductie, resp. disjuncte expansie).

Bijv.: [1] {

x A(x)}

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

x A(x)) : geldig.
C.q. (Sk.): {A(x_u)} [

_ref {x1,x2, ..};]

(D.w.z. van toepassing op elke x).

[1a1]

·[x

:=

c

_d];

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

c

_d) [

_ref {c1};] : geldig.

(

_[=1
]x (A( x)

=

c

_d ) ) );

(D.w.z. een bestaande, vaststaande selectie

c

_d uit x).

[1a2]

·[

c

_d:=

c

_s];

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

c

_s) [

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

(D.w.z. een nieuwe, onbepaalde keuze

c

_d uit x).

En/of (alternatieve afleiding):

[1b1]

·[x

:=

f

_d(x)];

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

f

_d(x)) [

_ref {(y*).x1,(y*).x2, ..};] : geldig.

(

_[=n[x]
]y_x A(y_x)

(y_x

=

f

_d(x) ) ) );

(D.w.z. Steeds een bestaande, vaststaande selectie

f

_d uit y, voor elk onderscheiden element x).

[1b1a1]

·[x

:=

c

_d];

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

f

_d(

c

_d) [

_ref {(y*).c1};] : geldig.

(

_[=n[c1]
]y_x A(y_x)

(y_x

=

f

_d(

c

_d) ) ) );

(D.w.z. een bestaande, vaststaande selectie

f

_d uit y, voor een bestaande, vaststaande selectie

c

_d uit x).

[1b1a2]

·[

c

_d:=

c

_s];

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

f

_d(

c

_s) ) [

_ref {((y*).x1/ (y*).x2/ ..).c0};] : geldig.

(D.w.z. Steeds een bestaande, vaststaande selectie

f

_d uit y, per element uit een nieuwe, onbepaalde keuze uit x).

Het verwijzingsgebied van

c

_s is hier -per definitie- onbepaald. Daardoor zijn ook de refenties van

f

_d hier niet kenbaar.
Daarom geldt hier synonymie:

[1b1a2(=1a2)] Syntactische reductie (synonymie):

·[

f

_d(

c

_s )

:=

d

_s];

_(Sk+1;snn.) A(

d

_s); [

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

(D.w.z. een nieuwe, onbepaalde keuze

d

_s uit x).

En/of:

[1b1b1]

·[

f

_d(x)

=

f

_s(x)];

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

f

_s(x) ) [

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

(D.w.z. Steeds één nieuwe, onbepaalde keuze

f

_s uit y, voor elk onderscheiden element x).

Het verwijzingsgebied van elke

f

_s instantie is hier -per definitie- onbepaald. Daarom geldt hier synonymie:

[1b1b1(=1a2)] Syntactische reductie (synonymie):

·[

f

_s(x)

:=

d

_s];

_(degres
) _{(cj.rdc.:Sk+1,ssm.)} A(

d

_s); [

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

(D.w.z. een nieuwe, onbepaalde keuze

c

_s uit x).

En/of: [1b1b2a1]

·[x

:=

c

_d];

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

f

_s(

c

_d) ) [

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

(D.w.z. een nieuwe, onbepaalde keuze

f

_s uit x, voor een bestaande, vaststaande selectie

c

_d uit x).

Het verwijzingsgebied van elke

f

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

c

_d. Daarom geldt hier synonymie:

[1b1b2a1(=1a2)] Syntactische reductie (synonymie):

·[

f

_s(

c

_d )

:=

d

_s];

_(Sk+1,snn.) A(

d

_s); [

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

(D.w.z. een nieuwe, onbepaalde keuze

c

_s uit x).

[1b1b2a2]

·[

c

:=

c

_s];

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

f

_s(

c

_s) )
[

_ref {((y1/y1/..).x1/ (y1/y2/..).x2/ ..).c0};]
: geldig.

(D.w.z. Steeds één nieuwe, onbepaalde keuze

f

_s uit y, per element uit een nieuwe, onbepaalde keuze

c

_s uit x).

Het verwijzingsgebied van elke

f

_s instantie is hier -per definitie- onbepaald. Dus dat geldt zeker ook voor een instantie met een onbepaalde selectie

c

_s. Daarom geldt synonymie:

[1b1b2a2(=1a2)] Syntactische reductie (synonymie):

·[

f

_s(

c

_s)

:=

d

_s];

_(Sk+1,snn.) A(

d

_s); [

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

(D.w.z. een nieuwe, onbepaalde keuze

c

_s uit x).

Idem, In Literaal, met meerplaatsig predicaat.

Zonder Argument-differentiatie/ Kwantor-splitsing.

Bijv.: [2] {

y A(x,y)}

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

x A(x,y)) : geldig.
C.q. (Sk.): {A(x_u,y_u)}

[

_ref {(x1,y1)(x1,y2), ..,(x2,y1), (x2,y2), ..};]
[

_ref {(x1,(y1,y2, ..)), (x2,(y1,y2, ..)), ..};]

(D.w.z. geldig voor elke combinatie van x en y).

[2a1]

·[y

:=

d

_d];

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

d

_d) : geldig.

[

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

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

[2a1]

(

_[=1
]y

x (A(x,y)

=

d

_d ) ) );

(D.w.z. Eén bestaande, vaststaande selectie

d

_d uit y, geldig bij elke x).

[2a2]

·[

d

:=

d

_s];

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

d

_s) : geldig.

[

_ref {(x1,(y1/y2/ ..).d0), (x2,(y1/y2/ ..).d0), ..};]
[

_ref {((x1,x2, ..), (y1/y2/ ..).d0)};]

_(Sk-1) (

x A(x,y) );

(D.w.z. Eén nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

Vervolg afleiding, geldig:

[2a3]

·[

d

:=

g

_s(

e

_d)];

_(Sk+1) A(x,

g

_s(

e

_d) ) : geldig.

[

_ref {(x1,(y1/y2/ ..).e1), (x2,(y1/y2/ ..]).e1), ..};]
[

_ref {((x1,x2,..), (y1/y2/ ..).e1)};]

(D.w.z. een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

e

_d uit x, geldig bij elke x).

En/of (alternatieve afleiding):

[2b1]

·[y

:=

g

_d(x)];

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

g

_d(x)) [

_ref {(x1,(y*).x1), (x2,(y*).x2), ..};] : geldig.

[2b1]

(

_[=n[x]
]y_x (A(x,y_x)

(y_x

=

g

_d(x) ) ) );

(D.w.z. Steeds een bestaande, vaststaande selectie

g

_d uit y, voor elk onderscheiden element x, geldig bij elke x).

Afleidbaar wegens subsumptie:

[2b2a1]

·[

g

_d(x)

:=

g

_d(

d

_d)];

_{(degres
)}_{(cj.rdc.:ssm.)} A(x,

g

_d(

d

_d)) : geldig.

[

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

_ref {((x1,x2, ..), (y*).d1)};]

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een bestaande, vaststaande selectie

d

_d uit x, geldig bij elke x).

[2b2a2]

·[

d

:=

d

_s];

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

g

_d(

d

_s)) : geldig.

[

_ref {(x1,(z*).(y1/y2/ ..).d0), (x2,(z*).(y1/y2/ ..).d0), ..};]
[

_ref {((x1,x2, ..), (z*).(y1/y2/ ..).d0)};]

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een nieuwe, onbepaalde keuze

d

_s uit x, geldig bij elke x).

Vervolgafleiding,

ongeldig

.
[2b2b1(=2a2)]

·[

g

_d(x)

:=

d

_s];

_(upgrad
)_{(cj.xpn.:Sk+1)} A(x,

d

_s) :

ongeldig

[

_ref {(x1,(y1/y2/ ..).d0), (x1,(y1/y2/ ..).d0), ..};]
[

_ref {((y1,y2, ..), (x1/x2/ ..).d0)};]

_(Sk-1) (

x A(x,y) );

(D.w.z. Eén nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

(a2)

Argument-reductie/ Instantiatie; vanuit variabele, /vanuit 'Skolem' constante enkelvoudig, naar 'Skolem' functie.

Vanuit [2a2]:
[2b3] Kwantor volgorde verandering;
Disjunctieve expansie:

·[

d

:=

g

_s(x)];

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

g

_s(x))
[

_ref {(x1,(y1/y2/ ..).1), (x2,(y1/y2/ ..).2), ..};] : geldig.
[2b3]

_(Sk-1) (

_[=n[x]
]y_x A(x,y_x) );

(D.w.z. Steeds een nieuwe, onbepaalde keuze

g

_s uit y, voor elk onderscheiden element x, geldig bij elke x).

(a3)

Argument-reductie/ Instantiatie; vanuit variabele, meervoudig, naar 'Skolem' constanten .

Vanuit [2b3]:

[2b4] Bijv.: {

y A(x,y)}

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

y A(x,y)) : geldig.
C.q. (Sk.): {A(x,

g

_s(x))} [

_ref {(x1,(y1/y2/ ..).1), (x2,(y1/y2/ ..).2), ..};]

(D.w.z. Steeds een nieuwe, onbepaalde keuze

g

_s uit y, voor elk onderscheiden element x, geldig bij elke x).

[2b5a1]

·[x

:=

c

_d];

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

c

_d,

g

_s(

c

_d) ) [

_ref {(c1,(y1/y2/ ..).c1)};] : geldig.

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij die

c

_d).

[2b5a1]

·[

g

_s(

c

_d)

:=

d

_s];

_{(Sk+1
)} A(

c

_d,

d

_s)

[

_ref {(c1,y1)/ (c1,y2)/ ..))};]
[

_ref {(c1,(y1/y2/ ..).d0)};]

: geldig.

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een bestaande, vaststaande selectie

c

_d uit x).

[2b5a2]

·[

c

:=

c

_s];

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

c

_s,

d

_s) : geldig.

[

_ref {(x1,y1)/ (x1,y2)/ ..(x2,y1)/ (x2,y2)/ ..};]
[

_ref {((x1,(y1/y2/ ..).d0)/ (x2,(y1/y2/ ..).d0)/ ..).c0};]

[2b5a2]

_(Sk-1) (

y A(x,y) );

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

Alternatieve afleiding, geldig:

[2b5b1]

·[

d

:=

d

_s];

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

g

_s(

d

_s) ) : geldig.

[

_ref {(x1,(z1/z2/ ..).(y1/y2/ ..).d0), (x2,(z1/z2/ ..).(y1/y2/ ..).d0), ..};]
[

_ref {((x1,x2, ..), (z1/z2/ ..).(y1/y2/ ..).d0)};]

(D.w.z. een nieuwe, onbepaalde selectie

g

_s uit z, per element uit een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x).

Vervolgafleiding,

ongeldig

[2b5b2]

·[

g

_s(

d

_s)

:=

e

_s];

_(degres
)_{(cj.rdc.:Sk+1,ssm.)} A(x,

e

_s ) :

ongeldig

[

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

_ref {(x1,x2,..), (y1/y2/ ..).c0};]

(D.w.z. een nieuwe, onbepaalde keuze

e

_s uit y, geldig bij elke x ).

Alternatieve afleiding,

ongeldig

[2b5c1]

·[

g

_s(x)

:=

g

_s(

c

_d)];

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

g

_s(

c

_d) ) ) :

ongeldig

[

_ref {(x1,(y1/y2/ ..).c1), (x2,(y1/y2/ ..).c1), ..};]
[

_ref {(x1,x2,..), (y1/y2/ ..).c1)};]

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij elke x).

[2b5c1]

·[

g

_s(

c

_d)

:=

d

_s];

_{(Sk+1
)} A(x,

d

_s) : geldig.

[

_ref {(x1,(y1/y2/ ..).d0), (x2,(y1/y2/ ..).d0), ..};]
[

_ref {(x1,x2, ..), (y1/y2/ ..).d0)};]

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

[2b5c2(=2b5a2)]

·[

c

:=

c

_s];

_(Sk+1) A(

c

_s,

d

_s) : geldig.

[

_ref {(x1,y1)/ (x1,y2)/ ..(x2,y1)/ (x2,y2)/ ..};]
[

_ref {(x1,(y1/y2/ ..).d0)/ (x2,(y1/y2/ ..).d0)/ ..};]

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

12.2.2. Argument-reductie/ Instantiatie ; In Conjunctie.

(a1)

Argument-reductie/ Instantiatie; vanuit variabele, enkelvoudig, naar 'Skolem' constante .

In Conjunctie, met één kwantor.

Bijv.: {

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

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

y (A(y), B(y) ) ) : geldig.
C.q. (Sk.): {A(x), B(x) } [

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

·[x

:=

c

_d];

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

c

_d), B(

c

_d) ) [

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

·[

c

_d:=

c

_s ]; (A(

c

_s), B(

c

_s) ) [

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

In Conjunctie, met meerdere kwantoren.

Bijv.: [2] {

x (A(x),

y B(y ) ) }

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

y (

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

_(snn.) (prenex): {

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

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

x (A(x), B(y) ) ) : geldig.
C.q. (Sk.): {A(x_u), B(y_u) }

[

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

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

(D.w.z. geldig voor elke combinatie van x en y).

[2a1]

·[y

:=

d

_d];

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

d

_d) ) : geldig.

[

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

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

[2a1]

(

_[=1
]y

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

=

d

_d ) ) );

(D.w.z. Eén bestaande, vaststaande selectie

d

_d uit y, bij elke x).

[2a2]

·[

d

_d:=

d

_s];

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

d

_s) ) : geldig.

[

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

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

_(Sk-1) (

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

(D.w.z. Eén nieuwe, onbepaalde keuze

d

_s uit y, bij elke x).

Vervolg afleiding, geldig:

[2a3]

·[

d

:=

g

_s(

e

_d)];

_(Sk+1) (A(x), B(

g

_s(

e

_d) ) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

e

_d uit x, geldig bij elke x).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

e

_d. Daarom geldt hier synonymie:

En/of (alternatieve afleiding):

[2b1]

·[y

:=

g

_d(x)];

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

g

_d(x) ) );
[

_ref {(A1,(B*).A1), (A2,(B*).A2), ..};] : geldig.

[2b1]

(

_[=n[x]
]y_x (A(x), B(y_x) , (y_x

=

g

_d(x) ) ) );

(D.w.z. Steeds een bestaande, vaststaande selectie

g

_d uit y, voor elk onderscheiden element x, geldig bij elke x).

Afleidbaar wegens subsumptie:

[2b2a1]

·[

g

_d(x)

:=

g

_d(

d

_d)];

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

g

_d(

d

_d) ) ) : geldig .

[

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

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

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een bestaande, vaststaande selectie

d

_d uit x, geldig bij elke x).

[2b2a2]

·[

d

:=

d

_s];

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

g

_d(

d

_s) ) ) : geldig.

[

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

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

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een nieuwe, onbepaalde keuze

d

_s uit x, geldig bij elke x).

Het verwijzingsgebied van

d

_s is hier -per definitie- onbepaald. Daardoor zijn ook de refenties van

g

_d hier niet kenbaar.
Daarom geldt hier synonymie:

[2b2a2(=2a2)] Syntactische reductie (synonymie):

·[

g

_d(

d

_s )

:=

e

_s];

_(Sk+1;snn.) (A(x), B(

e

_s) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

e

_s uit y, geldig bij elke x ).

(a2)

Argument-reductie/ Instantiatie; vanuit variabele, enkelvoudig, naar 'Skolem' functie .

Vanuit [2a2]:

[2b3] Disjunctieve expansie:

·[

d

:=

g

_s(x)];

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

g

_s(x) ) )
[

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

_(Sk-1) (

_[=n[x]
]y_x (A(x), B(y_x) ) );

(D.w.z. Steeds een nieuwe, onbepaalde keuze uit x, voor elk onderscheiden element y).

[2b3]

(

y (A(x), B(y) ) );
[2b3]

(A(x), B(

g

_s(z) ) );

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Daarom geldt hier synonymie:

[2b3(=2a2)] Syntactische reductie (synonymie):

·[

g

_s(z)

:=

e

_s];

_(Sk+1;snn.) (A(x ), B(

e

_s) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

e

_s uit x).

(a3)

Argument-reductie/ Instantiatie; vanuit variabele, meervoudig, naar 'Skolem' constanten .

Vanuit [2b3]:

[2b4] Bijv.: {

x (A(x), (

y B(y )))}

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

x (A(x), (

y B(y)))) : geldig.
E-kwantor buitenplaatsing.

_(snn.) (prenex): {

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

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

y (A(x), B(y) ) ) : geldig.
C.q. (Sk.): {A(x), B(

g

_s(x) ) } [

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

(D.w.z. Steeds een nieuwe, onbepaalde keuze

g

_s uit y, voor elk onderscheiden element x, geldig bij elke x).

[2b5a1]

·[x

:=

c

_d];

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

c

_d), B(

g

_s(

c

_d) ) ) [

_ref {c1, (B1/B2/ ..).c1};] : geldig.

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij die

c

_d).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

c

_d. Daarom geldt hier synonymie:

[2b5a1] Syntactische reductie (synonymie):

·[

g

_s(

c

_d )

:=

d

_s];

_(Sk+1;snn.) (A(

c

_d), B(

d

_s) );

[

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

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

: geldig.

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een bestaande, vaststaande selectie

c

_d uit x).

[2b5a2]

·[

c

:=

c

_s];

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

c

_s), B(

d

_s) ) : geldig.

[

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

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

[2b5a2]

_(Sk-1) (

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

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

De B term (Literaal) is hier wegens Conjunctie onafhankelijk interpreteerbaar.

Alternatieve afleiding, geldig:

[2b5b1]

C2·[x

:=

c

_d];

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

g

_s(

c

_d) ) ) : geldig.

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij elke x).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

c

_d. Daarom geldt hier synonymie:

[2b5b1] Syntactische reductie (synonymie):

·[

g

_s(

c

_d )

:=

d

_s];

_(Sk+1;snn.) (A(x), B(

d

_s) ) : geldig.

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

Alternatieve afleiding, geldig:

[2b5b2]

·[

c

:=

c

_s];

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

g

_s(

c

_s) ) ) : geldig .

[

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

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

(D.w.z. een nieuwe, onbepaalde selectie

g

_s uit z, per element uit een nieuwe, onbepaalde keuze

c

_s uit y, geldig bij elke x.

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt zeker ook voor een instantie met een onbepaalde selectie

c

_s. Daarom geldt hier synonymie:

[2b5b2] Syntactische reductie (synonymie):

·[

g

_s(

c

_s)

:=

d

_s];

_(Sk+1;snn.) (A(x), B(

d

_s) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

[2b5b3(=2b5a2)]

·[x

:=

c

_s];

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

c

_s), B(

d

_s) ) : geldig.

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

Idem dito, met meerplaatsige predikaten.

Bijv.: {

x (A(x), (

y C_(x, y)))}

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

x (A(x), (

y C_(x,y)))) : geldig.
E-kwantor buitenplaatsing.

_(snn.) (prenex): {

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

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

y (A( x), C_(x,y)))) : geldig.
C.q. (Sk.): {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), ..};]

·[x

:=

c

_d];

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

c

_d), C_(

c

_d,

g

_s(

c

_d))) [

_ref {A.c1, C.c1.((1/2/..).c1)};] : geldig.

·[

g

_s(

c

_d )

:=

d

_s];

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

c

_d), C_(

c

_d,

d

_s)) [

_ref {A.c1, C.c1.((1/2/..).d0)};] : geldig.

·[

c

:=

c

_s];

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

c

_s), C_(

c

_s,

d

_s)) [

_ref {(A1/A2/ ..).c0, C((1/2/..).c0).((1/2/..).d0)};] : geldig.

Bijv.: {

y (A(y),

z C_(x,z))}

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

y (A(y),

z C_(x,z))) : geldig.
U-kwantor buitenplaatsing; E-kwantor buitenplaatsing.

_(snn.) (prenex): {

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

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

z (A(y), C_(x,z))) : geldig.
C.q. (Sk.): {A(

d

_s), C_(x,

h

_s(x))}
[

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

·[x

:=

c

_d];

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

d

_s), C_(

c

_d,

h

_s(

c

_d) ) )
[

_ref {(A1/A2/..).d0, C.c1.((1/2/..).c1)};] : geldig.

·[

h

_s(

c

_d )

:=

e

_s];

_(Sk+1) (A(

d

_s), C_(

c

_d,

e

_s) )
[

_ref {(A1/A2/..).d0, C.c1.((1/2/..).d0)};] : geldig.

·[

c

:=

c

_s];

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

d

_s), C_(

c

_s,

e

_s) )
[

_ref {(A1/A2/ ..).d0, C((1/2/..).c0).((1/2/..).e0)};] : geldig.

12.2.3. Argument-reductie/ Instantiatie ; In Disjunctie.

(a1)

Argument-reductie/ Instantiatie; vanuit variabele, enkelvoudig, naar 'Skolem' constante .

In Conjunctie, met één kwantor.

Bijv.: {

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

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

y (A(y)

B(y) ) ) : geldig.
C.q. (Sk.): {A(x)

B(x) } [

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

·[x

:=

c

_d];

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

c

_d)

c

_d) ) [

_ref {(A.c1/B.c1)};] : geldig.

·[

c

_d:=

c

_s ]; (A(

c

_s)

c

_s) ) : geldig.

[

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

_ref {A1/A2/ ..B1/B2/ ..};]

In Conjunctie, met meerdere kwantoren.

Bijv.: [2] {

x (A(x)

y B(y) ) }

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

y (

x A(x)

B(y) ) ) : geldig.
U-kwantor buitenplaatsing.

_(snn.) (prenex): {

y (A(x)

B(y) ) }

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

x (A(x)

B(y) ) ) : geldig.
C.q. (Sk.): {A(x_u)

B(y_u) } [

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

(D.w.z. geldig voor elke combinatie van x en y).

[2a1]

·[y

:=

d

_d];

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

d

_d) ) : geldig.

[

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

_ref {A1/A2/ ../B.d1};]

[2a1]

(

_[=1
]y

x ((A(x)

B(y) )

=

d

_d ) ) );

(D.w.z. Eén bestaande, vaststaande selectie

d

_d uit y, bij elke x).

[2a2]

·[

d

_d:=

d

_s];

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

d

_s) ) : geldig.

[

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

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

_(Sk-1) (

x (A(x)

B(y) ) );

(D.w.z. Eén nieuwe, onbepaalde keuze

d

_s uit y, bij elke x).

Vervolg afleiding, geldig:

[2a3]

·[

d

:=

g

_s(

e

_d)];

_(Sk+1) (A(x)

g

_s(

e

_d) ) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

e

_d uit x, geldig bij elke x).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

e

_d. Daarom geldt hier synonymie:

En/of (alternatieve afleiding):

[2b1]

·[y

:=

g

_d(x)];

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

g

_d(x) ) );
[

_ref {(A1/(B*).A1), (A2/(B*).A2), ..};] : geldig.

[2b1]

(

_[=n[x]
]y_x ((A(x)

B(y_x) )

(y_x

=

g

_d(x) ) ) );

(D.w.z. Steeds een bestaande, vaststaande selectie

g

_d uit y, voor elk onderscheiden element x, geldig bij elke x).

En/of (alternatieve afleiding):

[2b1b]

·[y

:=

g

_d(z); z

:=

y)];

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

g

_d(y) ) );
[

_ref {(A1/(B*).A1), (A1/(B*).A2), .. (A2/(B*).A1), (A2/(B*).A2), ..};] : geldig.

[*Niet geldig in dj: onevenwichtige instantatie:]
Afleidbaar wegens subsumptie:

[2b2a1]

·[

g

_d(x)

:=

g

_d(

d

_d)];

_{(degres
)}_{(cj.rdc.:ssm.)} (A(x)

g

_d(

d

_d) ) ) : geldig.

[

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

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

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een bestaande, vaststaande selectie

d

_d uit x, geldig bij elke x).

[2b2a2]

·[

d

:=

d

_s];

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

g

_d(

d

_s ) ) ) : geldig.

[

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

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

(D.w.z. Een bestaande, vaststaande selectie

g

_d uit y, voor een nieuwe, onbepaalde keuze

d

_s uit x, geldig bij elke x).

Het verwijzingsgebied van

d

_s is hier -per definitie- onbepaald. Daardoor zijn ook de refenties van

g

_d hier niet kenbaar.
Daarom geldt hier synonymie).

[2b2a2(=2a2)] Syntactische reductie (synonymie):

·[

g

_d(

d

_s )

:=

e

_s];

_(Sk+1;snn.) (A(x)

e

_s) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

e

_s uit y, geldig bij elke x ).

(a2)

Argument-reductie/ Instantiatie; vanuit variabele, enkelvoudig, naar 'Skolem' functie .

Vanuit [2a2]:

[2b3] Disjunctieve expansie:

·[

d

:=

g

_s(x)];

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

g

_s(x ) ) )
[

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

_(Sk-1) (

_[=n[x]
]y_x (A(x)

B(y_x) ) );

(D.w.z. Steeds een nieuwe, onbepaalde keuze uit x, voor elk onderscheiden element y).

[2b3]

(

y (A(x)

B(y) ) );
[2b3]

(A(x)

g

_s(z) ) );

De B term (Literaal) is hier wegens Disjunctie niet onafhankelijk interpreteerbaar:

Disjunctieve reductie:

[2b3(=2a2)]

·[

g

_s(z)

:=

e

_s];

_{(dj.rdc.,Sk+1)} (A(x)

e

_s) ) :

ongeldig

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

e

_s uit x).

(a3)

Argument-reductie/ Instantiatie; vanuit variabele, meervoudig, naar 'Skolem' constanten .

Vanuit [2b3]:

[2b4] Bijv.: {

x (A(x)

(

y B(y)))}

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

x (A(x)

(

y B(y)))) : geldig.
E-kwantor buitenplaatsing.

_(snn.) (prenex): {

y (A(x)

B(y) ) }

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

y (A(x)

B(y) ) ) : geldig.
C.q. (Sk.): {A(x)

g

_s(x) ) } [

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

(D.w.z. Steeds een nieuwe, onbepaalde keuze

g

_s uit y, voor elk onderscheiden element x, geldig bij elke x).

[2b5a1]

·[x

:=

c

_d];

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

c

_d)

g

_s(

c

_d) ) ) [

_ref {c1/ (B1/B2/ ..).c1};] : geldig.

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij die

c

_d).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

c

_d. Daarom geldt hier synonymie:

[2b5a1] Syntactische reductie (synonymie):

·[

g

_s(

c

_d )

:=

d

_s];

_(Sk+1;snn.) (A(

c

_d)

d

_s ) ) : geldig.

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een bestaande, vaststaande selectie

c

_d uit x).

[2b5a2]

·[

c

:=

c

_s];

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

c

_s)

d

_s) ) : geldig.

[

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

_ref {A1/A2/ ..B1/B2/ ..};]

[2b5a2]

_(Sk-1) (

y (A(x)

B(y) ) );

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

Alternatieve afleiding,

ongeldig

:
Onevenwichtige instantiatie:

De B term (Literaal) is hier wegens Disjunctie niet onafhankelijk interpreteerbaar:

[2b5b1]

C2·[x

:=

c

_d];

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

g

_s(

c

_d) ) ) :

ongeldig

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij elke x).

Alternatieve afleiding, geldig:

Vanuit [2]:

[2c1(=2b5b1)]

·[y

:=

g

_s(

c

_d)];

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

g

_s(

c

_d) ) ) :

ongeldig

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

g

_s uit y, voor een bestaande, vaststaande selectie

c

_d uit x, geldig bij elke x).

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt niet minder voor een instantie met een welbepaalde selectie

c

_d. Daarom geldt hier synonymie:

[2c1(=2a2)] Syntactische reductie (synonymie):

·[

g

_s(

c

_d )

:=

d

_s];

_(Sk+1;snn.) (A(x)

d

_s) ) : geldig.

[

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

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

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

Alternatieve afleiding, geldig:

[2c1] Syntactische reductie (synonymie):

·[

c

:=

c

_s];

_(Sk+1;snn.) (A(x)

g

_s(

c

_s) ) ) : geldig.

[

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

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

(D.w.z. een nieuwe, onbepaalde selectie

g

_s uit z, per element uit een nieuwe, onbepaalde keuze

c

_s uit y, geldig bij elke x.

Het verwijzingsgebied van elke

g

_s instantie is hier -per definitie- onbepaald. Dus dat geldt zeker ook voor een instantie met een onbepaalde selectie

c

_s. Daarom geldt hier synonymie:
Maar: is een selectie {(B1/B2/ ..).(B1/B2/ ..).c0} wel identiek aan een selectie {(B1/B2/ ..).c0} ?

[2c2(=2a2)] Syntactische reductie (synonymie):

·[

g

_s(

c

_s)

:=

d

_s];

_(Sk+1;snn.) (A(x)

d

_s) ) :

ongeldig

[

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

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

(D.w.z. een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij elke x ).

[2c3(=2b5a2)]

·[x

:=

c

_s];

_(Sk+1) (A(

c

_s)

d

_s) ) : geldig.

[

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

_ref {A1/A2/ .. B1/B2/ ..};]

(D.w.z. Een nieuwe, onbepaalde keuze

d

_s uit y, geldig bij een nieuwe, onbepaalde keuze

c

_s uit x).

Idem dito, met meerplaatsige predikaten.

Bijv.: {

x (A(x)

(

y C_(x,y)))}

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

x (A(x)

(

y C_(x,y)))) : geldig.
E-kwantor buitenplaatsing.

_(snn.) (prenex): {

y (A(x)

C_(x,y)))}

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

y (A(x)

C_(x,y)))) : geldig.
C.q. (Sk.): {A(x)

C_(x,

g

_s(x))}

[

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

·[x

:=

c

_d];

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

c

_d)

C_(

c

_d,

g

_s(

c

_d))) : geldig.

[

_ref {A.c1/ C.c1.((1/2/..).c1)};]

·[

g

_s(

c

_d )

:=

d

_s];

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

c

_d)

C_(

c

_d,

d

_s)) [

_ref {A.c1/ C.c1.((1/2/..).d0)};] : geldig.

·[

c

:=

c

_s];

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

c

_s)

C_(

c

_s,

d

_s)) [

_ref {(A1/A2/ ..).c0/ C((1/2/..).c0).((1/2/..).d0)};] : geldig.

Bijv.: {

y (A(y)

z C_(x,z))}

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

y (A(y)

z C_(x,z))) : geldig.
U-kwantor buitenplaatsing; E-kwantor buitenplaatsing.

_(snn.) (prenex): {

z (A(y)

C_(x,z))}

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

z (A(y)

C_(x,z))) : geldig.
C.q. (Sk.): {A(

d

_s)

C_(x,

h

_s(x))}
[

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

·[x

:=

c

_d];

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

d

_s)

C_(

c

_d,

h

_s(

c

_d) ) )
[

_ref {(A1/A2/..).d0/ C.c1.((1/2/..).c1)};] : geldig.

·[

h

_s(

c

_d )

:=

e

_s];

_(Sk+1) (A(

d

_s)

C_(

c

_d,

e

_s) )
[

_ref {(A1/A2/..).d0/ (C.c1.((1/2/..).1), C.c1.((1/2/..).2), ..)};] : geldig.

·[

h

_s(

c

_d )

:=

e

_s];

_{(degres

)}_(dj.xpn.) (A(

d

_s)

C_(

c

_s,

e

_s) )
[

_ref {(A1/A2/ ..).d0, C((1/2/..).c0).((1/2/..).e0)};] : geldig.