Introductie_Predikatenlogica_PDL_Deel_IV_H

Cursus / training:

Methode Formele Logica

^©

IV. **Wetten voor logische Normaal Vorm conversies [III].**

**Wetten voor Semantische Parafrase Reductie, in PDL.**

Wetten voor reductie via eliminatie van redundante (deel)redenering (clause) - alle onder parafrase/ Equivalentie .

Syntactische verandering met (syntactische) termreductie;
met/zonder (semantische) verandering van hoofdconnectief, maar zonder (semantisch) verlies van logische kracht .

8. **Parafrase reductie via Syntactische doublure eliminatie.**

Syntactische verandering -

• met (syntactische) termreductie;
• met/zonder (semantische) verandering van hoofdconnectief;
• maar zonder (semantisch) verlies van logische kracht.

8A.

**Directe Syntactische doublure.**

8A.1.

Directe Syntactische doublure , in DNF: basale Conjunct Equivalentie.

Conjunct eliminatie; wegens 'basale Conjunct Equivalentie' (clause equivalence).
Triviaal:

{(

x A(x))

(

y A(y)) }

C2·[y

:=

x];

_(u) (

x A(x)) : geldig.

Maar:
[CHK:]

{(

x A(x))

(

y A(y)) }

C2·[y

:=

x];

_(u) (

x A(x)) :

ongeldig

.
{(

x A(x))

(

y A(y)) }

C2·[y

:=

x];

_(u,degres
) (

x A(x)) : geldig.

(Zie verder: Argument-unificatie).

8B.

**Indirecte Syntactische doublure .**

8B.1.

Indirecte Syntactische doublure , in CNF: basale Conjunct Implicatie.

Conjunct eliminatie; wegens 'basale Conjunct Implicatie' (clause implication).
Basale Condensatie - van Conjunctie: Het sterkste element 'overleeft'.
'Clause implication' (zie: A. Leitsch, 1997, pp.199-210).
Algemene regel (in

PPL

):
'Conjunct Implicatie regel'.

{(p

_(u) p;
{(p

q) }

_(u) p.

Bijv.: {A(x)

c

_d) }

[

_PPL {(A1

A2)

A1) }

(A1

A2).]
[Indien

c

_d is een (bestaande) 'domein' constante:
[

(

x (({x}

=

{x_[1]

..

, x_[i]

..

, x_[n]} )

((

c

{x} )

(A(x)

_(degres
) A(

c

_d) ) ) )_x );]

_(u,C) A(x).

Bijv.: {A(x)

f

_d(x)) }

[Indien

f

_d(x) is een (bestaande) 'domein' functie:
[

(

x (({x}

=

{x_[1]

..

, x_[i]

..

, x_[n]} )

((

f

_d(x)

{ x} )

(A(x)

_(degres
) A(

f

_d(x)) ) ) )_x );]

_(u,C) A(x).

9. **Parafrase reductie via Transferente Equivalentie.**

9A.

Indirecte Transferente Equivalentie: via Basale Implicatie.

Factoriseren (factoring) (in

PDL

): Levert een factor.

9A.2.

Indirecte Transferente Equivalentie , in DNF: via Basale Disjunct Implicatie.

Disjunct eliminatie; wegens 'Basale Disjunct Implicatie' (clause implication).
Bij 'Lokale redundantie' binnen Complexe Disjunctie.
Basale Condensatie - van Disjunctie: Het zwakste element 'overleeft'.
'Condensing principle' (zie: A. Leitsch, 1997, pp.95-96).
Algemene regel (in

PPL

):
'Disjunct Implicatie regel'.

{(p

_(u) q;
{(p

q) }

_(u) q.

9A.2a)

Algemene vorm.

Eliminatie van basale Disjunct.

Bijv.: {A(x)

c

_d) }

[

_PPL {(A1

A2)

A1) };

_(u) A1.]
[Indien

c

_d is een (bestaande) 'domein' constante:
[

(

x ((

c

{x} )

(A(x)

_{(degres
)} A(

c

_d) ) )_x );]

_(u,C) A(

c

_d).

Bijv.: {A(x)

f

_d(x)) }

[Indien

f

_d(x) is een (bestaande) 'domein' functie:
[

(

x (({x}

=

{x_[1]

..

, x_[i]

..

, x_[n]} )

((

f

_d(x)

{ x} )

(A(x)

_(degres
) A(

f

_d(x)) ) ) )_x );]

_(u,C) A(

f

_d(x)).

9A.1b)

Met tweeplaatsige predicatie.

Bijv.: {(A(x,x)

c

_d,

c

_d )) }

_(u,C) A(

c

_d,

c

_d ).

Echter:

Bijv.: {(A(x,x)

A(x,

c

_d)) }

A(x,

c

_d) :

ongeldig

(D.i. illegitieme argument-differentiatie, zie elders).

9A.1c)

Met drieplaatsige Disjunctie.

General Factoring.

9A.1c.1)

General Positive Factoring.

{(A(x)

c

_d)

B) } ≡ _(u,C) (A(

c

_d)

B).

Maar:
{(A(x)

c

_d)

B) }

c

_d) :

ongeldig

.
{(A(x)

c

_d)

B) }

(A(

x

)

B) :

ongeldig

9A.1b.2)

General Negative Factoring.

{(¬A(x)

¬A(

c

_d)

B) } ≡_(u,C) (¬A(

c

_d)

B).

9B.

Indirecte Transferente Equivalentie : via Complexe Implicatie.

9B.1.

Indirecte Transferente Equivalentie, in CNF: via Basale Complexe Conjunct Implicatie .

Eliminatie van basale Disjunctie, wegens 'Basale Complexe Conjunct Implicatie' (clause implication).
Bij (globale) redundantie van basale Disjunctie.

9B.1a)

Algemene vorm.

Eliminatie van basale Disjunctie, wegens 'Transferente Implicatie'.

Bijv.: {A(x)

(A(

c

_d)

B) }

[

_PPL {(A1

A2)

(A1

B) }

(A1

A2).]
Reïteratie 1.
[

(A(x)

c

_d)

(A(

c

_d)

B));
[

{A(x)

c

_d) } : is geldig.]
[

{A(x)

(A(

c

_d)

B) } : is geldig.]
Distributie 1:

((A(x)

c

_d))

(A(x)

B) );
Lokale Absorptie 1:

_(u,C) (A(x)

(A(x)

B) );

_(u,trf.eqv.) {A(x) }.

Echter: Conjunct Implicatie - niet reduceerbaar.

Bijv.: {A(

c

_d)

(A(x)

B) }

c

_d) :

ongeldig

[

_PPL {A1

((A1

A2)

B) };
[

_(lok.distr.) {A1

((A1

(A2

B)) };

_(trf.eqv.) {A1

(A2

B) };
[

{A(x)

c

_d) } : is geldig.]
[

{(A(x)

(A(

c

_d)

B) } : is geldig.]
[

{A(x)

(A(

c

_d) } : is

ongeldig

.]
Distributie 1:

((A(

c

_d)

A(x))

(A(

c

_d)

B) );
Lokale Absorptie 1:

_(u,C) (A(x)

(A(

c

_d)

B) ) );
Niet verder reduceerbaar.

N.b. Wel geldig is degressie, via Conjunctieve reductie, c.q. instantiatie:

Bijv.: {A(

c

_d)

(A(x)

B) }

C2·[x

:=

c

_d];

_(i)_(degres
) {A(

c

_d)

(A(

c

_d)

B);

_(u,trf.eqv.) A(

c

_d) : is geldig.

9B.1b)

Met daarnaast symmetrisch equivalente Disjuncten

Eliminatie van basale Disjunctie, Wegens 'Parallelle Implicatie'.
Via Contractie van Disjuncties.

{(

A(x)

(

A(
c
_d)

[

{(A(x)

(A(

c

_d)

B) } : is geldig.]
Basale Comprimatie 1:

_(u) ((

A(x)

A(
c
_d)

)

B )

C);
Lokale Absorptie 1:

_(u,C) ((

A(x)

C);

{(

A(x)

(

A(
c
_d)

[

{(A(x)

(A(

c

_d)

C) } : is geldig.]
Herordening 1:

((

A(x)

C) )

((

A(
c
_d)

C) )

D}
Comprimatie 1:

_(u) (((

A(x)

A(
c
_d)

)

C))

D);
Lokale Absorptie 1:

_(u,C) ((

A(x)

D).

(

A(x)

D).

9B.1c)

Met daarnaast symmetrisch niet-equivalente Disjuncten

{(

A(x)

(

A(
c
_d)

C) }

[

_PPL {((A1

A2)

(A1

C) };]

Route 1.

Distributie 1 (splits 1e Disjunctie):

(((

A(x)

(

A(
c
_d)

C))

(

A(
c
_d)

C)));
Distributie 2:

((

A(x)

A(
c
_d)

)

(

A(x)

A(
c
_d)

)

C));
Lokale Absorptie 1:

_(u,C) (

A(x)

(

A(x)

A(
c
_d)

)

C));
Globale transferente Equivalentie eliminatie 1:

_(u) (

A(x)

A(
c
_d)

)

C));
Globale transferente Implicatie eliminatie 1:

_(u) (

A(x)

C)).

Route 2.

Distributie 1 (splits 2de Disjunctie):

(((

A(x)

A(
c
_d)

)

((

A(x)

C)));
Distributie 2:

((

A(x)

A(
c
_d)

)

A(
c
_d)

)

(

A(x)

C));
Lokale Absorptie 1:

_(u,C) (

A(x)

(

A(
c
_d)

(

A( x)

C));
Globale transferente Implicatie eliminatie 1:

_(u) (

A(x)

(

A(x)

C));
Globale transferente Equivalentie eliminatie 1:

_(u) (

A(x)

C)).

Dus ook:

{(

A(x)

(

A(
c
_d)

D};

_(u,C) ((

A(x)

C))

D);

{(

A(x)

(

A(
c
_d)

E};

Comprimatie 1:

((B

((

A(x)

(

A(
c
_d)

D )))

E);
Lokale Distributie 1, 2; Lokale Complexe Disjuncties Contractie:

_(u,C) ((B

((

A(x)

D)))

E);

((

A(x)

D))

E).

9B.2.

Indirecte Transferente Equivalentie , in DNF: via Basale Complexe Disjunct Implicatie.

Eliminatie van basale Conjunctie, wegens 'Basale Complexe Disjunct Implicatie' (clause implication).
Bij (globale) redundantie van basale Conjunctie.
Algemene regel (in

PPL

{(p

q) }

_(u) q.
{(p

p} [

({p

p );]

_(u) p.
{(p

p} [

({p

p );]

_(u) p.

(9B.2a)

Algemene vorm.

Eliminatie van basale Conjunctie, wegens 'Transferente Implicatie'.

Bijv.: {A(

c

_d)

(A(x)

B) }

[

_PPL {A1

((A1

A2)

B) };

_(u) A1.]
Reïteratie 1.
[

(A(

c

_d)

(A(x)

c

_d)

B));
[

{A(x)

c

_d) } : is geldig.]
[

{(A(x)

c

_d) } : is geldig.]
Distributie 1:

((A(

c

_d)

A(x)) )

(A(

c

_d)

B) );
Lokale Condensatie 1:

_(u,C) (A(

c

_d)

(A(

c

_d)

B) );
Transferente Equivalentie eliminatie 1:

_(u) A(

c

_d).

Echter:
Disjunct Implicatie - niet reduceerbaar.

Bijv.: {A(x)

(A(

c

_d)

B) }

[

_PPL {(A1

A2)

(A1

B)) };

_(u) (A1

(A2

B)).]
[

{A(x)

c

_d) } : is geldig.]
[

{A(x)

(A(

c

_d)

B) } : is

ongeldig

.]
Distributie 1:

((A(x)

c

_d))

(A(x)

B) );
Lokale Condensatie 1:

_(u,C) (A(

c

_d)

(A(x)

B) );
Is niet verder reduceerbaar.

N.b. Wel geldig is degressie, via Conjunctieve reductie, c.q. instantiatie:

{A(x)

(A(

c

_d)

B) }

·[y

:=

x];

_(i)_{(degres
)} A(

c

_d) : is geldig.

9B.2b)

Met daarnaast symmetrisch equivalente Disjuncten

Eliminatie van basale Conjunctie, Wegens 'Parallelle Implicatie'.
Via Contractie van Conjuncties.

{(A(x)

(A(

c

_d)

Basale Comprimatie 1:

_(u) ((A(x)

c

_d))

B )

C);
Lokale Condensatie 1:

_(u,C) ((A(

c

_d)

C);

{(A(x)

( A(

c

_d)

Herordening 1:

((A(x)

C) )

((A(

c

_d)

C) )

D}
Comprimatie 1:

_(2u) (((A(x)

c

_d))

C))

D);
Lokale Condensatie 1:

_(u,C) ((A(

c

_d)

D).

9B.2c)

Met daarnaast symmetrisch niet-equivalente disjuncten

{(A(x)

(A(

c

_d)

C) }

[

_PPL {((A1

A2)

(A1

C) };]

Route 1.

Distributie 1 (splits 1e Conjunctie:

(((A(x)

(A(

c

_d)

C))

(A(

c

_d)

C)));
Distributie 2:

((A(x)

c

_d))

(A(x)

c

_d))

C));
Lokale Condensatie 1:

_(u,C) (A(

c

_d)

(A(x)

c

_d))

C));
Globale transferente Equivalentie eliminatie 1:

_(u) (A(

c

_d)

(A(x)

C)) : niet verder reduceerbaar.

Route 2.

Distributie 1 (splits 2de Conjunctie:

(((A(x)

c

_d))

((A(x)

C)));
Distributie 2:

((A(x)

c

_d))

c

_d))

(A(x)

C));
Lokale Condensatie 1:

_(u,C) (A(

c

_d)

c

_d))

(A(x)

C));
Globale transferente Equivalentie eliminatie 1:

_(u) (A(

c

_d)

(A(x)

C)) : niet verder reduceerbaar.

Dus ook:

{(A(x)

(A(

c

_d)

D};

((A(

c

_d)

(A(x)

C)))

D) : niet verder reduceerbaar.

{(A(x)

( A(

c

_d)

E};

Comprimatie 1:

_(u) ((B

((A(x)

(A(

c

_d)

D)))

E);
Lokale Distributie 1, 2; Lokale Complexe Disjuncties Contractie:

_(u,C) ((B

((A(x)

D)))

E);

((A(x)

D))

E).

10. **Parafrase reductie via 'Niet-fatale ' ('pseudo') contradictie.**

10A.

Directe 'Niet-fatale' ('pseudo') contradictie.

10A.2.

Directe 'Niet-fatale' ('pseudo') contradictie, in DNF: tussen (basale/ lokale ) disjuncten.

Tautologie.
Algemeen: mutatis mutandis als in

PPL

.
Specifiek in

PDL

:
Bijv. via argument renaming:

Bijv.: {A(x,x)

¬A(x,y) }

C2·[y:=x]

_(u)_(bas.taut.)

$

1 : is geldig.

10B.

Indirecte 'Niet-fatale ' ('pseudo') contradictie.

10B.1.

Indirecte 'Niet-fatale' contradictie, in CNF: via Complexe Conjunct Contradictie.

Indirecte Transferente contradictie reductie.
Met basale Negatieve Literaal.

{(

A

(x)

¬A

(

c

_d) }

Route 1.

Reductie via Basale Distributie, naar Disjunctie:

_(bas.distr.) ((

A

(x)

¬A

(

c

_d) )

¬A

(

c

_d)) );

_{(lok.cj.rei.)} ((

A

(x)

A

(

c

_d)

¬A

(

c

_d) )

¬A

(

c

_d)) );

_(u,lok.ctd.) ((

A

(x)

$

0 )

¬A

(

c

_d)) );

_(lok.ctd.) ((

$

¬A

(

c

_d)) );

Route 2.

Reductie via Lokale reïteratie, resp. Lokale Distributie:

_{(lok.cj.rei.)} (((

A

(x)

A

(

c

_d) )

B )

¬A

(

c

_d) );

_(lok.distr.) (((

A

(x)

B )

(

A

(

c

_d)

B ) )

¬A

(

c

_d) );

_(syn.rdc.) ((

A

(x)

B )

(

A

(

c

_d)

B )

¬A

(

c

_d) );

_(u,trf.ctd) ((

A

(x)

B )

¬A

(

c

_d ) );

Route 2.1.

Reductie via Basale Transferente Equivalentie, direct.

_{(bas.trf.eqv.)} (B

¬A

(

c

_d) );

Route 2.2.

Reductie via Basale Transferente Equivalentie, indirect.

_(bas.distr.) ((

A

(x)

¬A

(

c

_d) ) )

¬A

(

c

_d ) ) ) );

_(lok.doub.) ((

A

(x)

¬A

(

c

_d) )

¬A

(

c

_d) ) );

_{(lok.cj.rei.)} ((

A

(x)

A

(

c

_d)

¬A

(

c

_d) )

¬A

(

c

_d) ) );

_(lok.ctd.) ((

A

(x)

$

B )

¬A

(

c

_d) ) );

_(lok.ctd.) ((

$

¬A

(

c

_d) ) );

Route 2.3.

Nutteloos:

_{(lok.cj.rei.)} (((

A

(x)

A

(

c

_d) )

B )

¬A

(

c

_d) );

_(lok.distr.) (((

A

(x)

(

A

(

c

_d)

B) ) )

¬A

(

c

_d) );

_(syn.rdc.) ((

A

(x)

B )

(

A

(

c

_d)

B )

¬A

(

c

_d) );

_(trf.ctd) ((

A

(x)

B )

¬A

(

c

_d) );

_(syn.rdc.) ((

A

(x)

B )

¬A

(

c

_d ) );
etc..

¬A(

c

_d)).

Idem ditto, met impliciete argument instantiatie.

{(

A

(x,

d

)

¬A

(

c

_d,y) }

((

A

(x,

d

)

¬A

(

c

_d,y))

¬A

(

c

_d,y)) );
[

(

x (A(x,

d

)

·[x

:=

c

_d];

_(i) A(

c

_d,

d

));]
[

(

y (A(

c

_d,y )

·[y

:=

d

];

_(i) A(

c

_d,

d

));]

((

A

(x,

d

)

¬A

(

c

_d,y)

A

(

c

_d,

d

)

¬A

(

c

_d,

d

) )

¬A

(

c

_d,y)) );

_(u) ((

A

(x,

d

)

¬A

(

c

_d,y)

c

_d 0 )

¬A

(

c

_d ,y)) );

((

$

¬A(

c

_d,

d

)) );

¬A(

c

_d,

d

)).

{(

A

(

c

_d)

¬A

(x) }

Route 1.

Reductie via Basale Distributie, naar Disjunctie:

_(bas.distr.) ((

A

(

c

_d)

¬A

(x) )

¬A

( x)) );

_{(lok.cj.rei.)} ((

A

(

c

_d)

¬A

(

c

_d)

¬A

(x) )

¬A

(x)) );

_(u,lok.ctd.) ((

$

¬A

(x))

¬A

(x )) );

_(lok.ctd.) ((

$

¬A

(x)) );

¬A(x)).

Met lokale Negatieve Literaal.

{

A

(x)

(

¬A

(

c

_d)

B) };

Route 1.

Basale Distributie:

_(bas.distr.) ((

A

(x)

¬A

(

c

_d))

(

A

(x)

B));
Lokale Contradictie:

_(lok.ctd.) ((

$

(

A

(x)

B));

(

A

(x)

B).

{

A

(

c

_d)

(

¬A

(x)

B) };

Route 1.

Basale Distributie:

_(bas.distr.) ((

A

(

c

_d)

¬A

(x))

(

A

(

c

_d)

B));
Lokale Contradictie:

_(lok.ctd.) ((

$

(

A

(

c

_d)

B));

(

A

(

c

_d)

B).

10B.2.

Indirecte 'Niet-fatale' contradictie , in DNF: via Indirecte Transferente contradictie.

Impliciete relatie van Implicatie.

10B.2.1.

Indirecte 'Niet-fatale' contradictie, in DNF: via Indirecte Transferente contradictie ; met 'domein' constanten/ functies.

10B.2.1 (1a).

Bijv.: {A(x)

¬A(

c

_d) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

(

x (A(x)

¬A(

c

_d)) );

(

x (¬A(

c

_d)

A(x)) );
Connectief conversie: naar Implicatie.

(

x (A(

c

_d)

A(x)) );

(A(

c

_d)

(

x A(x)) );

(A(

c

_d)

A(x) );

(

c

x ) :

ongeldig

(niet (verder) reduceerbaar).
[2]

Lezing 2.

Inadequate interpretatie.

Inverse universele instantiatie, naar proximaal vorm.

((

x A(x))

¬A(

c

_d) );

(¬A(

c

_d)

(

x A(x)) );
Connectief conversie: naar Implicatie.

(A(

c

_d)

(

x A(x)) );

(

x (A(

c

_d)

A(x)) );

[1] :

ongeldig

(niet verder reduceerbaar).

10B.2.1 (1b).

Bijv.: {A(x)

¬A(

f

_d(x)) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

(

x (A(x)

¬A(

f

_d(x)) );

(

x (¬A(

f

_d( x))

A(x) );
Connectief conversie: naar Implicatie.

(

x (A(

f

_d(x ))

A(x) );

(A(

f

_d(x))

A( x) );

(

f

_d(x)

x ) :

ongeldig

(niet (verder) reduceerbaar).

10B.2.1 (2a).

Bijv.: {¬A(x)

c

_d) }

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

(

x (¬A(x)

c

_d)) );
Connectief conversie: naar Implicatie.

(

x (A(x)

c

_d)) );

(

x (x

c

_d) ) :

ongeldig

(niet (verder) reduceerbaar).
[2]

Lezing 2.

Inadequate interpretatie.

Inverse universele instantiatie, naar proximaal vorm.

((

x ¬A(x))

c

_d) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.

((¬

x A(x))

c

_d) );

(¬(

x A(x))

c

_d) );
Connectief conversie: naar Implicatie.

((

x A(x))

c

_d) );

(

x (A(x)

c

_d) );

[1] :

ongeldig

(niet (verder) reduceerbaar).

10B.2.1 (2b).

Bijv.: {¬A(x)

f

_d(x)) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

Inverse NNF conversie: Basale Negatie voorplaatsing.

(

x (¬A(x)

f

_d(x)) );
Connectief conversie: naar Implicatie.

(

x (A(x)

f

_d(x))) );

(A(x)

f

_d( x)) );

f

_d(x ) ) :

ongeldig

(niet (verder) reduceerbaar).

10B.2.2.

Indirecte 'Niet-fatale' contradictie , in DNF: via Indirecte Transferente contradictie; met Skolem constanten/ functies.

10B.2.2 (1a).

Bijv.: {A(x)

¬A(

c

_s) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

_(UI-1) (

x (A(x)

¬A(

c

_s)) );

Globale Kwantor binnenplaatsing.

[Zie 7.1.2.1. U-Kwantor-verplaatsing: 'binnenplaatsing', volgordebehoudend. (3) In Disjunctie. Eerste term.]
(

x (P(x)

Q );

_(iso) (P1/Q, P2/Q, ..);

_{(bas.comp.:cj.-dj.)} ((P1,P2, ..)/ Q );

_(PDL) ((

x P(x))

Q );

_(NNF-1) ((

x A(x))

¬A(

c

_s)) );
Inverse Skolemisatie.

_(Sk-1) (

x (A(x)

¬A(y)) );

(

x (A(y)

A(x)) );

(A(

c

_s)

A(x );

(

c

x ) :

ongeldig

(niet (verder) reduceerbaar).

Idem, genoteerd (isomorf) in

PPL

_(iso
) ((A₁, A₂, A₃,

..

)

(¬A₁/ ¬A₂/ ¬A₃/

..

) );

((A₁, A₂, A₃,

..

) / ¬A₁ / ¬A₂/ ¬A₃/

..

);

_(trf.ctd.1) ((A₁, A₂,

..

) / ¬A₁/ ¬A₂/ ¬A₃/

..

);

_(trf.ctd.2) ((A₁,

..

) / ¬A₁/ ¬A ₂/ ¬A₃/

..

);

..

_{(trf.ctd. (n-1)))} (A₁ / ¬A₁/ ¬A₂ / ¬A₃/

..

);

_(bas.taut.) (

$

1/ ¬A₂/ ¬A₃/

..

);

_{(bas.cds. 2..n)}

$

[2]

Lezing 2.

Inadequate interpretatie.

Inverse universele instantiatie, naar proximaal vorm.

_(UI-1) ((

x A(x))

¬A(

c

_s) );
Inverse Skolemisatie.

_(Sk-1) ((

x A(x))

(

y ¬A(y)) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.

((

x A(x))

(¬

y A(y)) );

((

x A(x))

¬(

y A(y)) );
Connectief conversie: naar Implicatie.

((

y A(y))

(

x A(x)) );

[2.1]

Lezing 2.1.

_(bas.taut.)

$

1 : geldig (Tautologie).
[2.2]

Lezing 2.2.

Inadequate interpretatie.

Illegitieme universele instantiatie.

x );
Inverse universele instantiatie, naar prenex vorm.
Universele kwantor differentiatie.

(

x (A(y)

A(x)) ) :

ongeldig

(niet (verder) reduceerbaar ).

10B.2.2 (1b).

Bijv.: {A(x)

¬A(

f

_s(x)) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

_(UI-1) (

x (A(x)

¬A(

f

_s(x)) );
Inverse Skolemisatie.

_(Sk-1) (

y (A(x)

¬A(y)) );
Connectief conversie: naar Implicatie.

(

y (A(y)

A(x)) );

(A(

f

_s(x))

A(x) );

(

f

_s(x)

x ) :

ongeldig

(niet (verder) reduceerbaar).
[2]

Lezing 2

. Inadequate interpretatie.

Universele kwantor differentiatie.

(A(x)

¬A(

f

_s(z)) );
Inverse universele instantiatie, naar proximaal vorm.

_(UI-1) ((

x A(x))

¬A(

f

_s(z)) );
Inverse Skolemisatie.

_(Sk-1) ((

x A(x))

(

z ¬A(y)) );

((

x A(x))

(¬

z A(y)) );

((

x A(x))

(¬

y [

z] A(y)) );

((

x A(x))

¬(

y [

z] A(y)) );

(¬(

y [

z] A(y))

(

x A(x)) );
Connectief conversie: naar Implicatie.

((

y [

z] A(y))

(

x A(x)) );

(

y (([

z] A(y))

(

x A(x))) );

(

y [

z] (A(y)

(

x A(x)) );

(

y [

x (A(y)

A(x)) );

(A(y)

A(x) );

x ) :

ongeldig

(niet (verder) reduceerbaar).

10B.2.2 (2a).

Bijv.: {¬A(x)

c

_s) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

_(UI-1) (

x (¬A(x)

c

_s) );
Globale Kwantor binnenplaatsing.

[Zie 7.1.2.1. U-Kwantor-verplaatsing: 'binnenplaatsing', volgordebehoudend. (3) In Disjunctie. Eerste term.]
(a) [(

x (P(x)

Q )

((

x P(x))

Q );

_(iso) (((P1/ Q ), (P2/ Q ), .. )

_{(bas.comp.:cj.-dj.)} ((P1, P2 )/ Q ) : geldig.]
(b) [(

x (¬P(x)

Q );

_(iso) (¬P1/Q, ¬P2/Q, ..);

_{(bas.comp.:cj.-dj.)} ((¬P1,¬P2, ..)/ Q );

_(PDL) ((

x ¬P(x))

Q );]
(c) [(

x (¬P(x)

Q )

((

x ¬P(x))

Q );

_(iso) (((¬P1/ Q ), (¬P2/ Q ), .. )

_{(bas.comp.:cj.-dj.)} ((¬P1, ¬P2 )/ Q ) : geldig.]

((

x ¬A(x))

c

_s) );
Inverse NNF conversie.

[((

x ¬P(x))

Q )

(¬(

x P(x))

Q );

_(iso) ((¬P1, ¬P2 )/ Q )

_{(lok.cnc.cvs.cj-dj.)} (¬(P1/ P2 )/ Q ) : geldig.]

(¬(

x A(x))

c

_s) );
Inverse Skolemisatie.

_(Sk-1) (

x (¬A(x)

A(y)) );

_(iso) (((¬P1/ (Q1/Q2).c0 ), (¬P2/ (Q1/Q2).c0 ), .. );

[1a]

(

y ((

x ¬A(x))

A(y)) );

_{(compr.:cj.-dj.)} ((¬P1, ¬P2 )/ (Q1/Q2).c0 );

(

y (¬(

x A(x))

A(y)) );

_(iso) ((¬P1, ¬P2 )/ (Q1/Q2) )

_{(lok.cnc.cvs.cj-dj.)} (¬(P1/ P2 )/ (Q1/Q2) ) : geldig.]

Inverse NNF conversie.
(Lokale Kwantor binnenplaatsing).

(¬(

x A(x))

(

y A(y)) );
Connectief conversie: naar Implicatie.

((

x A(x))

(

y A(y)) );
[1b] Connectief conversie: naar Implicatie.

(

x (A(x)

A(y)) );
Kwantor-binnenplaatsing met Universeel-existentieel conversie.

(

y ((

x A(x))

A(y)) );

Verantwoording van het voorgaande:
[(

x (P(x)

Q )

((

x P(x))

Q );

_(iso) (((P1 imp. Q ), (P2 imp. Q ), .. )

_{(lok.compr.:cj.-dj.)} ((P1/ P2 ) imp. Q ) : geldig.]
{(

x P(x))

Q } : Dat er een (minstens één) x een P is, is voldoende voorwaarde voor (waarheid/geldigheid van) Q.
D.w.z. '

x P(x)' wijst op een Disjunctie van (alle) x uit X.
Wijst dus (nog) niet op een [? onbekende /onbepaalde] subset (Conjunctie) van (sommige) x uit X.
(Is dus (nog) niet een [? onbekend /onbepaald] element uit de power set van X).

Tweede Kwantor-binnenplaatsing (zonder kwantor conversie).

((

x A(x))

(

y A(y)) )

_(lok.taut.)

$

1 :

sluit

(blijkt geldig);

Verantwoording van het voorgaande:

_(iso) ((P1 imp. (P1/P2/..).c0), (P2 imp. (P1/P2/..).c0), .. );

_{(lok.compr.:dj.-cj.)} ((P1/P2/..) imp. (P1/P2/..).c0 );
{(

x P(x))

(

y P(y))} : Dat er een (minstens één) ding x een P is, betekent : Dat er een (minstens één) ding y een P is.
Als dit geldig is, zou dat betekenen: dat je uit een existentiële predicatie altijd kunt differentiëren naar een identieke existentiële predicatie modulo de existentiële variabelenaam/namen.

[1.1]

Route 1.1.

Her-Skolemisatie.

_(Sk+1) (

x (¬A(x)

c

_s));

((

x ¬A(x))

c

_s));

(¬(

x A(x))

c

_s));
[

(¬(

x A(x))

c

_s));]
Skolemisatie.
Van lokale existentiële kwantor: Illegitiem.

_(Sk+1) (¬A(

d

_s)

c

_s) ) :

open

(blijkt ongeldig);
[1.2]

Route 1.2.

Vanaf hier is het onzin:
schending vereiste voorbewerkingen voor Skolemisatie; tevoorschijn toveren van een heel andere UI-Sk formule).
Skolemisatie.
Illegitiem.

_(Sk+1) (

y (A(

d

_s)

A(y)) ) :

open

(blijkt ongeldig );

(A(

d

_s)

(

y A(y)) );

Dit is alleen geldig als

d

_s nieuw is.
[Maar zo Skolemiseer je toch niet, in een niet-NNF, niet-CNF enz. formule?]

Connectief conversie: naar Implicatie.

(

y (¬A(

d

_s)

A(y)) );

(¬A(

d

_s)

(

y A(y)) );
Her-Skolemisatie.

Is dit alleen geldig als ook

c

_s nieuw is?

_(Sk+1) (¬A(

d

_s)

c

_s) );

(A(

d

_s)

c

_s) );
Onder invariantie van predikaatnaam:

(

d

c

_s ) :

Illegitiem

Ad [10B.2.2] (2a).
(¬P(x)

c

_s))

_(UI-1) (

x (¬P(x)

c

_s));

_(Sk-1) (

x (¬P(x)

P(y));

(

y ((

x ¬P(x))

P(y));

(

y (¬(

x P(x))

P(y));

(

x (P(x)

P(y));

(

y (

x P(x))

P(y));

((

x P(x))

(

y P(y)) );

_(lok.taut.)

$

1 :

sluit

(blijkt geldig);

_(Sk+1) (

x (¬P(x)

c

_s));

((

x ¬P(x))

c

_s));

(¬(

x P(x))

c

_s));

((

x P(x))

c

_s));

Idem, genoteerd (isomorf) in

PPL

_(iso
) ((¬A₁, ¬A₂, ¬A₃ ,

..

)

(A₁/ A₂/ A₃/

..

) );

((¬A₁, ¬A₂, ¬A₃,

..

) / A₁ / A₂/ A₃/

..

);

_(trf.ctd.1) ((¬A₁, ¬A₂,

..

) / A ₁/ A₂/ A₃/

..

);

_(trf.ctd.2) ((¬A₁,

..

) / A₁/ A₂/ A₃/

..

);

..

_{(trf.ctd. (n-1))} (¬A₁ / A₁/ A₂ / A₃/

..

);

_(bas.taut.) (

$

1/ A₂/ A₃/

..

);

_{(bas.cds. 2..n)}

$

[2]

Lezing 2.

Inadequate interpretatie.

Inverse universele instantiatie, naar proximaal vorm.

_(UI-1) ((

x ¬A(x))

c

_s) );
Inverse Skolemisatie.

_(Sk-1) ((

x ¬A(x))

(

y A(y)) );
Inverse NNF conversie: Lokale Negatie voorplaatsing.

((¬

x A(x))

(

y A(y)) );

(¬(

x A(x))

(

y A(y)) );
Connectief conversie: naar Implicatie.

((

x A(x))

(

y A(y)) );

(A(

d

_s)

(

y A(y)) );

(A(

d

_s)

c

_s) );

(

d

c

_s );

_(vld.)

$

1 : geldig (disjuncte expansie).

10B.2.2 (2b).

Bijv.: {¬A(x)

f

_s(x)) };

Interpretaties.

[1]

Lezing 1.

Inverse universele instantiatie, naar prenex vorm.

_(UI-1) (

x (¬A(x)

f

_s(x)) );
Globale Kwantor binnenplaatsing.

((

x ¬A(x))

f

_s(x)) );
Inverse NNF conversie.

(¬(

x A(x))

f

_s(x)) );

Verantwoording van het voorgaande:
(a) [(

x (P(x)

Q )

((

x P(x))

Q );

_(iso) (((P1/ Q ), (P2/ Q ), .. )

_{(compr.:cj.-dj.)} ((P1, P2 )/ Q ) : geldig.]
(b) [(

x (¬P(x)

Q )

((

x ¬P(x))

Q );

(¬(

x P(x))

Q );

_(iso) (((¬P1/ Q ), (¬P2/ Q ), .. )

_{(compr.:cj.-dj.)} ((¬P1, ¬P2 )/ Q );

_{(lok.cnc.cvs.cj-dj.)} (¬(P1/ P2 )/ Q ) : geldig.]

Inverse Skolemisatie.

_(Sk-1) (

y (¬A(x)

A(y)) );

_(iso) (((¬P1/ (Q1/Q2).f1 ), (¬P2/ (Q1/Q2).f2 ), .. );

[1.1]

Route 1.1.

Connectief conversie: naar Implicatie.

_{(lok.cnc.cvs.dj-imp.)} (

y (A(x)

A(y)) );

_PPL_(iso) (((P1

(Q1/Q2).f1 ), (P2

(Q1/Q2).f2 ), .. );

_PPL_(iso) (((A1

(A1/A2).f1 ), (A2

(A1/A2).f2 ), .. );

_PPL_(iso) (((A1

(A1/A2).1 ), (A2

(A1/A2).2 ), .. );

Her-Skolemisatie.

_(Sk+1) (

x (A(x)

f

_s(x)));
[1.2]

Route 1.2.

Her-Skolemisatie.

_(Sk+1) (

x (¬A(x)

f

_s(x))); Connectief conversie: naar Implicatie.

_{(lok.cnc.cvs.dj-imp.)} (

x (A( x)

f

_s(x)));

_(vld.)

$

1 : geldig (disjuncte expansie).

Ad [10B.2.2] (2b).
(¬P(x)

f

_s(x)))

_(UI-1) (

x (¬P(x)

f

_s(x)));

_(Sk-1) (

x (¬P(x)

P(y));

(

y ((

x ¬P(x))

P(y));

(

y (¬(

x P(x))

P(y));

(

x (P(x)

P(y));

(

y (

x P(x))

P(y));

((

x P(x))

(

y P(y)) );

_(lok.taut.)

$

1 :

sluit

(blijkt geldig);

_(Sk+1) (

x (¬P(x)

f

_s(x)));

((

x ¬P(x))

f

_s(x)));

(¬(

x P(x))

f

_s(x)));

((

x P(x))

f

_s(x)));