Kapitel 4 Lukasiewicz Fuzzy-Logik
18. Mai 2005
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Ruckblick
I Tarskis Deduktionsbegriff,
I Verbandstheoretische Grundlagen,
I Verband der [0,1]-wertigen Fuzzy-Mengen.
2(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Uberblick
I Hilbert-Beweissysteme
I Fuzzy-Hilbert-Beweissysteme
I Beweissystem fur FLn
I Abstrakte Fuzzy-Logik
3(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Was ist Logik ?
I primarer Zweck: objektive Gesetze des menschlichen Denkenszu untersuchen,
I Objektivitat: Argumente mussen kommunizierbar undverifizierbar fur andere Menschen sein,
I Zentraler Begriff: Korrektheit eines Schlusses,
I Objektivitat des Denkens und Striktheit des Folgerns undArgumentierens ist verbunden mit Formalisierbarkeit.
4(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Anwendung
I Strikte Trennung von pragmatischen, syntaktischen undsemantischen Aspekten,
I Aussagen bzw. Wissen wird in eine formale Sprache uberfuhrt,
I Semantik ist das Bindeglied zwischen der Welt dermathematischen bzw. realen Objekte und der Welt dersyntaktischen Darstellung,
I Semantik befaßt sich mit der Bedeutung (oder dem Inhalt, derWahrheit oder Gultigkeit)
I Syntax befaßt sich mit der formalen Darstellung.
5(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Logische Kalkule
I Bereitstellung von beschreibendem Wissen in einer formalenSprache fuhrt nicht nur zu weniger Mißvertsandnissen,
I sondern Mechanisierung von menschlichen Schlußweisen wirddadurch moglich(Leibnitz
”ars magna“).
I Zweck logischer Kalkule: Ableitung( Deduktion, Beweis) vonWissen auf rein syntaktischer Ebene,
I logische Kalkule sind eng mit einer Semantik verbunden:Korrektheit: alles, was beweisbar ist, ist wahr,Vollstandigkeit: alles, was wahr ist, ist ableitbar.
6(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Kalkule fur klassische Logik
I formale Sprache: Menge von Formeln uber einem abzahlbarenAlphabet, einer Menge von Junktoren, Konstanten und evtl.Quantoren und Pradikatensymbolen,
I Kalkule des naturlichen Schließens,
I Sequenzen-Kalkule im Gentzen-Stil,
I Beweissysteme im Hilbert-Stil
7(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweissysteme im Hilbert-Stil
I FL-Menge von Formeln,
I Ableitungsregeln,
I logische Axiome.
8(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Ableitungsregeln und Axiome
DefinitionEine k-stellige Ableitungsregel ist eine partielle Abbildungr : F k
L → FL.dom(r) –Definitionsbereich von r .
DefinitionEin Hilbert-Beweissystem ist ein Paar S = (AX ,R), mit AX ⊆ FL
= Menge der logischen Axiome, und R eine Menge vonAbleitungsregeln.
9(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweisbegriff
DefinitionEin Beweis π einer Formel ψ aus einer Menge X ⊆ FL vonFormeln- den echten Axiomen oder Hypothesen- ist eine endlicheFolge von Formeln ϕ1, . . . ϕn mit ϕn = ψ, so daß fur alle ϕi miti ∈ {1, . . . n} gilt:
(i) ϕi ist ein logisches Axiom, d.h. ϕi ∈ AX , oder
(ii) ϕi ist ein echtes Axiom, d.h. ϕi ∈ X , oder
(iii) ϕi ist entstanden durch Anwendung einer Ableitungsregel,d.h. ϕi = r(ϕi1 , . . . ϕik ), wobei ij ∈ {1, . . . n − 1}.
Fur eine gegebene Menge von Formeln X schreiben wir X ` ψ,falls ein Beweis fur ψ aus X existiert.
10(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Deduktionsoperator
DefinitionSei S = (AX ,R) ein Hilbert-Beweissystem. Der zu S gehorendeDeduktionsoperator DS : P(FL) → P(FL) ist definiert durch:
DS(X ) = {ψ ∈ FL : X ` ψ}.
SatzSei DS : P(FL) → P(FL) ein zu einem Hilbertsystem gehorenderDeduktionsoperator. Dann ist DS ein kompakter Abschlußoperator.Umgekehrt gilt: sei D : P(FL) → P(FL) ein kompakterAbschlußoperator. Dann existiert ein Hilbert-Beweissystem S, sd.D = DS .
11(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Theorien
DefinitionSei D : P(FL) → P(FL) ein Abschlußoperator. Ein T ⊆ FL heißtD-Theorie , falls T ein Fixpunkt von D ist, d.h. T = D(T ).
DefinitionT ⊆ FL heißt abgeschlossen unter einer k-stelligen Ableitungsregelr , wenn fur jedes k-Tupel (ϕ1, . . . , ϕk) ∈ dom(r) gilt:
aus ϕ1, . . . , ϕk ∈ T folgt r(ϕ1, . . . , ϕk) ∈ T .
SatzT ⊆ FL ist eine DS-Theorie fur ein Hilbert-Beweissystem S, wenn:
1. T enthalt die Menge AX der logischen Axiome,
2. T ist abgeschlossen unter allen Ableitungsregeln aus R.
12(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Hilbert-Kalkul fur klassische Logik–Axiome
1. ϕ⇒ (ϕ ∧ ϕ)
2. (ψ ∧ ϕ)(ϕ ∧ ψ)
3. (ϕ⇒ ψ) ⇒ ((ϕ ∧ χ) ⇒ (ψ ∧ ϕ))
4. ((ϕ⇒ ψ) ∧ (ψ ⇒ χ)) ⇒ (ϕ⇒ χ)
5. ϕ⇒ (ψ ⇒ ϕ)
6. (ϕ ∧ (ϕ⇒ ψ) ⇒ ψ)
7. ϕ⇒ (ϕ ∨ ψ)
8. (ϕ ∨ ψ) ⇒ (ϕ ∨ ψ)
9. ((ϕ⇒ ψ) ∧ (χ⇒ ψ)) ⇒ ((ϕ ∨ χ) ⇒ ψ)
10. ¬ϕ⇒ (ϕ⇒ ψ)
11. ((ϕ⇒ ψ) ∧ (ϕ⇒ ¬ψ)) ⇒ ¬ϕ12. ¬ϕ ∨ ϕ
13(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Hilbert-Kalkul fur klassische Logik
I Axiome sind anwendbar auf alle Formeln, die Instanzen derAxiome sind,
I einzige Ableitungsregel ist die Abtrennungsregel:
ϕ,ϕ⇒ ψ
ψ
14(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Kurzer Hilbert-Kalkul fur klassische Logik
Alphabet enthalt nur die Junktoren ⇒ und ¬A1 ϕ⇒ (ψ ⇒ ϕ)
A2 (ϕ⇒ (ψ ⇒ χ)) ⇒ ((ϕ⇒ ψ) ⇒ (ϕ⇒ χ))
A3 (¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ)
rMP (ϕ,ϕ⇒ ψ) 7→ ψ
zusatzliche Junktoren werden als verkurzte Schreibweiseneingefuhrt:
ϕ ∧ ψ ≡ ¬(ϕ⇒ ¬ψ)ϕ ∨ ψ ≡ ¬ϕ⇒ ψ
⊥ ≡ ¬(ϕ⇒ ϕ)
15(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beispiel
Beweisziel: ∅ ` ¬ψ ⇒ (ψ ⇒ ϕ)
1. ¬ψ ⇒ (¬ϕ⇒ ¬ψ) A12. (¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ) A33. ((¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ)) ⇒
(¬ψ ⇒ ((¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ))) A14. ¬ψ ⇒ ((¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ)) rMP , 2., 3.5. (¬ψ ⇒ ((¬ϕ⇒ ¬ψ) ⇒ (ψ ⇒ ϕ))) ⇒
((¬ψ ⇒ (¬ϕ⇒ ¬ψ)) ⇒ (¬ψ ⇒ (ψ ⇒ ϕ))) A26. (¬ψ ⇒ (¬ϕ⇒ ¬ψ)) ⇒ (¬ψ ⇒ (ψ ⇒ ϕ)) rMP , 4., 5.7. ¬ψ ⇒ (ψ ⇒ ϕ) rMP , 1., 6.
16(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Fuzzy-Ableitungsregeln
Ziel:formales System, mit Hilfe dessen aus einer Fuzzy-Menge von Pramissen eine Fuzzy-Menge von Kon-klusionen abgeleitet werden kann.
Definition
Eine Fuzzy-Ableitungsregel r = (r ′, r ′′) ist ein Paar von k-stelligenOperationen mit:
r ′ : D → FL wobei D ⊆ F kL und
r ′′ : [0, 1]k → [0, 1] so, daß
r ′′(a1, . . . , aj = supi∈I
bi , . . . , ak) = supi∈I
r ′′(a1, . . . , bi , . . . , ak)
fur jeden Index 1 ≤ j ≤ k.
17(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Fuzzy-Ableitungsregeln II
I die Bedingung sichert die Stetigkeit,
I Darstellung von Fuzzy-Ableitungsregeln:
ϕ1, . . . , ϕk
r ′(ϕ1, . . . , ϕk)
a1, . . . , ak
r ′′(a1, . . . , ak)
I Wenn die Formeln ϕ1, . . . , ϕk zum Grad a1, . . . , ak gegebensind,dann konnen wir folgern, daß die Formel r ′(ϕ1, . . . , ϕk)mindestens zum Grad r ′′(a1, . . . , ak) gelten muß.
18(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Fuzzy-Beweissystem im Hilbert-Stil
LAX ∈ F(FL) –Fuzzy-Menge der logischen Axiome
Definition
Ein Fuzzy-Beweissystem im Hilbert-Stil ist ein Paar S = (LAX ,R),bestehend aus LAX ⊆ FL einer Fuzzy-Menge von logischen Axiomenund einer Menge R von Fuzzy-Inferenzregeln.
19(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweise
Definition
Sei S = (LAX ,R) ein Fuzzy-Hilbert-Beweissystem.Sei u ∈ F(FL) eine Fuzzy-Menge (von Hypothesen).Ein Beweis π fur einer Formel ψ aus u ist eine endliche Folge vonFormeln ϕ1, . . . ϕn mit ϕn = ψ, zusammen mit einer Menge von
”Rechtfertigungen“. Das bedeutet fur eine gegebene Formel ϕi wird
gekennzeichnet, ob:
(i) ϕi als logisches Axiom,
(ii) ϕi wird als echtes Axiom, oder
(iii) ϕi als Ergebnis der Anwendung einer Fuzzy-Ableitungsregel,d.h. ϕi = r ′(ϕi1 , . . . ϕik ), wobei ij ∈ {1, . . . n − 1}, betrachtetwird.
Es existieren immer genau zwei Beweise der Lange 1.20(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Bewertung der Beweise
u ∈ F(FL), die Bewertung val(π, u) von π in bezug auf u istinduktiv uber die Lange m von π definiert:
- Falls m = 1, dann ist
val(π, u) =
{LAX (ϕ1) betrachte ϕ1 als log. Axiom,
u(ϕ1) betrachte ϕ1 als echtes Axiom.
- Andernfalls ist
val(π, u) =
LAX (ϕm) betrachte ϕm als log. Axiom,
u(ϕm) betrachte ϕm als echtes Axiom,
r ′′(val(πi1 , u), . . . val(πik , u)) falls B
B: ϕm = r ′(ϕi1 , . . . , ϕik ), wobei ij ∈ {1, . . . n − 1}.
21(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Bewertung der Beweise
I Interpretation: Bei gegebener Information u, sichert der Beweisπ, daß die Formel ψ mindestens zum Grad val(π, u)gilt.
I fur eine Formel ψ kann ein zweiter Beweis π′ existieren, mitval(π′, u) ≥ val(π, u),
I um den Grad der Gultigkeit einer Formel ψ bei gegebenerAnfangsbelegung u zu berechnen,mussen alle Beweise fur ψberucksichtigt werden.
Definition
S = (LAX ,R)–Fuzzy-H-System, u ∈ F(FL), ψ ∈ FL.
DS(u)(ψ) = sup{val(π, u) | π ist ein Beweis fur ψ}
DS(u)(ψ) ist die bestmogliche Bewertung fur ψ, die wir aus derAnfangsbelegung u ableiten konnen.
22(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Lukasiewicz-Fuzzy-Logik FLn
I benannt nach dem polnischen Mathematiker Jan Lukasiewicz,der 1915 dreiwertigen Logikkalkul entwarf
I Sei L ein Alphabet, das eine abzahlbare Menge VAR vonVariablen, eine Menge von Symbolen {¬,→,∧,∨,&} fur dieJunktoren, sowie fur jede rationale Zahl q ∈ (Q ∩ [0, 1]) einelogische Konstante q enthalt.
I Formelmenge FL uber L ist dann wie gewohnlich induktivdefiniert.
23(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Axiomatisierung von FLn
Bezeichnungen:
λ1(ϕ, χ, ψ) = ϕ→ (φ→ ϕ)λ2(ϕ, χ, ψ) = (ϕ→ ψ) → ((ψ → χ) → (ϕ→ χ))λ3(ϕ, χ, ψ) = (¬ϕ→ ¬ψ) → (ψ → ϕ)λ4(ϕ, χ, ψ) = ((ϕ→ ψ) → ψ) → ((ψ → ϕ) → ϕ)
LAX (φ) =
a falls φ = a,
1− a falls φ = ¬a,
1 falls φ = λi (ϕ, χ, ψ), i ∈ {1, ..4}, ϕ, χ, ψ ∈ FL,
0 sonst.
rMP = (r ′MP , r′′MP) :
ϕ,ϕ→ ψ
ψ,
a, b
max{0, a + b − 1}24(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Heap-Paradoxon
I 100000 Sandkornchen bildet einen Haufen,
I Wenn ich von einem Haufen ein Sandkornchen wegnehme,habe ich immer noch einen Sandhaufen ubrig.
I Ergebnis nach Iteration dieses Schlusses: Eine Menge von 0Sandkornchen ist ein Sandhaufen.
25(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Heap-Paradoxon
fur jedes n, 0 ≤ n ≤ 100.000}{H(n)}: n Sandkornchen sind Haufen.{H(n) → H(n − 1)}: Wenn n Sandkornchen einen Haufen
bilden, dann bilden n − 1 Sandkornchenebenfalls einen Haufen.
Anfangsbelegung u:
u(ϕ) =
1 falls ϕ = H(100000),
0.99999 falls ϕ = H(n) → H(n − 1), n ∈ {1, . . . , 100.000}0 sonst.
26(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweise der Lange 1
π1 = H(99999)(Logisches Axiom).π2 = H(99999)(Echtes Axiom).
Bewertungen der Beweise:
Val(π1, u) =LAX (H(99999)) = u(H(99999)) = Val(π2, u) = 0.
27(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweise der Lange 3
π3 = H(100000) (Echtes Axiom),H(100000) → H(99999) (Echtes Axiom),H(99999) = r ′MP(H(100000),H(99999)) (Modus Ponens).
val(π3) = r ′′MP(val(π31), val(π3
2))= r ′′MP(u(H(100000)), u(H(100000) → H(99999)))= max{0, 1 + 0.99999− 1}= 0.99999
28(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweise der Lange 3 fortgesetzt
π4 = H(100000) (Logisches Axiom),H(100000) → H(99999) (Echtes Axiom),H(99999) = r ′MP(H(100000),H(99999)) (Modus Ponens).
val(π4) = r ′′MP(val(π41), val(π4
2))= r ′′MP(LAX (H(100000)), u(H(100000) → H(99999)))= max{0, 0 + 0.99999− 1}= 0
29(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Beweise der Lange 3 fortgesetzt
π5 = H(100000) (Echtes Axiom),H(100000) → H(99999) (Logisches Axiom),H(99999) = r ′MP(H(100000),H(99999)) (Modus Ponens).
val(π5) = r ′′MP(val(π51), val(π5
2))= r ′′MP(u(H(100000)), LAX (H(100000) → H(99999)))= max{0, 1 + 0− 1}= 0
30(31)
Ruckblick und Uberblick Hilbert-Beweissysteme Fuzzy-Hilbert-Beweissysteme Beweissystem fur FLn
Auswertung Heap-Paradoxon
I großte untere Schranke fur den Wert der Beweise furH(99999) ist hier 0.99999, d.h.Dluk(u)(H(99999)) = 0.99999.
I es existiert ein k ∈ N, so daß Dluk(H(k)) = 0. Fur unsereAnfangsbelegung u ist k = 1; ein einzelnes Sandkorn istSandhaufen zum Grad 0,
I Fuzzy-Logik ist geeignet, klassische Paradoxien aufzulosen.
31(31)
Top Related