Introductie_Predikatenlogica_PDL_Deel_VIe_H

Cursus / training:

Methode Formele Logica

^©

16. Modus ponens (MP).

Sluitrede, 'Material detachment', 'Strong inductive argument'.

16.1. **Algemene regels voor Modus ponens.**

16.1.1. **Opbouw van Modens Ponens.**

Elke Modus Ponens figuur bestaat uit minstens drie elementen c.q. componenten.
Dit zijn zinnen (proposities), nl. minstens twee premissen en één conclusie.

Formalisme, notaties:

(Uitbreiding van de structuur voor Substitutie).

Redeneervorm.

Globale syntax (gestandaardiseerd).

{F₁, F₂ }

F₃.

Conventionele volgorde:

{F₂, F₁ }

F₃.

Componenten:

Drie basale proposities).

(1) F₁ : formule 1, eerste expliciete basale conjunct term;
nl. basisaanname, factieve premisse (Literaal).
In Conjunctie met:
(2) F₂ : formule 2, tweede expliciete basale conjunct term;
nl. afleidingsregel, conditionele premisse (Implicatie).
Levert:
(3) F₃ : formule 3, derde expliciete basale conjunct term;
nl. (eind)conclusie, factieve consequens (Literaal).

Lokale syntax:

(F₁ : {A₁, .. } );
(F₂ : {(A₂

C₂ ) } );
(F₃ : {C₃ } ).

Elementaire termen:

A₁: referent (assumptie, premisse(n) op de baseline).
A₂: target element (assumptie, antecedens, premisse(n) binnen F₂).

C₂: voorwaardelijke conclusie (consequens, binnen F₂).
C₃: eindconclusie (binnen F₃).

Afgeleiden:

A₂(A₁)

=

_(i) A₃ : versie van A₂ in F₂ op grond van A₁; d.w.z., na mgu instantiatie van {A₁,A₂}.

{mgu: most general unifier, zie definitie in 14.1.2).

C₂(A₂(A₁))

=

_(i) C₃ : versie van C₂ in F₂ volgens A₂(A₁); d.w.z. valt onder dezelfde kwantificatie (c.q. extensie) als A₂(A₁).

16.1.2. **Toepassing van Modens Ponens .**

(Applicatie).

Geldige toepassing van Modus ponens.

(·) Het verbinden van twee termen uit de twee gegeven premissen, met name:

• de basale conjunct (referent) in de eerste, factieve basale premisse,
• en de lokale consequens in de tweede, conditionele basale premisse.

Dit op grond van de relatie tussen de betreffende literalen:

(&bull) de betreffende referent
(&bull) en de lokale antecedens (target) in de conditionele premisse:

Van toepassing zijn specififeke criteria:

(&bull) afdoende syntactische relatie (overeenkomstig de beschreven connectiefstructuur);
(&bull) voldoende (relevante) formele gelijkenis;
(&bull) voldoende semantisch raakvlak en overlapping ('gemeenschappelijke deler', unifier), nodig voor een transitieve conclusie.

(·) De tweede premisse 'importeert' het referent vanuit de eerste premisse.
(·) De (eind)conclucie vormt een derde basale conjunct.
Deze bestaat uit de lokale consequens van de conditionele premisse.
De kwantificatie van deze eindconclusie komt hoogstens overeen met de maximale gemeenschappelijke deler ( most general unifier) van referent en target element.

16.2. **Hoofdvormen van Modus ponens .**

Geldige basisvormen: drie standaard normaalvormen.
Daarnaast zijn er diverse andere geldige vormen.

16.2.1. Modus ponens, standaardvorm, in PPL.

(1a1)

Bewijs via 'bevestigende wijs': Modus Ponens (MP).

Via Factief bevestigde premisse;
resp. (impliciete) Transferente contradictie eliminatie; resp. Conjunctieve reductie.
Eenvoudige vorm.

Bijv. (PPL): {X, (X

C)}

(¬X

C) );

_(u) (X

_(degres
) C : is geldig.

Structuurweergave.

Bijv.: {F₁:A₁, F₂: (A₂

C ₂)}

(F₁:A₁, F₂:(¬A₂

C₂) );

(

u (A₁

_(u) A₂ )_u );

|

(A₃

:=

A₁_(u);

:=

A₂_(u);

:=

mgu

_[u](A₁,A₂ ) )_u );
Unificatie, via substitutie.

(F₁ ·[A₁

:=

A₃]; F₂ ·[A₂

:=

A₃] );

_(u,s) (.., F₃: A₃, F₄: (¬A₃

C₂) );
Lokale atomaire disjunct eliminatie wegens Transferente contradictie (1x).

_(Rd-tc) (.., F₅: C₂ );
Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie (1x).

_(degres
)_(Rd-cj) F₅: C₂ : is geldig.

(1a2)

Weerlegging via 'ontkennende wijs': Modus Tollens (MT).

Via Factief uitgesloten conclusie;
resp. Contrapositie, c.q. Transpositie; resp. (impliciete) Transferente contradictie eliminatie reductie; resp. Conjunctieve reductie.
Eenvoudige vorm.

Bijv.: {¬X, (C

X)}

(¬X

(¬C

X ) );

_(u) (¬X

_(degres
) C : is geldig.
Bijv.: {X, (¬C

¬X)}

¬X ) );

_(u) (X

_(degres
) C : is geldig.

Structuurweergave.

Bijv.: {F₁:¬C₁, F₂: (A₂

C ₂)}

(F₁:¬C₁, F₂:(¬A₂

C₂) );

(

u (C₁

_(u) C₂ )_u );

|

(C₃

:=

C₁_(u);

:=

C₂_(u);

:=

mgu

_[u](C₁,C₂ ) )_u );
Unificatie, via substitutie.

(F₁ ·[C₁

:=

C₃]; F₂ ·[C₂

:=

C₃] );

_(u,s) (.., F₃: ¬C₃, F₄: (¬A₂

C₃) );
Lokale atomaire disjunct eliminatie wegens Transferente contradictie (1x).

_(Rd-tc) (.., F₅: ¬A₂ );
Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie (1x).

_(degres
)_(Rd-cj) F₅: ¬A₂ : is geldig.

16.2.2. Modus ponens, hoofdvormen in PDL.

16.2.2.1. Modus ponens, standaardvorm, in PDL.

Algemene vorm.

Bijv. (PDL, Skl): {F₁:A₁(t₁), F₂:(A₂(t₂)

C₂(t₂)) };

F₁:(A₁(t₁), F₂:(¬A₂(t ₂)

C₂(t₂)) );

(

u1 (A₁(t₁)

_(u1) A₂(t₂) )_u1 );

(u1

|

(

t₃ (1

≤

|

Q

^*(t₃)

|

≤

|

Q

^*(

mgu

_[u](t₁,t ₂) )

|

)_t3 )_u1 );

Unificatie, via substitutie.

(F₁ ·[t₁

:=

t₃]; F₂ ·[t₂

:=

t₃] );

_(u1,s) (.., F₃: A₁(t₃), F₄:(¬A₂(t₃)

C₂(t₃)) );

(t₃

|

(A₁(t₃)

A₂(t₃)) );

F₄ ·[A₂(t₃)

:=

A ₁(t₃)];

_((u,s) (.., F₅:(¬A₁(t₃)

C₂(t₃)) );

Lokale atomaire disjunct eliminatie, wegens Transferente contradictie (1x).

_(Rd-tc) (.., F₆:C₂(t₃) );

Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie(1x).

_(degres
)_(Rd-cj) F₆:C₂(t₃)) : is geldig.

16.2.2.2. Modus ponens, in PDL; Universeel normaal vorm.

D.w.z. met beide premissen universeel.
Het referent en het target element omsluiten elkaar (getalsmatig) (volledig).

Bijv. (PDL): {F₁:(

x A₁(x)), F₂:(

x (A₂(x)

C₂( x))}

(

u (

x (A₁(x)

_(u) A₂(x) )_x )_u );

F₂ ·[(

x A₂( x) )

:=

(

x A₁(x) )];

_(u,s) (.., F₃:(

x (A₁(x)

C₂(x)) );

_(Rd-tc) (.., F₄:(

x C₂(x)) );

_(degres
)_(Rd-cj) F₄:(

x C₂(x) ) : is geldig.

Suboptimaal is:

_(degres
) F₅:C₂(t) : is geldig.

Bijv. (PDL, Skl): {F₁:A₁(x), F₂:(A₂(x)

C₂(x))}

(

u (

x (A₁(x)

_(u) A₂(x) )_x )_u );

F2·[A₂(x)

:=

A₁(x) ];

_(u,s) (.., F₃:(A₁(x)

C₂(x)) );

_(Rd-tc) (.., F₄:C₂(x) );

_(degres
)_(Rd-cj) F₄:C₂(x)) : is geldig.

Suboptimaal is:

_(degres
)_(i) F₅:C₂( t) : is geldig.

16.2.2.3. Modus ponens, in PDL; Existentieel normaal vorm I.

D.w.z. met eerste premisse existentieel, tweede premisse universeel.
Het target element omsluit het referent (getalsmatig).

Bijv. (PDL): {F₁:(

x A₁(x)), F₂:(

x (A₂(x)

C₂( x)))}

F2·[x

:=

y];

_(v) (.., F₃: (

y (A₂(y)

C₂(y))_y) );

Globale E-Kwantor-voorplaatsing c.q. bereikvergroting, (volgordebehoudend), in Conjunctie.
{

x[X]

Y }

_(prenex) (

x[X

Y ] );

_(i) (.., F₄: (

x (A₁(x), (

y (A₂(y)

C₂(y))_y))_x) );

Lokale U-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{

x[X]

y[ Y] }

_(prenex) (

y [X

Y ] );

_(prenex) (.., F₅: (

y (A₁(x), (A₂(y)

C₂(y)))_y,x) );

Lokale E-U Kwantor-samenvoeging, met downgrading, in Conjunctie.

_(Rd-Q) (.., F₆: (

x (A ₁(x), (A₂(x)

C₂(x)))_x) );

(

u (

x (A₁(x)

_(u) A₂(x) )_x )_u );

|

((

x A₁( x) )

_(u) (

x A₂(x) ) )_u );

F6.2·[(

x A₂(x ) )

:=

(

x A₁(x) )];

_(u,s) (.., F₇: (

x (A₁(x), (A₁(x)

C₂(x)))_x) );

Lokale Transferente contradictie eliminatie.

_(Rd-tc) (.., F₈: (

x (A₁(x), C₂(x))_x) );

Lokale E-kwantor splitsing.

_{(dj.samp.xpn.)} (.., F₉: (

x (A₁(x))_x), F₁₀: (

x (C₂(x))_x) );

Globale Conjunctieve reductie.

_(degres
)_(Rd-cj) F₁₀: (

x C₂(x)) : is geldig.

Bijv. (PDL, Skl): {F₁: A₁(

c

_s), F₂: (A₂(x)

C₂(x))}

(

u1 (

x (

c

=

mgu

_[u1](x,

c

_s) )_x )_u1 );

(u1

|

(A₂(x)

A₂(

c

_s) )_u1 );

F2·[x

:=

c

_s];

_(i) (.., F₃: (A₂(

c

_s)

C₂(

c

_s)) );

(

u2 ((A₁(

c

_s) )

_(u2) (A₂(

c

_s) ) )_u2 );

F3·[A₂(

c

_s)

:=

A₁(

c

_s)];

_(u2,s) (.., F₄: (A₂(

c

_s)

C₂(

c

_s)) );

(.., F₅: (¬A₂(

c

_s)

C₂(

c

_s)) );

_(Rd-tc) (.., F₆: C₂(

c

_s) );

_(degres
)_(Rd-cj) F₇: C₂(

c

_s) : is geldig.

16.2.2.4. Modus ponens, in PDL; Existentieel normaal vorm II.

Het referent omsluit het target element (getalsmatig).

Bijv. (PDL): {F₁: (

x A₁(x)), F₂: (

x (A₂(x)

C₂( x)))}

F2·[x

:=

y];

_(v) (.., F₃: (

y (A₂(y)

C₂( y))_y) );

Globale E-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{X

y[Y] }

_(prenex) (

y[X

Y ] );

_(i) (.., F₄: (

y ((A₂(y)

C₂(y)), (

x A₁(x)_x))_y) );

Lokale U-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{

x[X]

y[ Y] }

_(prenex) (

y [X

Y ] );

_(prenex) (.., F₅: (

x ((A₂(y)

C₂(y)), A₁(x) )_x,y) );

Lokale E-U Kwantor-samenvoeging, met downgrading, in Conjunctie.

_(degres
)_(Rd-Q) (.., F₆: (

y ((A₂(y)

C₂( y)), A₁(y) )_y) );

(

u (

x (A₁(x)

_(u) A₂(x) )_x ) )_u );

|

((

x A₁( x) )

_(u) (

x A₂(x) ) ) );

F2·[(

x A₂(x) )

:=

(

x A₁(x) )];

_(u,s) (.., F₇: (

y ((A₁(y)

C₂(y)), A₁(y) )_y) );

Lokale Transferente contradictie eliminatie.

_(Rd-tc) (.., F₈: (

x (C₂(x), A₁(x))_x) );

Lokale E-kwantor splitsing.

_{(dj.samp.xpn.)} (.., F₉: (

x C₂(x)_x), F₁₀: (

y A₁(y) )_y) );

Globale Conjunctieve reductie.

_(degres
)_(Rd-cj) F₉: (

x C₂(x)) : is geldig.

Bijv. (PDL, Skl): {F₁: A₁(x), F₂: (A₂(

c

_s)

C₂(

c

_s)) };

(

u1 (

x (

c

=

mgu

_[u1](x,

c

_s) )_x )_u1 );

(u1

|

(A₁(x)

A₁(

c

_s) )_u1 );

F2·[x

:=

c

_s];

_(i) (.., F₃: A₁(

c

_s ) );

(

u2 (A₁(

c

_s)

_(u2) A₂(

c

_s) )_u2 );

F3·[A₁(

c

_s)

:=

A₂(

c

_s)];

_(u2,s) (.., F₄: (A₂(

c

_s)

C₂(

c

_s)) );

(.., F₅: (¬A₂(

c

_s)

C₂(

c

_s)) );

_(Rd-tc) (.., F₆: C₂(

c

_s) );

_(degres
)_(Rd-cj) F₇: C₂(

c

_s) : is geldig.