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

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

q }

_(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

_d0 )

¬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)) );

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

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] (2a).
(¬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)));