skip to main content

kiesler.at
PraedikatenLogik
Back to Page | Back to History

Difference between revisions

Version 1, 2005-03-12 22:05 Version 2, 2005-03-12 22:13
Lines 112 - 114 Lines 112 - 186
++++ Beispiel ++++ Beispiel
   
[brother] { ( Charles, Edward), ( Charles, Andrew) , (Edward, Andrew) } teilmenge_von U x U [brother] { ( Charles, Edward), ( Charles, Andrew) , (Edward, Andrew) } teilmenge_von U x U
   
   
  +++ Terme
   
  V = Menge von Variablen
   
  Terme: rekursiv / induktiv definiert
   
  (1) x, falls x (- V
   
  * jede Variable ist ein Term
   
  (2) c, falls c (- Func und c hat Stelligkeit 0
   
  * jede Konstante ist kein Term
   
  (3) f(t1, ..., tn) falls f (- Func mit Stelligkeit n>0 und t1, ..., tn Terme
   
  * Induktionsschritt.
   
   
  +++ Variablenbelegung
   
  alpha: V -> U
   
  2 Parameter:
  * Signatur
  * Variablenmenge (Wert aus Domain, Interpretationsfrage)
   
   
  +++ Termausweitung
   
  Termauswertung eines Terms t in einer Interpretation I unter einer Variablenbelegung:
   
  |[t]|_{ I,alpha } (- U
   
  ist definiert durch
   
  |[x]|_{ I, alpha } = alpha(x)
   
  |[f(t1, ..., tn) ]|_{ I, alpha } = f_I(|[t_1]|_t{I, alpha}, ..., |[t_n]|_{ I, alpha }
   
  Interpretation stark von Termdefinition abhängig!
   
  Für die Terme, Interpretation udn endlichen Term //terminiert// diese Auswertung (später mehr)!
   
  Gilt für allgemeine Formeln nicht (im Wesentlichen wegen alpha).
   
  I und alpha richtig wählen ist Herausforderung, der Rest ist sehr einfach.
   
  * atomare Formeln P(t1, ..., tn)
  * komplexere Forlemn mit Junkoren (NOT, AND, OR, =>, <=>)
  * quantifizierte Formeln mit Quantoren und Variablen.
   
   
  FORALL xF "Für alle x gilt F" (Allquantor)
  EXISTS xF "Es gibt ein x, sodass F gilt" (Existenz-Quantor)
   
   
  * FORALL x Mensch (x) => sterblich (x)
  * NOT NOT sterblich (Sokrates) .... Doppelnegationselimination
  * EXISTS x Großvater (x, Sokrates)
  * FORALL x Großvater(Vater_von((Mutter_von(x)), x)
  * NOT prim (3)
  * FORALL x EXISTS y prim(y) AND x < y .... Für jede Zahl x gibt es eine größere Primzahl.
   
  Somit gibt es unendlich viele Primzahlen. Prim ist hier als intendierte Semantik über natürliche Zahlen definiert.
   
   
  +++ Erfüllungsrelation