Semantik formalisieren

Semantik der Aussagenlogik

Auswertungsfunktion der Aussagenlogik

B={f,t}\mathcal{B}=\{\mathbf{f}, \mathbf{t}\} Wahrheitswerte

I:AVBI: A V \mapsto \mathcal{B} Interpretation

I={II:AVB}\mathcal{I}=\{I \mid I: A V \mapsto \mathcal{B}\} Environment


Auswertung von Aussagenlogische Formeln mit Interpretation festgelegt durch Funktion:

val : I×AFB \text {val : } \mathcal{I} \times \mathcal{A} \mathcal{F} \mapsto \mathcal{B} 

  1. valI(A)=I(A)\operatorname{val}_{I}(A)=I(A)

    wenn AAVA \in A V

  1. valI(T)=t\operatorname{val}_{I}(T)=\mathbf{t}

    wenn valI()=f\operatorname{val}_{I}(\perp)= \mathbf{f}

  1. valI(¬F)= not valI(F) \operatorname{val}_{I}(\neg F)=\text { not } \operatorname{val}_{I}(F) 
  1. valI((FG))=valI(F)valI(G) \operatorname{val}_{I}((F * G))=\operatorname{val}_{I}(F) \circledast \operatorname{val}_{I}(G) 

    wobei \circledast die logische Operation zu * ist.

Aussagenlogische Funktionen

Wichtig: Wir nutzen hier \equiv um metasprachliche Äquivalenz auszudrücken.

Semantik der Prädikatenlogik

Ausdrucksstärke der Prädikatenlogik

  • Beispiel: Relation

    Prädikat: " RR ist eine Äquivalenzrelation" mit Signatur {R},{},{}\langle\{\underline{R}\},\{\},\{\}\rangle lässt sich ausdrücken als F1F2F3F_{1} \wedge F_{2} \wedge F_{3} .

    F1=xR(x,x)F2=xy[R(x,y)R(y,x)]F3=xyz[(R(x,y)R(y,z))R(x,z)] \begin{aligned}&F_{1}=\forall x \underline{R}(x, x) \\&F_{2}=\forall x \forall y[\underline{R}(x, y) \supset \underline{R}(y, x)] \\&F_{3}=\forall x \forall y \forall z[(\underline{R}(x, y) \wedge \underline{R}(y, z)) \supset \underline{R}(x, z)]\end{aligned} 

Prädikatenlogische InterpretationI=D,Φ,ξ\small \mathcal I=\langle D, \Phi, \xi\rangle

Zur Erinnerung:

SignaturΣ\small \Sigmaals Menge von Symbolen

ModellstrukturD\small \mathcal Dals Beziehungen zwischen Symbol und Funktion für meaning-function

Prädikatenlogische Interpretation über Signatur Σ=PSΣ,KSΣ,FSΣ \small \Sigma=\left\langle P S_{\Sigma}, K S_{\Sigma}, F S_{\Sigma}\right\rangle  :

D\small D Domäne

Φ\small \Phi Signaturinterpretation

Man übergibt der FunktionΦ\small \Phiein Symbol und erhält die jeweilige Funktion.

PPSΣΦ(P):Dn{f,t} \small P \in P S_{\Sigma} \longrightarrow \Phi(P): D^{n} \mapsto\{\mathbf{f}, \mathbf{t}\} 

cKSΣΦ(c)D \small c \in K S_{\Sigma} \longrightarrow \Phi(c) \in D 

fFSΣΦ(f):DnD \small f \in F S_{\Sigma} \longrightarrow \Phi(f): D^{n} \mapsto D 

ξ\small \xi Variablenbelegung

ξ:IVSD\small \xi: I V S \mapsto D


Man sagt man interpretiert einen Ausdruck über eine (Modell-)StrukturD\small \mathcal{D}(zBZ,N,S\small \mathbb{Z}, \mathbb{N}, \mathbb{S}) und VariablenbelegungI\small I.

Jede PL-Interpretation I\small \mathcal I bestimmt eine Modellstruktur DI=D;PD,KD,FD \small \mathcal{D}_{\mathcal{I}}=\left\langle D ; P_{D}, K_{D}, F_{D}\right\rangle  und Variablenbelegung:

Man erhält die Menge aller Funktionen für die Modellstruktur aus der PL-Interpretation, indem man alle Zeichen aus der Signatur in die Φ\small \Phi-Funktion einsetzt.

PD={Φ(P)PPSΣ} \small P_{D}=\left\{\Phi(P) \mid P \in P S_{\Sigma}\right\} 

KD={Φ(c)cKSΣ} \small K_{D}=\left\{\Phi(c) \mid c \in K S_{\Sigma}\right\} 

FD={Φ(f)fFSΣ} \small F_{D}=\left\{\Phi(f) \mid f \in F S_{\Sigma}\right\} 

Die Menge aller PL-Interpretationen I\small \mathcal I : PINTΣ\small PINT_{\Sigma}

Auswertungsfunktion für PL-Formeln

valI:PINTΣ×PFΣ{f,t} \operatorname{val}_{\mathcal{I}}: P I N T_{\Sigma} \times \mathcal{P} \mathcal{F}_{\Sigma} \rightarrow\{\mathbf{f}, \mathbf{t}\} 

  1. valI()=t,valI()=f \small \operatorname{val}_{\mathcal{I}}(\top)=\mathbf{t}, \operatorname{val}_{\mathcal{I}}(\perp)=\mathbf{f} 
  1. valI(P(t1,,tn))=Φ(P)(MT(ξ,t1),,MT(ξ,tn)) \small \operatorname{val}_{\mathcal{I}}\left(P\left(t_{1}, \ldots, t_{n}\right)\right)=\Phi(P)\left(\mathcal{M}_{\mathcal{T}}\left(\xi, t_{1}\right), \ldots, \mathcal{M}_{\mathcal{T}}\left(\xi, t_{n}\right)\right) 
  1. valI(s=t)=t \small \operatorname{val}_{\mathcal{I}}(s=t)=\mathbf{t} 

    genau dann wenn Mτ(ξ,s)=MT(ξ,t) \small \mathcal{M} \mathcal{\tau}(\xi, s)=\mathcal{M} \mathcal{T}(\xi, t)  sonst f\small \mathbf f .

  1. valI(¬F)=¬valI(F) \small \operatorname{val}_{\mathcal{I}}(\neg F)=\neg \operatorname{val}_{\mathcal{I}}(F) 
  1. valI((FG))=valI(F) and valI(G) \small \operatorname{val}_{\mathcal{I}}((F \wedge G))=\operatorname{val}_{\mathcal{I}}(F) \text { and } \operatorname{val}_{\mathcal{I}}(G) 
  1. valI((FG))=valI(F) or valI(G) \small \operatorname{val}_{\mathcal{I}}((F \vee G))=\operatorname{val}_{\mathcal{I}}(F) \text { or } \operatorname{val}_{\mathcal{I}}(G) 
  1. valI((FG))=valI(F) implies valI(G) \small \operatorname{val}_{\mathcal{I}}((F \supset G))=\operatorname{val}_{\mathcal{I}}(F) \text { implies } \operatorname{val}_{\mathcal{I}}(G) 
  1. valI(vF)=tvalI(F)=t fu¨r alle IvI \small \operatorname{val}_{\mathcal{I}}(\forall v F)=\mathbf{t} \Longleftrightarrow \operatorname{val}_{\mathcal{I}^{\prime}}(F)=\mathbf{t} \text { für alle } \mathcal{I}^{\prime} \stackrel{v}{\sim} \mathcal{I} 
  1. valI(vF)=tvalI(F)=t fu¨r ein IvI \small \operatorname{val}_{\mathcal{I}}(\exists v F)=\mathbf{t} \Longleftrightarrow \operatorname{val}_{\mathcal{I}^{\prime}}(F)=\mathbf{t} \text { für ein } \mathcal{I}^{\prime} \stackrel{v}{\sim} \mathcal{I} 


IvI\small \mathcal{I}^{\prime} \stackrel{v}{\sim} \mathcal{I} bedeutet

I=D,Φ,ξ\small \mathcal{I}=\langle D, \Phi, \xi\rangle

I=D,Φ,ξ \small \mathcal{I}^{\prime}=\left\langle D, \Phi, \xi^{\prime}\right\rangle 

Und das wiederum bedeutet ξvξ\small \xi \stackrel{v}{\sim} \xi^{\prime} :

Gleiche Variablenbelegung ξ(w)=ξ(w)\small \xi(w)=\xi^{\prime}(w) für alle Variablen wIVS\small w \in IVS außer der Variable vv(alsovw\small v \ne w). Dennv\small vist die Variable die vom Quantor gebunden wurde.

Semantische Grundbegriffe

Formel FPFΣF \in \mathcal{P F}_{\Sigma}

(allgemein) gültig wenn für alle IPINTΣ\mathcal{I} \in P I N T_{\Sigma} immer valI(F)=t\operatorname{val}_{\mathcal{I}}(F)=\mathbf{t}

Immer wahr - dann nennt man es "Tautologie"

Alle Interpretationen sind Modelle

erfüllbar wenn für mindestens eine IPINTΣ\mathcal{I} \in P I N T_{\Sigma} gilt valI(F)=t\operatorname{val}_{\mathcal{I}}(F)=\mathbf{t}

Mind. bei 1 Fall wahr - dann nennt man es "Modell vonF"

widerlegbar wenn für mindestens eine IPINTΣ\mathcal{I} \in P I N T_{\Sigma} gilt valI(F)=f\operatorname{val}_{\mathcal{I}}(F)=\mathbf{f}

Mind. bei 1 Fall falsch - dann nennt man es "Gegenbeispiel" / "Gegenmodell"

unerfüllbar wenn für alle IPINTΣ\mathcal{I} \in P I N T_{\Sigma} immer valI(F)=f\operatorname{val}_{\mathcal{I}}(F)=\mathbf{f}

Immer falsch

Alle Interpretationen sind Gegenbeispiele

Bei einer Menge von Formeln FF : FPFΣ\mathcal{F} \subseteq \mathcal{P F}_{\Sigma}

erfüllbar wenn für mindestens eine IPINTΣ\mathcal{I} \in P I N T_{\Sigma} gilt fF:valI(f)=t \forall f\in F: \operatorname{val}_{\mathcal{I}}(f)=\mathbf{t} 

widerlegbar wenn für mindestens eine IPINTΣ\mathcal{I} \in P I N T_{\Sigma} gilt fF:valI(f)=f \forall f\in F: \operatorname{val}_{\mathcal{I}}(f)=\mathbf{f} 

Für gegebene Modellstrukturen D\mathcal D und Signaturinterpretationen Φ\Phi - sind Formeln FPFΣF \in \mathcal{P F}_{\Sigma}

zB erfüllbar in D\mathcal D bezüglich Φ\Phi wenn es mindestens ein I\mathcal{I} gibt mit DI=D\mathcal{D_I=D} für das gilt valI(F)=t\operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} .

Dann heißt I\mathcal I bezüglich Φ\Phi ein Modell von D\mathcal D in FF für alle ξ\xi .

Satz

FF hat keine endlichen Modelle.

Für alle Interpretationen I\mathcal I folgt mit valI(F)=t\operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} , dass die Domäne DD unendlich ist.

Modellierung mit PL

Auswahl der Stelligkeit

Richtige Anzahl hängt vom Kontext ab

  • Beispiel

    " Max liest Zeitung "

    Mögliche Prädikate:

    (0-stellig) Max_liest_Zeitung \text {Max\_liest\_Zeitung }

    (1-stellig) Liest_Zeitung(max)\text{Liest\_Zeitung(max)}

    (2-stellig) Liest(max, zeitung)\text{Liest(max, zeitung)}

Formalisierung natürlicher Sprache

  • Eigenschafen → Nomen

    Immer die Nomen als Argument nutzen, nie Eigenschaften

    Vermeiden: Sokrates_ist(sterblich)\text{Sokrates\_ist(sterblich)}

    Sinnvol: Ist_sterblich(sokrates)\text{Ist\_sterblich(sokrates)}

  • Pronomen

    "max liebt mia - mia liebt max"

    Sinnvoll: Liebt(mia, max)Liebt(max, mia) \text{Liebt(mia, max)} \wedge \text{Liebt(max, mia)} 

  • Unbestimmte Fürwörter

    "Ich kann nichts sehen."

    ¬x Kann_sehen(chris, x) \neg \exists x \text { Kann\_sehen}(\text {chris, } x) 

  • Fürwörter, Bindewörter

    "Vor mir ist etwas großes und es ist hungrig."

    x(Befindet_sich_vor(x, chris)Groß(x) Hungrig (x)) \exists x(\text {Befindet\_sich\_vor}(x, \text { chris}) \wedge \operatorname{Groß}(x) \wedge \text { Hungrig }(x)) 

  • Quantoren, Typen und Beziehungen

    "Jeder Student ist jünger als irgendein Professor."

    x(Stud(x)y(Prof(y)Ju¨nger(x,y))) \forall x(\operatorname{Stud}(x) \supset \exists y(\operatorname{Prof}(y) \wedge \operatorname{Jünger}(x, y))) 

    "Alle vernünftigen Leute verabscheuen Gewalt"

    x(Vernu¨nftig(x) Verabscheut(x, gewalt)) \forall x(\text {Vernünftig}(x) \supset \text { Verabscheut}(x, \text { gewalt})) 

    "Es gibt vernünftige Leute die Gewalt verabscheuen"

    x( Vernu¨nftig (x) Verabscheut (x, gewalt )) \exists x(\text { Vernünftig }(x) \wedge \text { Verabscheut }(x, \text { gewalt })) 

    Vertauschung von unterschiedlichen Quantoren

    "Jeder hat eine Mutter"

    xy Mutter(y,x)\forall x \exists y \text { Mutter}(y, x)

    yy hängt vom gewählten xx ab

    "Jemand ist die Mutter von allen"

    yxMutter(y,x) \exists y \forall x \operatorname{Mutter}(y, x) 

    yy ist unabhänging vom gewählten xx

  • Funktionssymbole

    "Jedes Kind ist jünger als seine Mutter"

    xy[(Kind(x)Mutter(y,x))Ju¨nger(x,y)] \forall x \forall y[(\operatorname{Kind}(x) \wedge \operatorname{Mutter}(y, x)) \supset \operatorname{Jünger}(x, y)] 

    Dadurch wird nicht berücksichtigt, dass jedes Kind eine biologische Mutter hat.

    Mutter sollte besser als Funktion aufgefasst werden, die jedem Kind seine eindeutig bestimmte Mutter zuordnet.

    x(Kind (x)Ju¨nger(x, mutter (x)) \forall x(\text {Kind }(x) \supset \operatorname{Jünger}(x, \text { mutter }(x)) 

    Eindeutige Beziehung

  • Beschränkung der Anzahl

    "Eva hat höchstens 2 Söhne"

    xyz(Sohn(z, eva )(z=xz=y)) \exists x \exists y \forall z(\operatorname{Sohn}(z, \text { eva }) \supset(z=x \vee z=y)) 

    "Kain hat mindestens 3 Söhne"

    xyz(Sohn(x, kain)Sohn(y, kain)Sohn(z, kain)xyxzyz) \exists x \exists y \exists z(\operatorname{Sohn}(x, \text { kain}) \wedge \operatorname{Sohn}(y, \text { kain}) \wedge \operatorname{Sohn}(z, \text { kain}) \\~~ \wedge ~x \neq y \wedge x \neq z \wedge y \neq z) 

Formalisierung formaler Inhalte

Nicht-totale Funktionen als nach-eindeutige Relationen

Relation R(x1,,xn,xn+1)R\left(x_{1}, \ldots, x_{n}, x_{n+1}\right) ist nach-eindeutig in D\mathcal D wenn gilt:

yzx1xn[(R(x1,,xn,y)R(x1,,xn,z))y=z] \forall \textcolor{pink}y \forall \textcolor{pink}z \forall x_{1} \cdots \forall x_{n}\left[\left(R\left(x_{1}, \ldots, x_{n}, \textcolor{pink}y\right) \wedge R\left(x_{1}, \ldots, x_{n}, \textcolor{pink}z\right)\right) \supset \textcolor{pink}y=\textcolor{pink}z\right] 

Satz von Gödel, Church, Turing

Jede partiell berechenbare Funktion lässt sich über N\N ausdrücken.

Logisches Schließen

Schlüsse, Konsequenz, Theorien

FIG\mathcal{F} \models_\mathcal{I} G

F1,,FnIGF_{1}, \ldots, F_{n} \models_{\mathcal{I}} G

Immer wenn alle Prämissen / Annahmen in allen beliebigen Interpretationen I\mathcal I wahr sind, ist auch die Konklusion / Folgerung in I\mathcal I wahr.

Spezialfall:F={}:G\mathcal{F}=\{\}: ~~\models GbedeutetGGist gültig.


GG folgt aus F\mathcal F genau dann wenn F{¬G}\mathcal{F} \cup\{\neg G\} unerfüllbar ist.

Semantisches Schließen

F1,,FnGF_{1}, \ldots, F_{n} \models G genau dann wenn F1(F2(FnG)) F_{1} \supset\left(F_{2} \supset \cdots\left(F_{n} \supset G\right) \cdots\right)  bzw (F1Fn)G\left(F_{1} \wedge \cdots \wedge F_{n}\right) \supset G gültig ist.

Logische Äquivalenz

FGF \lrarr G wenn FGF \models G und GFG \models F

bzw (FG)(GF)\models(F \supset G) \wedge(G \supset F) .

Axiomatische Theorien

Eine Theorie ist eine Menge von Formeln.

Eine axiomatische Theorie T\mathcal T ist gegeben durch

eine Menge Axiome A\mathcal A

sodass T={FAF}\mathcal{T}=\{F \mid \mathcal{A} \models F\}

Man sagt: A\mathcal A axiomatisiert T\mathcal T .

Wir wollen dass A\mathcal A möglichst endlich oder zumindest entscheidbar ist.

Theorie einer (Modell-)Struktur

Für jede Struktur I\mathcal I ist Th(I)={FvalI(F)=t} \operatorname{Th}(\mathcal{I})=\left\{F \mid \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t}\right\}  die Theorie.

Logische Unabhängigkeit (von anderen Formeln)

Eine Formel GG heißt unabhängig von der Formel-Menge F\mathcal F , wenn

FG\mathcal{F} \models G und F¬G\mathcal F \models \neg G nicht gelten.

Dafür muss man zwei Modelle I,I\mathcal I, \mathcal I' finden für die gilt valI(G)=f\operatorname{val}_{\mathcal{I}}(G)=\mathbf{f} und valI(G)=t\operatorname{val}_{\mathcal{I}^{\prime}}(G)=\mathbf{t} .