AL0PFX1.htm

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).
{F1, F2 } F3.
Conventionele volgorde:
{F2, F1 } F3.

Componenten:


Drie basale proposities).
(1) F1 : formule 1, eerste expliciete basale conjunct term;
nl. basisaanname, factieve premisse (Literaal).
In Conjunctie met:
(2) F2 : formule 2, tweede expliciete basale conjunct term;
nl. afleidingsregel, conditionele premisse (Implicatie).
Levert:
(3) F3 : formule 3, derde expliciete basale conjunct term;
nl. (eind)conclusie, factieve consequens (Literaal).

Lokale syntax:


(F1 : {A1, .. } );
(F2 : {(A2 C2 ) } );
(F3 : {C3 } ).

Elementaire termen:


A1: referent (assumptie, premisse(n) op de baseline).
A2: target element (assumptie, antecedens, premisse(n) binnen F2).

C2: voorwaardelijke conclusie (consequens, binnen F2).
C3: eindconclusie (binnen F3).

Afgeleiden:


A2(A1)

=

(i) A3 : versie van A2 in F2 op grond van A 1; d.w.z., na mgu instantiatie van {A1,A2}.
{mgu: most general unifier, zie definitie in 14.1.2).
C2(A2(A1))

=

(i) C3 : versie van C2 in F 2 volgens A2(A1); d.w.z. valt onder dezelfde kwantificatie (c.q. extensie) als A 2(A1).

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 (¬X C) );   (u) (X (C) );   (

degres

) C : is geldig.
Structuurweergave.
Bijv.: {F1:A1,   F2: (A2   C 2)}
 (F1:A1,   F2:(¬A2   C2) );
 (u (A1   (u) A2 )u );
 (u

|

(A3

:=

A1(u) ;

:=

A2(u);

:=

mgu

[u](A1,A 2 ) )u );
Unificatie, via substitutie.
 (F1 ·[A1

:=

A3]; F2 ·[A2

:=

A3] );
 (u,s) (.., F3: A3, F4: (¬A3   C2) );
Lokale atomaire disjunct eliminatie wegens Transferente contradictie (1x).
 (Rd-tc) (.., F5: C2 );
Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie (1x).
 (

degres

)(Rd-cj) F5: C2 : 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 (C) );   (

degres

) C : is geldig.
Bijv.: {X, (¬C ¬X)}   (X (C ¬X ) );   (u) (X (C) );   (

degres

) C : is geldig.
Structuurweergave.
Bijv.: {F1:¬C1,   F2: (A2   C 2)}
 (F1:¬C1,   F2:(¬A2   C2) );
 (u (C1   (u) C2 )u );
 (u

|

(C3

:=

C1(u) ;

:=

C2(u);

:=

mgu

[u](C1,C 2 ) )u );
Unificatie, via substitutie.
 (F1 ·[C1

:=

C3]; F2 ·[C2

:=

C3] );
 (u,s) (.., F3: ¬C3, F4: (¬A2   C3) );
Lokale atomaire disjunct eliminatie wegens Transferente contradictie (1x).
 (Rd-tc) (.., F5: ¬A2 );
Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie (1x).
 (

degres

)(Rd-cj) F5: ¬A2 : is geldig.

16.2.2.

 

Modus ponens, hoofdvormen in PDL.



16.2.2.1.

 

Modus ponens, standaardvorm, in PDL.


Algemene vorm.
Bijv. (PDL, Skl): {F1:A1(t1), F2:(A2(t2) C2(t2)) };
F1:(A1(t1), F2:(¬A2(t 2) C2(t2)) );
 (u1 (A1(t1)   (u1) A2(t2) )u1 );
 (u1

|

(t3 (1

≤

|

Q

*(t3)

|

≤

|

Q

*(

mgu

[u](t1,t2 ) )

|

)t3 )u1 );
Unificatie, via substitutie.
 (F1 ·[t1

:=

t3 ]; F2 ·[t2

:=

t3] );
(u1,s) (.., F3: A1(t3), F4 :(¬A2(t3) C2(t3)) );
 (t3

|

(A1(t3) A2(t3)) );
 F4 ·[A2(t3)

:=

A 1(t3)];
 ((u,s) (.., F5:(¬A1(t3) C2(t3)) );
Lokale atomaire disjunct eliminatie, wegens Transferente contradictie (1x).
 (Rd-tc) (.., F6:C2(t3) );
Basale atomaire conjunct eliminatie, via globale Conjunctieve reductie(1x).
 (

degres

)(Rd-cj) F6:C2 (t3)) : 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): {F1:(x A1(x)), F2:( x (A2(x) C2(x))}
 (u (x (A 1(x)  (u) A2(x) )x )u );
 F2 ·[(x A2( x) )

:=

(x A1(x) )];
 (u,s) (.., F3:(x (A 1(x) C2(x)) );
 (Rd-tc) (.., F4:(x C2(x)) );
 (

degres

)(Rd-cj) F4:( x C2(x) ) : is geldig.
Suboptimaal is:
 (

degres

) F5:C2(t) : is geldig .

Bijv. (PDL, Skl): {F1:A1(x), F2:(A2(x) C2(x))}
 (u (x (A 1(x)  (u) A2(x) )x )u );
 F2·[A2(x)

:=

A1(x) ];
 (u,s) (.., F3:(A1(x) C2(x)) );
 (Rd-tc) (.., F4:C2(x) );
 (

degres

)(Rd-cj) F4:C2 (x)) : is geldig.
Suboptimaal is:
 (

degres

)(i) F5:C2( 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): {F1:(x A1(x)), F2:( x (A2(x) C2(x)))}
 F2·[x

:=

y];
 (v) (.., F3: (y (A 2(y) C2(y))y) );
Globale E-Kwantor-voorplaatsing c.q. bereikvergroting, (volgordebehoudend), in Conjunctie.
{x[X] Y }     (prenex) (x[X Y ] );
 (i) (.., F4: (x (A 1(x), (y (A2(y) C2(y))y))x) );
Lokale U-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{x[X] y[Y ] }    (prenex) (x y [X Y ] );
 (prenex) (.., F5: ( x y (A1(x), (A2(y) C2(y)))y,x) );
Lokale E-U Kwantor-samenvoeging, met downgrading, in Conjunctie.
(

degres

)(Rd-Q) (.., F6: ( x (A1(x), (A2(x) C2(x))) x) );
 (u (x (A 1(x)  (u) A2(x) )x )u );
 (u

|

((x A1( x) )  (u) (x A2 (x) ) )u );
 F6.2·[(x A2(x) )

:=

(x A1(x) )];
 (u,s) (.., F7: (x (A 1(x), (A1(x) C2(x)))x ) );
Lokale Transferente contradictie eliminatie.
 (Rd-tc) (.., F8: (x (A1(x), C2(x))x) );
Lokale E-kwantor splitsing.
 (dj.samp.xpn.) (.., F9: ( x (A1(x))x), F10: (x (C 2(x))x) );
Globale Conjunctieve reductie.
 (

degres

)(Rd-cj) F10: ( x C2(x)) : is geldig.

Bijv. (PDL, Skl): {F1: A1(

c

s), F2: (A2(x) C2(x))}
 (u1 (x (

c

s

=

mgu

[u1](x,

c

s) )x )u1 );
  (u1

|

 (A2 (x) A2(

c

s) )u1 );
 F2·[x

:=

c

s];
 (i) (.., F3: (A2(

c

s) C2(

c

s)) );
 (u2 ((A1(

c

s ) )  (u2) (A2(

c

s) ) )u2 );
 F3·[A2(

c

s)

:=

A1 (

c

s)];
 (u2,s) (.., F4: (A2(

c

s ) C2(

c

s)) );
 (.., F5: (¬A2(

c

s) C2(

c

s)) );
 (Rd-tc) (.., F6: C2(

c

s ) );
 (

degres

)(Rd-cj) F7: C2 (

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): {F1: (x A1(x)), F2: ( x (A2(x) C2(x)))}
 F2·[x

:=

y];
 (v) (.., F3: ( y (A2(y) C2(y))y) );
Globale E-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{X y[Y] }     (prenex) (y[X Y ] );
 (i) (.., F4: (y ((A 2(y) C2(y)), ( x A1(x)x))y) );
Lokale U-Kwantor-voorplaatsing c.q. bereikvergroting (volgordebehoudend), in Conjunctie.
{x[X] y[Y ] }    (prenex) (x y [X Y ] );
 (prenex) (.., F5: ( y x ((A2(y) C2 (y)), A1(x) )x,y) );
Lokale E-U Kwantor-samenvoeging, met downgrading, in Conjunctie.
(

degres

)(Rd-Q) (.., F6: ( y ((A2(y) C2(y)), A1(y) ) y) );
 (u (x (A 1(x)  (u) A2(x) )x ) )u );
 (u

|

((x A1( x) )  (u) (x A2 (x) ) ) );
 F2·[(x A2(x) )

:=

(x A1(x) )];
 (u,s) (.., F7: (y ((A 1(y) C2(y)), A1(y) )y ) );
Lokale Transferente contradictie eliminatie.
 (Rd-tc) (.., F8: (x (C2(x), A1(x))x) );
Lokale E-kwantor splitsing.
 (dj.samp.xpn.) (.., F9: ( x C2(x)x), F10: (y A1 (y) )y) );
Globale Conjunctieve reductie.
 (

degres

)(Rd-cj) F9: ( x C2(x)) : is geldig.

Bijv. (PDL, Skl): {F1: A1(x), F2: (A2(

c

s) C2(

c

s)) };
 (u1 (x (

c

s

=

mgu

[u1](x,

c

s) )x )u1 );
 (u1

|

 (A1(x) A1(

c

s) )u1 );
 F2·[x

:=

c

s];
 (i) (.., F3: A1(

c

s) );
 (u2 (A1(

c

s )  (u2) A2(

c

s) )u2 );
 F3·[A1(

c

s)

:=

A2 (

c

s)];
 (u2,s) (.., F4: (A2(

c

s ) C2(

c

s)) );
 (.., F5: (¬A2(

c

s) C2(

c

s)) );
 (Rd-tc) (.., F6: C2(

c

s ) );
 (

degres

)(Rd-cj) F7: C2 (

c

s) : is geldig.

C.P. van der Velde © 2004, 2016, 2019.