Cursus / training: Methode Formele Logica
©
18.
Kwantor-bewerkingen; met semantische expansie.
Kwantor upgrading: Upgrading van kwantificaties.
18.1.
U-Kwantor upgrading.
Kwantor- upgrading: Universeel.
(N.v.t.)
18.2. E-Kwantor upgrading.
Kwantor- upgrading: Existentieel.
Algemeen:
'  '  (degres) ' 
' : is ongeldig.
Toepasbaar in Literaal, Conjunctie, Disjunctie.
Equivalentie/ Parafrase: nooit valide.
Implicatie/ Degressie: nooit valide.
(1) In Literaal (atoom/predicatie).
Via operatie: conjuncte expansie.
{ y x A( x, y)} 
(degres)(cj.xpn.) ( x
y A( x, y)) : ongeldig.
{ x y A( x, y)}
(degres)(cj.xpn.) ( x
y A( x, y)) : ongeldig.
(2) In Conjunctie.
Tweede term, met Kwantor-volgordeverandering.
{ y x (A( x) 
B( y))} (degres)(dj.rdc.;cj.xpn.) (
x w (A( x) B( w))) :
ongeldig.
{ y x
z (A( y) C_( x, z))}
(degres)(dj.-cj.xpn.) ( y
x z (A( y) C_( x, z
))) : ongeldig.
Tweede term, met Kwantorsplitsing.
{ y (A( y) B( y))}
(degres)(dj.-cj.xpn.) ( y
x (A( x) B( y))) : ongeldig.
Beide termen.
{ x (A( x) (
y C_( x, y)))}; (degres)(dj.-cj.xpn.)
( x (A( x) (
y C_( x, y)))) : ongeldig.
(3) In Disjunctie.
Tweede term.
{( x A( x))  (
y B( y))} (degres)(dj.-cj.xpn.) (
x w (A( x) B( w))) :
ongeldig.
Beide termen.
{ y (A( y) B( y))}
(degres)(dj.-cj.xpn.) ( x (A( x)
B( x))) : ongeldig.
Eerste term.
{ x (A( x) (
y B( y)))} (degres)(dj.-cj.xpn.) (
x (A( x) ( y B( y)))) :
ongeldig.
19. Wetten voor logische strijdigheid
(contradictie).
19A.
Directe 'fatale' strijdigheid (in CNF
).
19A.1.
Directe, 'fatale', interne enkelvoudige strijdigheid.
Directe ' Basale contradictie' ( unit conflict).
[Wet in PPL: {p ¬p} ≡ (u) p. ]
[Wet in PPL: {p ¬p & q} ≡ (u) $
0 q; ≡ $0. ]
Zie ook PPL wetten (7.6).
19B. Indirecte 'fatale' strijdigheid.
19B.1.
Impliciete Basale Conjunct Contradictie (in CNF
).
Indirecte ' Basale contradictie'.
Graduele onjuistheid - 'horizontaal'.
In PDL ( Skolem).
(19B.1a) Partieel Exclusief Disjunctie; Met existentieel Negatieve predicatie/Literaal.
Bijv.: {A( x) ¬A( cd) };
( cd is een (bestaande) ' domein' constante).
Route 1.
 (xts.) ({A(x [1]) .., A(x [i]
) .., A(x [n])} ¬A( cd));
i (A(x [i])·[x
[i] := cd] );
(sbs.) ({A(x [1]) .., A(x [c
d]) .., A(x [n]) } ¬A( c
d) );
(bas.cj.rei.) ({A(x [1]) .., A(x [
cd]) .., A(x [n]) } A(
cd) ¬A( cd) );
(its.) (A( x) A( c
d) ¬A( cd) );
(u,bas.ctd) (A( x) ( $
0) );
('¬A( cd)' is tegenvoorbeeld ( contra-indicatie, falsificator) voor algemene regel
'A( x)' ).
Route 2.
(bas.cj.rei.) (A( x) A(
cd) ¬A( cd) );
(u,bas.ctd.) (A( x) $
0 );
Route 3.
· [ x:= cd]
(i) (A( cd) ¬A( cd));
$0.
Idem, genoteerd ( isomorf) in PPL:
(iso) ((A 1, A 2, A 3,
.. ) (¬A 1/ ¬A 2/ ¬A 3/ .. ) );
(A 1, A 2, A 3, .. , (¬A 1
/ ¬A 2/ ¬A 3/ .. ) );
(trf.ctd.1) (A 1, A 2, A 3, ..
, (¬A 1/ ¬A 2/ .. ) );
(trf.ctd.2) (A 1, A 2, A 3, ..
, (¬A 1/ .. ) );
..
(trf.ctd. (n-1)) (A 1, A 2, A 3,
.. , ¬A 1 );
(bas.ctd.1) ( $0, A 2, A 3,
.. );
(bas.ctd. 2..n) $0.
(19B.1b) Partieel Exclusief Disjunctie; Met universeel Negatieve predicatie/Literaal:
Bijv.: {A( cd) ¬A( x) };
( cd is een (bestaande) ' domein' constante).
Route 1.
(xts.) ({¬A(x [1]) .., ¬A(x [i]
) .., ¬A(x [n])} A( cd));
i (A(x [i]·[x
[i] := cd] );
(sbs.) ({¬A(x [1]) ..
¬A( cd) .. ¬A(x [n])}
A( cd) );
(bas.cj.rei.) ({¬A(x [1]) .., ¬A(x [i
]) .., ¬A(x [n]) } ¬A( c
d) A( cd) );
(its.) (¬A( x) ¬A( c
d) A( cd) );
(u,bas.ctd.) (¬A( x) (
$0) );
('A( cd)' is tegenvoorbeeld ( contra-indicatie, falsificator) voor algemene regel '¬A(
x)').
Route 2.
(U-intro) ((( x ¬A( x) )
A( cd) );
(Mits de formule staat in normaal vorm).
(bas.cj.rei.) (( x ¬A( x
) ) ¬A( cd) A( c
d) );
(u,bas.ctd.) (( x ¬A( x) )
$0 );
(U-elim.) (A( x) $
0 );
$0.
Idem, genoteerd ( isomorf) in PPL:
(iso) ((¬A 1, ¬A 2, ¬A 3
, .. ) (A 1/ A 2/ A 3/ .. ) );
(¬A 1, ¬A 2, ¬A 3, .. , (A 1
/ A 2/ A 3/ .. ) );
(trf.ctd.1) (¬A 1, ¬A 2, ¬A 3, ..
, (A 1/ A 2/ .. ) );
(trf.ctd.2) (¬A 1, ¬A 2, ¬A 3, ..
, (A 1/ .. ) );
..
(trf.ctd. (n-1)) (¬A 1, ¬A 2, ¬A 3
, .. , A 1 );
(bas.ctd.1) $0, ¬A 2, ¬A 3,
.. );
(bas.ctd. 2..n) $0.
19B.2. Factief uitgesloten conclusie.
Factief uitgesloten conclusie;
met enkelvoudige ( disjuncte) premisse, en (deels) ware referent-premisse.
Bijv.: {((A( x) B( x)) ¬B( c
d) ) A( dd) }
(((¬A( x) B( x))
A( dd) ¬B( cd) );
(u,trf.ctd.) (¬A( x) A(
dd) ¬B( cd) );
(u,bas.ctd.) ( $0 ¬B(
cd));
(bas.ctd.) $0.
C.P. van der Velde © 2004, 2016, 2019.
|
|