Logische Äquivalenz
        
                        
                                                                                    
                                                                                            Definition 2.7 [Logische Äquivalenz]  | 
                                                                                 
                                                                                            
                                                                                            Zwei Formeln φ, ψ ∈ FO(S) heißen (logisch) äquivalent, gdw. für alle S-Interpretationen J gilt: J |= φ gdw. J |=ψ. In Symbolen: φ≡ψ.  | 
                                                                                 
                                                                         
                            Bem.: Logische Äquivalenzen der AL übertragen sich auf FO. Hinzu treten charakteristische logische Äquivalenzen im Zusammenhang mit Quantoren. 
 
Z.B. die Dualität zwischen ∀ und ∃, die besagt dass für alle φ ∈ FO(S):  
 
∃xφ ≡ ¬∀x¬φ, 
∀xφ ≡ ¬∃x¬φ.  
                             
    
    
            Erfüllbarkeitsäquivalenz
        
                        
                                                                                    
                                                                                            Definition 2.10 Erfüllbarkeitsäquivalenz  | 
                                                                                 
                                                                                            
                                                                                            Formeln φ,φ′ heißen erfülbarkeitsäquivalent wenn gilt: φ erfüllbar gdw. φ′ erfülbar. Analog wird Erfüllbarkeitsäquivalenz für Formelmengen definiert.  | 
                                                                                 
                                                                         
                             
    
    
            Signaturen
        
                        
                                    
                        Eine Signatur S ist eine Menge von Konstanten-, Funktions- und Relationssymbolen, mit angegebenen Stelligkeiten. Spezialfa ̈lle: S ohne Funktionssymbole : relationale Signatur; S ohne Relationssymbole : funktionale Signatur.  | 
                     
                             
                             
    
    
            S-Strukturen
        
                        
                                                                                    
                                                                                            Definition 1.1 [S-Strukturen]  | 
                                                                                 
                                                                                            
                                                                                            Für Signatur S: Eine S-Struktur A = (A,cA,...,fA,...,RA,...) besteht aus ihrer Trägermenge A ≠ ∅ zusammen mit einer Interpretation der Symbole in S, d.h., für jedes Konstantensymbol c ∈ S: ein ausgezeichnetes Element cA ∈ A. für jedes n-stellige Funktionssymbol f ∈ S: eine n-stellige Funktion fA : An→ A. für jedes n-stellige Relationssymbol R ∈ S: eine n-stellige Relation RA ⊆ An.  | 
                                                                                 
                                                                         
                             
    
    
            S-Terme
        
                        
                                    
                        Definition 1.3 [S-Terme] Die Menge der S-Terme, T(S) (mit Variablenmenge V) ist induktiv erzeugt wie folgt: 
• x∈T(S) für jede Variable x ∈ V. 
• c ∈ T(S) für jedes Konstantensymbol c ∈ S. 
• ist f ∈ S ein n-stelliges Funktionssymbol, und sind t 1
 , . . . , t n
  ∈ T (S), so ist auch ft 1
 ...t n
  ∈T(S).
 
T n
 (S) ⊆ T(S): die Mengen der Terme, in denen nur Variablensymbole aus V n
  = {x 1
 , . . . , x n
 } vorkommen.
 Speziell steht  T0 (S) für die Menge der Variablen-freien Terme (= ∅ wenn S keine Konstanten hat).   | 
                     
                             
                             
    
    
            Allgemeingültigkeit
        
                        
                                                                                    
                                                                                            Definition 2.6 [Allgemeingültigkeit]  | 
                                                                                 
                                                                                            
                                                                                            Eine Formel φ ∈ FO(S) heißt allgemeingültig gdw. für alle S-Interpretationen J gilt: J |= φ.  | 
                                                                                 
                                                                         
                             
                             | 
                                                                              | 
                                                        
                                
    
    
            Folgerungsbeziehung
        
                        
                                                                                    
                                                                                            Definition 2.5 [Folgerungsbeziehung]  | 
                                                                                 
                                                                                            
                                                                                            φ |= ψ bzw. Φ |= ψ.  | 
                                                                                 
                                                                         
                            Für φ,ψ ∈ FO(S): 
ψ ist eine logische Folgerung von φ, oder ψ folgt aus φ, in Symbolen φ |= ψ, gdw. für alle S-Interpretationen J gilt: J |= φ ⇒ J |= ψ. 
 
Entsprechend ist Φ |= ψ für Formelmengen Φ definiert (ψ folgt aus Φ).  
                             
    
    
            FO mit und ohne Gleichheit
        
                        
                                                                                    
                                                                                            Definition 2.11 [FO ohne Gleichheit]  | 
                                                                                 
                                                                                            
                                                                                            FO≠(S) ⊆ FO(S) ist aufgebaut wie FO aber ohne Termgleichheiten als atomare Formeln. Die Semantik von FO überträgt sich auf die Teillogik FO≠.  | 
                                                                                 
                                                                                            
                                                                                            Bemerkung 2.13 Zu jeder Formelmenge Φ ⊆ FO(S) erhält man durch eine systematische Übersetzung in eine explizite Modellierung der Gleichheitsrelation durch eine neues Relationssysmbol ∼ eine erfülbarkeitsäquivalente Formelmenge Φ ∼
   ⊆ F0 ≠(S ∪ {∼}).   | 
                                                                                 
                                                                         
                             
    
    
            Termstruktur
        
                        
                                                                                    
                                                                                            Defintion 1.4 Termstrukturen  | 
                                                                                 
                                                                                            
                                                                                            Die Menge der S-Terme ist Träger einer S F
 -Struktur T = T (S), der Termstruktur ( Herbrand-Struktur) zu S, mit der folgenden natürlichen Interpretation der Konstanten- und Funktionssymbole in S:  | 
                                                                                 
                                                                         
                            • für Konstantensymbol c ∈ S:  
c T := c ∈ T(S). 
• für n-stelliges Funktionssymbol f ∈ S: f  T: T(S) n  → T(S) 
(t 1
 ,...,t n
 )  → ft 1
  ...t n
 . 
Wenn S Konstantensymbole hat, ist auch T 0
 (S) Träger einer entsprechenden Termstruktur T 0
 (S) (eine Substruktur von T (S)).  
                             
    
    
            Pränexe Normalform
        
                        
                                                                                    
                                                                                            Definition 3.1 [pränexe NF] FO-Formeln in pränexer Normalform sind von der Form Q 1
 x i
 1
  ...Q k
 x ik
  ψ, wo k ∈ N, Q i
  ∈ {∀, ∃} und ψ  quantorenfrei. ψ heißt auch quantorenfreier Kern der Formel, Q 1
 x i1
  . . . Q k
  x i
 k
  ihr Quantorenpräfix.   | 
                                                                                 
                                                                                            
                                                                                            Man braucht i.d.R. zusätzliche Variablensymbole!  | 
                                                                                 
                                                                                            
                                                                                            Satz 3.4 Jede FO-Formel ist  äquivalent zu einer Formel in pränexer NF.  | 
                                                                                 
                                                                         
                            Beispiel 3.2 S = {E}, E 2-st. Relations-Symbol. Die folgenden Äquivalenzen liefern auf der rechten Seite pränexe Formalisierungen:  
∃y(Exy ∧ ∀x(Eyx → x = y)) ≡ ∃y∀z Exy ∧ (Eyz → z = y) ,  
∃y∀xExy ∨ ¬∃yExy ≡ ∃y1∀y2∀y3 Ey2y1 ∨ ¬Exy3 .  
                             
                             | 
                                                                              | 
                                                        
                                
    
    
            Belegungen
        
                        
                                    
                        Definition 1.5 
[Belegungen und Interpretationen]
Eine Funktion β: V → A heißt Belegung (für die x ∈ V) in der S-Struktur A = (A,...). Eine S-Struktur A und Belegung β zusammen bilden eine S-Interpretation J = (A, β).
 
•Für t = x ( x ∈ V Variable): 
 t J:=β(x). 
• Für t = c ( c ∈ S Konstantensymbol): 
 t J:= c A. 
• Für t = ft 1
  ...t n
 , mit n-stelligem Funktionssymbol f ∈ S: 
 t J := f A (t 1 J,...,t n J ).   | 
                     
                             
                            Schreibweisen für Belegungen und Interpretationen auf Seite 6 FO Skript über Kapitel 2  
                             
    
    
            Freie Variablen
        
                        
                                                                                    
                                                                                            Definition 2.2 [freie Variablen]  | 
                                                                                 
                                                                                            
                                                                                            Induktive Definition der Menge der freien Variablen, frei(φ) ⊆ V, für φ ∈ FO(S):  | 
                                                                                 
                                                                                            
                                                                                            Formeln ohne freie Variablen heißen Sätze.  | 
                                                                                 
                                                                                            
                                                                                            Schreibweisen: FO n
 (S) := {φ ∈ FO(S): frei(φ) ⊆ V n
 }. Für φ ∈ FO n
 (S) schreiben wir auch φ = φ(x 1
 , . . . , x  n
 ) um die möglicherweise freien Variablen explizit anzudeuten.   | 
                                                                                 
                                                                         
                            frei(t 1
  = t 2
 ) := var(t 1
 ) ∪ var(t 2
 ).  
frei(Rt 1
  . . . t  n
 ) := var(t 1
 ) ∪ . . . ∪ var(t  n
 ). 
frei(¬φ) := frei(φ).  
frei(φ ∧ ψ) = frei(φ ∨ ψ) := frei(φ) ∪ frei(ψ). 
frei(∃xφ) = frei(∀xφ) := frei(φ) \ {x}.  
                             
    
    
            Quantorenrang
        
                        
                                                                                    
                                                                                            Definition 2.3 [Quantorenrang]  | 
                                                                                 
                                                                                            
                                                                                            Induktive Definition des Quantorenrangs, qr(φ) ∈ N, für φ ∈ FO(S):  | 
                                                                                 
                                                                                            
                                                                                            Formeln von Quantorenrang 0 heißen quantorenfrei.  | 
                                                                                 
                                                                         
                            qr(φ) = 0 für atomares φ. 
qr(¬φ) := qr(φ). 
qr(φ ∧ ψ) = qr(φ ∨ ψ) := max(qr(φ), qr(ψ)).  
qr(∃xφ) = qr(∀xφ) := qr(φ) + 1.  
                             
    
    
            Semantik
        
                        
                                                                                    
                                                                                            Definition 2.4 [Semantik]  | 
                                                                                 
                                                                                            
                                                                                            Für S-Interpretation J = (A, β) und φ ∈ FO(S): J erfüllt φ gdw. φ J = 1. Schreibweise: J|= φ.  | 
                                                                                 
                                                                                            
                                                                                            Für Formelmengen Φ ⊆ AL(V) entsprechend:  J|= Φ gdw. J |= φ für alle φ ∈ Φ.  | 
                                                                                 
                                                                                            
                                                                                            Die Relation |= heißt Modellbeziehung.  | 
                                                                                 
                                                                         
                             
    
    
            Herbrand
        
                        
                                                                                    
                                                                                            Satz 3.10 (Herbrand)  | 
                                                                                 
                                                                                            
                                                                                            Sei Φ ⊆ FO 0
 ≠ (S) eine Menge von universellen, gleichheitsfreien Sätzen. Dann sind äquivalent:  | 
                                                                                 
                                                                                            
                                                                                            (i) Φ erfüllbar.  | 
                                                                                 
                                                                                            
                                                                                            (ii)  Φ hat ein Herbrand-Modell  H =  ( T0 (S), (RH)R ∈S ) |= Φ, dessen Trägermenge und Funktions- und Konstanteninterpretationen mit der Termstruktur T 0
 (S) übereinstimmen (H erweitert die S F
 -Struktur T 0
 (S) lediglich um eine geeignete Interpretation der Relationssymbole in S).   | 
                                                                                 
                                                                                            
                                                                                            Definition 3.8 Eine Formel ist universell wenn sie aus atomaren und negiert atomaren Formeln allein mittels ∧, ∨ und ∀-Quantoren aufgebaut ist.  | 
                                                                                 
                                                                                            
                                                                                            Lemma 3.12 Sei Φ ⊆ FO 0
 ≠ (S) eine Menge von universell-pränexen Sätzen. Dann sind  äquivalent:   | 
                                                                                 
                                                                                            
                                                                                            (i) Φ erfüllbar. (ii) [[Φ]]AL erfüllbar.  | 
                                                                                 
                                                                         
                             
                             | 
                                                                              | 
                                                        
                                
    
    
            Erfülbarkeit
        
                        
                                                                                    
                                                                                            • Φ ⊆ FO 0
 (S) eine Satzmenge (ohne freie Variablen) ist. Man erhält eine zu einer Formelmenge erfüllbarkeitsäquivalente Satzmenge, indem man neue Konstantensymbole für alle freien Variablen substituiert  | 
                                                                                 
                                                                                            
                                                                                            • Φ ⊆ FO 0
 ≠ (S) gleichheitsfrei ist. Eine explizite Modellierung der Gleichheitsrelation durch eine zusätzliche Äquivalenzrelation (siehe Bemerkung 2.13) führt zu erfüllbarkeitsäquivalenten Satzmengen ohne Gleichheit.  | 
                                                                                 
                                                                                            
                                                                                            • Φ ⊆ FO 0
 ≠ (S) aus universell-pränexen, gleichheitsfreien Sätzen besteht. Skolemisierung liefert eine erfüllbarkeitsäquivalente Satzmenge in universell-pränexer Form.  | 
                                                                                 
                                                                                            
                                                                                            • S mindestens ein Konstantensymbol enthält, sodass T 0
 (S) ≠ ∅ ist, und wir uns ggf. auf Herbrand-Modelle von Φ ⊆ FO 0
 ≠ (S) zurückziehen können.  | 
                                                                                 
                                                                         
                            Φ erfüllbar ⇔ H |= Φ für eine 
                        Herbrand-Struktur H =  T 0
 (S),(R H) R
 ∈ S
  .  
                             
    
    
            Kompaktheitssatz (FO)
        
                        
                                                                                    
                                                                                            Satz 4.1 (Kompaktheitssatz) Für jede Formelmenge Φ ⊆ FO sind  äquivalent:  | 
                                                                                 
                                                                                            
                                                                                            (i) Φ erfüllbar. (ii) Jede endliche Teilemenge Φ 0
  ⊆ Φ ist erfüllbar.  | 
                                                                                 
                                                                                            
                                                                                            Korollar 4.2 Für jede Formelmenge Φ ⊆ FO und Formel ψ ∈ FO sind  äquivalent:  | 
                                                                                 
                                                                                            
                                                                                            (i) Φ |= ψ.  (ii) Es existiert eine endliche Teilemenge Φ 0
  ⊆ Φ, sodass Φ 0
  |= ψ.   | 
                                                                                 
                                                                                            
                                                                                            Das Korollar folgt aus dem Satz über den Zusammenhang: Φ|=φ gdw. Φ ∪ {¬φ} unerfüllbar.  | 
                                                                                 
                                                                         
                             
                             | 
                                                            
            
Created By
Metadata
Comments
No comments yet. Add yours below!
Add a Comment
More Cheat Sheets by tiziano123