Semantik der Aussagenlogik Auswertungsfunktion der Aussagenlogik
B = { f , t } \mathcal{B}=\{\mathbf{f}, \mathbf{t}\} B = { f , t }
Wahrheitswerte
I : A V ↦ B I: A V \mapsto \mathcal{B} I : A V ↦ B
Interpretation
I = { I ∣ I : A V ↦ B } \mathcal{I}=\{I \mid I: A V \mapsto \mathcal{B}\} I = { I ∣ I : A V ↦ B }
Environment
Auswertung von Aussagenlogische Formeln mit Interpretation festgelegt durch Funktion:
val : I × A F ↦ B
\text {val : } \mathcal{I} \times \mathcal{A} \mathcal{F} \mapsto \mathcal{B}
val : I × A F ↦ B
val I ( A ) = I ( A ) \operatorname{val}_{I}(A)=I(A) val
I
( A ) = I ( A )
wenn
A ∈ A V A \in A V A ∈ A V
val I ( T ) = t \operatorname{val}_{I}(T)=\mathbf{t} val
I
( T ) = t
wenn
val I ( ⊥ ) = f \operatorname{val}_{I}(\perp)= \mathbf{f} val
I
( ⊥ ) = f
val I ( ¬ F ) = not val I ( F )
\operatorname{val}_{I}(\neg F)=\text { not } \operatorname{val}_{I}(F)
val
I
( ¬ F ) = not val
I
( F ) val I ( ( F ∗ G ) ) = val I ( F ) ⊛ val I ( G )
\operatorname{val}_{I}((F * G))=\operatorname{val}_{I}(F) \circledast \operatorname{val}_{I}(G)
val
I
(( F ∗ G )) = val
I
( F ) ⊛ 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: "
R R R
ist eine Äquivalenzrelation" mit Signatur
⟨ { R ‾ } , { } , { } ⟩ \langle\{\underline{R}\},\{\},\{\}\rangle ⟨{ R } , { } , { }⟩
lässt sich ausdrücken als
F 1 ∧ F 2 ∧ F 3 F_{1} \wedge F_{2} \wedge F_{3} F 1 ∧ F 2 ∧ F 3
.
F 1 = ∀ x R ‾ ( x , x ) F 2 = ∀ x ∀ y [ R ‾ ( x , y ) ⊃ R ‾ ( y , x ) ] F 3 = ∀ x ∀ y ∀ z [ ( 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}
F
1 = ∀ x
R
( x , x )
F
2 = ∀ x ∀
y
[
R
( x ,
y
) ⊃
R
(
y
, x )]
F
3 = ∀ x ∀
y
∀
z
[(
R
( x ,
y
) ∧
R
(
y
,
z
)) ⊃
R
( x ,
z
)]
Prädikatenlogische Interpretation I = ⟨ D , Φ , ξ ⟩ \small \mathcal I=\langle D, \Phi, \xi\rangle I = ⟨ D , Φ , ξ ⟩
Zur Erinnerung:
Signatur Σ \small \Sigma Σ als Menge von Symbolen
Modellstruktur D \small \mathcal D D als Beziehungen zwischen Symbol und Funktion für meaning-function
Prädikatenlogische Interpretation über Signatur
Σ = ⟨ P S Σ , K S Σ , F S Σ ⟩
\small \Sigma=\left\langle P S_{\Sigma}, K S_{\Sigma}, F S_{\Sigma}\right\rangle
Σ = ⟨ P S Σ , K S Σ , F S Σ ⟩
:
D \small D D
Domäne
Φ \small \Phi Φ
Signaturinterpretation
Man übergibt der Funktion Φ \small \Phi Φ ein Symbol und erhält die jeweilige Funktion.
P ∈ P S Σ ⟶ Φ ( P ) : D n ↦ { f , t }
\small P \in P S_{\Sigma} \longrightarrow \Phi(P): D^{n} \mapsto\{\mathbf{f}, \mathbf{t}\}
P ∈ P S Σ ⟶ Φ ( P ) : D n ↦ { f , t }
c ∈ K S Σ ⟶ Φ ( c ) ∈ D
\small c \in K S_{\Sigma} \longrightarrow \Phi(c) \in D
c ∈ K S Σ ⟶ Φ ( c ) ∈ D
f ∈ F S Σ ⟶ Φ ( f ) : D n ↦ D
\small f \in F S_{\Sigma} \longrightarrow \Phi(f): D^{n} \mapsto D
f ∈ F S Σ ⟶ Φ ( f ) : D n ↦ D
ξ \small \xi ξ
Variablenbelegung
ξ : I V S ↦ D \small \xi: I V S \mapsto D ξ : I V S ↦ D
Man sagt man interpretiert einen Ausdruck über eine (Modell-)Struktur D \small \mathcal{D} D (zB Z , N , S \small \mathbb{Z}, \mathbb{N}, \mathbb{S} Z , N , S ) und Variablenbelegung I \small I I .
Jede PL-Interpretation
I \small \mathcal I I
bestimmt eine Modellstruktur
D I = ⟨ D ; P D , K D , F D ⟩
\small \mathcal{D}_{\mathcal{I}}=\left\langle D ; P_{D}, K_{D}, F_{D}\right\rangle
D I = ⟨ D ; P D , K D , F D ⟩
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.
P D = { Φ ( P ) ∣ P ∈ P S Σ }
\small P_{D}=\left\{\Phi(P) \mid P \in P S_{\Sigma}\right\}
P
D
= { Φ ( P ) ∣ P ∈ P S Σ }
K D = { Φ ( c ) ∣ c ∈ K S Σ }
\small K_{D}=\left\{\Phi(c) \mid c \in K S_{\Sigma}\right\}
K
D
= { Φ ( c ) ∣ c ∈ K S Σ }
F D = { Φ ( f ) ∣ f ∈ F S Σ }
\small F_{D}=\left\{\Phi(f) \mid f \in F S_{\Sigma}\right\}
F
D
= { Φ ( f ) ∣ f ∈ F S Σ }
Die Menge aller PL-Interpretationen
I \small \mathcal I I
:
P I N T Σ \small PINT_{\Sigma} P I N T Σ
Auswertungsfunktion für PL-Formeln
val I : P I N T Σ × P F Σ → { f , t }
\operatorname{val}_{\mathcal{I}}: P I N T_{\Sigma} \times \mathcal{P} \mathcal{F}_{\Sigma}
\rightarrow\{\mathbf{f}, \mathbf{t}\}
val I : P I N T Σ × P F Σ → { f , t }
val I ( ⊤ ) = t , val I ( ⊥ ) = f
\small \operatorname{val}_{\mathcal{I}}(\top)=\mathbf{t},
\operatorname{val}_{\mathcal{I}}(\perp)=\mathbf{f}
val I ( ⊤ ) = t , val I ( ⊥ ) = f val I ( P ( t 1 , … , t n ) ) = Φ ( P ) ( M T ( ξ , t 1 ) , … , M T ( ξ , t n ) )
\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)
val I ( P
(
t 1 , … , t n
)
) = Φ ( P ) ( M
T
(
ξ , t 1
)
, … , M
T
(
ξ , t n
)
) val I ( s = t ) = t
\small \operatorname{val}_{\mathcal{I}}(s=t)=\mathbf{t}
val I ( s = t ) = t
genau dann wenn
M τ ( ξ , s ) = M T ( ξ , t )
\small \mathcal{M} \mathcal{\tau}(\xi, s)=\mathcal{M} \mathcal{T}(\xi, t)
M τ ( ξ , s ) = M T ( ξ , t )
sonst
f \small \mathbf f f
.
val I ( ¬ F ) = ¬ val I ( F )
\small \operatorname{val}_{\mathcal{I}}(\neg F)=\neg \operatorname{val}_{\mathcal{I}}(F)
val I ( ¬ F ) = ¬ val I ( F ) val I ( ( F ∧ G ) ) = val I ( F ) and val I ( G )
\small \operatorname{val}_{\mathcal{I}}((F \wedge G))=\operatorname{val}_{\mathcal{I}}(F) \text {
and } \operatorname{val}_{\mathcal{I}}(G)
val I (( F ∧ G )) = val I ( F ) and val I ( G ) val I ( ( F ∨ G ) ) = val I ( F ) or val I ( G )
\small \operatorname{val}_{\mathcal{I}}((F \vee G))=\operatorname{val}_{\mathcal{I}}(F) \text { or }
\operatorname{val}_{\mathcal{I}}(G)
val I (( F ∨ G )) = val I ( F ) or val I ( G ) val I ( ( F ⊃ G ) ) = val I ( F ) implies val I ( G )
\small \operatorname{val}_{\mathcal{I}}((F \supset G))=\operatorname{val}_{\mathcal{I}}(F) \text {
implies } \operatorname{val}_{\mathcal{I}}(G)
val I (( F ⊃ G )) = val I ( F ) implies val I ( G ) val I ( ∀ v F ) = t ⟺ val I ′ ( F ) = t f u ¨ r alle I ′ ∼ v I
\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}
val I ( ∀ v F ) = t ⟺ val
I
′ ( F ) = t f u ¨ r alle I ′ ∼
v
I val I ( ∃ v F ) = t ⟺ val I ′ ( F ) = t f u ¨ r ein I ′ ∼ v I
\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}
val I ( ∃ v F ) = t ⟺ val
I
′ ( F ) = t f u ¨ r ein I ′ ∼
v
I
I ′ ∼ v I \small \mathcal{I}^{\prime} \stackrel{v}{\sim} \mathcal{I} I ′ ∼ v I
bedeutet
I = ⟨ D , Φ , ξ ⟩ \small \mathcal{I}=\langle D, \Phi, \xi\rangle I = ⟨ D , Φ , ξ ⟩
I ′ = ⟨ D , Φ , ξ ′ ⟩
\small \mathcal{I}^{\prime}=\left\langle D, \Phi, \xi^{\prime}\right\rangle
I ′ = ⟨ D , Φ , ξ ′ ⟩
Und das wiederum bedeutet
ξ ∼ v ξ ′ \small \xi \stackrel{v}{\sim} \xi^{\prime} ξ ∼ v ξ ′
:
Gleiche Variablenbelegung
ξ ( w ) = ξ ′ ( w ) \small \xi(w)=\xi^{\prime}(w) ξ ( w ) = ξ ′ ( w )
für alle Variablen
w ∈ I V S \small w \in IVS w ∈ I V S
außer der Variable
v v v (also v ≠ w \small v \ne w v = w ). Denn v \small v v ist die Variable die vom Quantor gebunden wurde.
Semantische Grundbegriffe
Formel
F ∈ P F Σ F \in \mathcal{P F}_{\Sigma} F ∈ P F Σ
(allgemein) gültig
wenn für alle
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
immer
val I ( F ) = t \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} val I ( F ) = t
Immer wahr - dann nennt man es "Tautologie"
Alle Interpretationen sind Modelle
erfüllbar
wenn für mindestens eine
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
gilt
val I ( F ) = t \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} val I ( F ) = t
Mind. bei 1 Fall wahr - dann nennt man es "Modell von F "
widerlegbar
wenn für mindestens eine
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
gilt
val I ( F ) = f \operatorname{val}_{\mathcal{I}}(F)=\mathbf{f} val I ( F ) = f
Mind. bei 1 Fall falsch - dann nennt man es "Gegenbeispiel" / "Gegenmodell"
unerfüllbar
wenn für alle
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
immer
val I ( F ) = f \operatorname{val}_{\mathcal{I}}(F)=\mathbf{f} val I ( F ) = f
Immer falsch
Alle Interpretationen sind Gegenbeispiele
Bei einer Menge von Formeln
F F F
:
F ⊆ P F Σ \mathcal{F} \subseteq \mathcal{P F}_{\Sigma} F ⊆ P F Σ
erfüllbar
wenn für mindestens eine
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
gilt
∀ f ∈ F : val I ( f ) = t
\forall f\in F: \operatorname{val}_{\mathcal{I}}(f)=\mathbf{t}
∀ f ∈ F : val I ( f ) = t
widerlegbar
wenn für mindestens eine
I ∈ P I N T Σ \mathcal{I} \in P I N T_{\Sigma} I ∈ P I N T Σ
gilt
∀ f ∈ F : val I ( f ) = f
\forall f\in F: \operatorname{val}_{\mathcal{I}}(f)=\mathbf{f}
∀ f ∈ F : val I ( f ) = f
Für gegebene Modellstrukturen
D \mathcal D D
und Signaturinterpretationen
Φ \Phi Φ
- sind Formeln
F ∈ P F Σ F \in \mathcal{P F}_{\Sigma} F ∈ P F Σ
zB
erfüllbar
in
D \mathcal D D
bezüglich
Φ \Phi Φ
wenn es mindestens ein
I \mathcal{I} I
gibt mit
D I = D \mathcal{D_I=D} D I = D
für das gilt
val I ( F ) = t \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} val I ( F ) = t
.
Dann heißt
I \mathcal I I
bezüglich
Φ \Phi Φ
ein Modell von
D \mathcal D D
in
F F F
für alle
ξ \xi ξ
.
Satz
F F F
hat keine endlichen Modelle.
Für alle Interpretationen
I \mathcal I I
folgt mit
val I ( F ) = t \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t} val I ( F ) = t
, dass die Domäne
D D D
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 } Max_liest_Zeitung
(1-stellig)
Liest_Zeitung(max) \text{Liest\_Zeitung(max)} Liest_Zeitung(max)
(2-stellig)
Liest(max, zeitung) \text{Liest(max, zeitung)} 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)} Sokrates_ist(sterblich)
Sinnvol:
Ist_sterblich(sokrates) \text{Ist\_sterblich(sokrates)} 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)}
Liebt(mia, max) ∧ 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)
¬∃ x Kann_sehen ( 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))
∃ x ( Befindet_sich_vor ( x , chris ) ∧ Groß ( x ) ∧ Hungrig ( x ))
Quantoren, Typen und Beziehungen "Jeder Student ist jünger als irgendein Professor."
∀ x ( Stud ( x ) ⊃ ∃ y ( Prof ( y ) ∧ J u ¨ n g e r ( x , y ) ) )
\forall x(\operatorname{Stud}(x) \supset \exists y(\operatorname{Prof}(y) \wedge
\operatorname{Jünger}(x, y)))
∀ x ( Stud ( x ) ⊃ ∃ y ( Prof ( y ) ∧ J u ¨ nger ( x , y )))
"Alle vernünftigen Leute verabscheuen Gewalt"
∀ x ( Vern u ¨ nftig ( x ) ⊃ Verabscheut ( x , gewalt ) )
\forall x(\text {Vernünftig}(x) \supset \text { Verabscheut}(x, \text { gewalt}))
∀ x ( Vern u ¨ nftig ( x ) ⊃ Verabscheut ( x , gewalt ))
"Es gibt vernünftige Leute die Gewalt verabscheuen"
∃ x ( Vern u ¨ nftig ( x ) ∧ Verabscheut ( x , gewalt ) )
\exists x(\text { Vernünftig }(x) \wedge \text { Verabscheut }(x, \text { gewalt }))
∃ x ( Vern u ¨ nftig ( x ) ∧ Verabscheut ( x , gewalt ))
Vertauschung von unterschiedlichen Quantoren
"Jeder hat eine Mutter"
∀ x ∃ y Mutter ( y , x ) \forall x \exists y \text { Mutter}(y, x) ∀ x ∃ y Mutter ( y , x )
y y y
hängt vom gewählten
x x x
ab
"Jemand ist die Mutter von allen"
∃ y ∀ x Mutter ( y , x )
\exists y \forall x \operatorname{Mutter}(y, x)
∃ y ∀ x Mutter ( y , x )
y y y
ist unabhänging vom gewählten
x x x
Funktionssymbole "Jedes Kind ist jünger als seine Mutter"
∀ x ∀ y [ ( Kind ( x ) ∧ Mutter ( y , x ) ) ⊃ J u ¨ n g e r ( x , y ) ]
\forall x \forall y[(\operatorname{Kind}(x) \wedge \operatorname{Mutter}(y, x)) \supset
\operatorname{Jünger}(x, y)]
∀ x ∀ y [( Kind ( x ) ∧ Mutter ( y , x )) ⊃ J u ¨ 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 ) ⊃ J u ¨ n g e r ( x , mutter ( x ) )
\forall x(\text {Kind }(x) \supset \operatorname{Jünger}(x, \text { mutter }(x))
∀ x ( Kind ( x ) ⊃ J u ¨ nger ( x , mutter ( x ))
Beschränkung der Anzahl "Eva hat höchstens 2 Söhne"
∃ x ∃ y ∀ z ( Sohn ( z , eva ) ⊃ ( z = x ∨ z = y ) )
\exists x \exists y \forall z(\operatorname{Sohn}(z, \text { eva }) \supset(z=x \vee z=y))
∃ x ∃ y ∀ z ( Sohn ( z , eva ) ⊃ ( z = x ∨ z = y ))
"Kain hat mindestens 3 Söhne"
∃ x ∃ y ∃ z ( Sohn ( x , kain ) ∧ Sohn ( y , kain ) ∧ Sohn ( z , kain ) ∧ x ≠ y ∧ x ≠ z ∧ y ≠ z )
\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)
∃ x ∃ y ∃ z ( Sohn ( x , kain ) ∧ Sohn ( y , kain ) ∧ Sohn ( z , kain ) ∧ x = y ∧ x = z ∧ y = z )
Formalisierung formaler Inhalte
Nicht-totale Funktionen als nach-eindeutige Relationen
Relation
R ( x 1 , … , x n , x n + 1 ) R\left(x_{1}, \ldots, x_{n}, x_{n+1}\right) R ( x 1 , … , x n , x n + 1 )
ist nach-eindeutig in
D \mathcal D D
wenn gilt:
∀ y ∀ z ∀ x 1 ⋯ ∀ x n [ ( R ( x 1 , … , x n , y ) ∧ R ( x 1 , … , x n , 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]
∀ y ∀ z ∀ x 1 ⋯ ∀ x n [ ( R ( x 1 , … , x n , y ) ∧ R ( x 1 , … , x n , z ) ) ⊃ y = z ]
Satz von Gödel, Church, Turing
Jede partiell berechenbare Funktion lässt sich über
N \N N
ausdrücken.
Logisches Schließen Schlüsse, Konsequenz, Theorien
F ⊨ I G \mathcal{F} \models_\mathcal{I} G F ⊨ I G
F 1 , … , F n ⊨ I G F_{1}, \ldots, F_{n} \models_{\mathcal{I}} G F 1 , … , F n ⊨ I G
Immer wenn alle Prämissen / Annahmen in allen beliebigen Interpretationen
I \mathcal I I
wahr sind, ist auch die Konklusion / Folgerung in
I \mathcal I I
wahr.
Spezialfall: F = { } : ⊨ G \mathcal{F}=\{\}: ~~\models G F = { } : ⊨ G bedeutet G G G ist gültig.
G G G
folgt aus
F \mathcal F F
genau dann wenn
F ∪ { ¬ G } \mathcal{F} \cup\{\neg G\} F ∪ { ¬ G }
unerfüllbar ist.
Semantisches Schließen
F 1 , … , F n ⊨ G F_{1}, \ldots, F_{n} \models G F 1 , … , F n ⊨ G
genau dann wenn
F 1 ⊃ ( F 2 ⊃ ⋯ ( F n ⊃ G ) ⋯ )
F_{1} \supset\left(F_{2} \supset \cdots\left(F_{n} \supset G\right) \cdots\right)
F 1 ⊃ ( F 2 ⊃ ⋯ ( F n ⊃ G ) ⋯ )
bzw
( F 1 ∧ ⋯ ∧ F n ) ⊃ G \left(F_{1} \wedge \cdots \wedge F_{n}\right) \supset G ( F 1 ∧ ⋯ ∧ F n ) ⊃ G
gültig ist.
Logische Äquivalenz
F ↔ G F \lrarr G F ↔ G
wenn
F ⊨ G F \models G F ⊨ G
und
G ⊨ F G \models F G ⊨ F
bzw
⊨ ( F ⊃ G ) ∧ ( G ⊃ F ) \models(F \supset G) \wedge(G \supset F) ⊨ ( F ⊃ G ) ∧ ( G ⊃ F )
.
Axiomatische Theorien Eine Theorie ist eine Menge von Formeln.
Eine axiomatische Theorie
T \mathcal T T
ist gegeben durch
eine Menge Axiome
A \mathcal A A
sodass
T = { F ∣ A ⊨ F } \mathcal{T}=\{F \mid \mathcal{A} \models F\} T = { F ∣ A ⊨ F }
Man sagt:
A \mathcal A A
axiomatisiert
T \mathcal T T
.
Wir wollen dass
A \mathcal A A
möglichst endlich oder zumindest entscheidbar ist.
Theorie einer (Modell-)Struktur
Für jede Struktur
I \mathcal I I
ist
Th ( I ) = { F ∣ val I ( F ) = t }
\operatorname{Th}(\mathcal{I})=\left\{F \mid \operatorname{val}_{\mathcal{I}}(F)=\mathbf{t}\right\}
Th ( I ) = { F ∣ val I ( F ) = t }
die Theorie.
Logische Unabhängigkeit (von anderen Formeln)
Eine Formel
G G G
heißt unabhängig von der Formel-Menge
F \mathcal F F
, wenn
F ⊨ G \mathcal{F} \models G F ⊨ G
und
F ⊨ ¬ G \mathcal F \models \neg G F ⊨ ¬ G
nicht gelten.
Dafür muss man zwei Modelle
I , I ′ \mathcal I, \mathcal I' I , I ′
finden für die gilt
val I ( G ) = f \operatorname{val}_{\mathcal{I}}(G)=\mathbf{f} val I ( G ) = f
und
val I ′ ( G ) = t \operatorname{val}_{\mathcal{I}^{\prime}}(G)=\mathbf{t} val I ′ ( G ) = t
.