Aussagenlogik
Definition der Syntax: Alphabet,
Aussagensymbole AS, induktive Definition der Formeln AF. (2.1.1)
Die Menge der Formeln AF läßt sich mit geeigneten Funktionen
als Peano-Algebra auffassen. Dadurch wird strukturelle Induktion möglich.
(2.1.2)
Definition der Semantik: Durch
Interpretation I:AS ® AUS
und Auswertungsfunktion IÙ oder durch Belegung s:AS®{0,1} (BEL:={0,1}AS) und
durch Auswertungsfunktion <s>.
(2.2.1, 2.2.3)
Tautologie,
Erfüllbarkeit, Kontradiktion, logische Implikation (a |= b) und Äquivalenz (a º b).
Die Definitionen sind semantisch: a |= b
ungleich a®b und a º b ungleich a«b.
a |= b und a º b sind keine
Formeln, sondern metasprachliche Ausdrücke! (2.3.2) Es gilt aber a |= b gdw. (a®b)
ist Tautologie und a º b gdw. (a«b) ist Tautologie. (2.3.6)
Die Menge der aussagenlogischen
Tautologien ist entscheidbar mit Wahrheitswerttafel. Aufwand (n-1).2n.
Problem ist NP-vollständig.
Dies folgt aus dem
Koinzidenzlemma:
Falls für alle BÎAS(a)
s(B)=s´(B)
gilt, folgt <s>(a)=<s´>(a). (2.4.1) (Beweis durch strukturelle
Induktion.)
Tautologien sind unter Substitution und modus ponens
abgeschlossen. (2.3.5)
Ersetzung von äquivalenten Teilformeln führt zu äquivalenter
Formel. (2.3.8)
Zu jeder Booleschen Funktion
g:{0,1}n®{0,1}
und jeder injektiven Funktion C:{1,...,n}®AS
gibt es eine Formel a mit g=fa,C. (2.4.3) (Beweis durch Formel in
kanonischer disjunktiver Normalform, siehe Beispiel S17)
Definition von (kanonischer) disjunktiver und konjunktiver
Normalform. (2.4.4)
Zu jeder Formel gibt es eine äquivalente in kanonischer
disjunktiver und konjunktiver Normalform. (2.4.5) (Beweis des ersten Teils
durch Rückgriff auf das Koinzidenzlemma, des zweiten Teils durch Erzeugen der
kan. disj. Normalform der Negation, danach Negation und de Morgan) (Beispiel
S18)
Die Junktorenmenge {T,^,Ø,Ù,Ú,®} ist vollständig, wie auch {Ø,Ú}, {Ø,Ù} und {Ø,®}.
Definition 2.4.6:
Erf(X):={sÎBEL | <s>(b)=1 für alle bÎX}
ist die Erfüllungsmenge von X.
X heißt erfüllbar, gdw.
Erf(X)≠Æ.
X heißt endlich erfüllbar, gdw. Y
erfüllbar für jede endliche Teilmenge YÍX.
X |=
a gdw. Erf(X)ÍErf(a).
Kompaktheitssatz,
Endlichkeitssatz:
Erf(X)=Æ, gdw. Erf(Y)=Æ für
eine endliche Menge YÍX.
Erf(X)≠Æ, gdw. X endlich erfüllbar ist.
X |=
a gdw. Y |= a für eine endliche
Menge YÍX.
Beweisidee zu 2: X wird durch Hinzunahme von {A0iA} oder {ØA0iA} zu X_ aufgebläht. Es gibt eine Belegung s mit <s>(a)=1 für alle aÎX_.. Also ist X_ erfüllbar und damit auch X.
Prädikatenlogik
Syntax und Semantik
Definition der Syntax: Alphabet,
Individuenvariablen Var, Prädikatsbezeichner Präd, Funktionsbezeichner Funk,
Typ t=(I,J), induktive Definition der
Terme Tmt, Atome PATt, induktive Definition der Formeln PFt.
Strukturelle Induktion. (3.2.5)
Rekursionssatz. (3.2.7)
Freie Variablen, Allabschluß, Substitution von freien
Variablen Sub, Variablenumbenennung VU,
gebundene Umbenennung GU.
Der Term t ist frei für die Variable y in der Formel a, gdw.
keine in t vorkommende Variable z in den Wirkungsbereich einer Quantifizierung "z oder $z
gerät. Beispiel: Sei a=(P(z)®"x$yQ(x,y,z)) und t=f(x,z). Nach Ersetzung von
z durch t erhält man (P(f(x,z))®"x$yQ(x,y,f(x,z))).
t ist nicht frei für z in a.
Definition der Semantik: t-Stuktur S=(S,P,g),
Belegung s:Var®S, BelS, Wert des Terms t unter der Belegung s WS(t)(s), Wahrheitswert der Formel g unter der Belegung s WWS(g)(s),
S |=
g(s) für WWS(g)(s)=1.
(3.3.3)
Koinzidenzlemma:
1) s|Vk(t)=s´|Vk(t) Þ WS(t)(s)=WS(t)(s´)
2) s|Fr(a)=s´|Fr(a) Þ WWS(a)(s)=WWS(a)(s´)
Beweis durch strukturelle
Induktion. (3.3.4)
Überführungslemma: Ersetzungen können in der Formel oder in
der Belegung durchgeführt werden. (3.3.6) (Beweis durch strukturelle
Induktion.) (Vergleiche mit smn-Theorem der Theoretischen Informatik)
Definition:
1) S heißt Modell von a (S
|= a), gdw. S |= a(s) für alle Belegungen sÎBelS.
2) a
heißt logisch gültig oder allgemeingültig, gdw. a
in allen t-Strukturen gültig ist.
3) Die Formeln a und b
heißen äquivalent in S , gdw. WWS(a)=WWS(b).
4) a
und b heißen logisch äquivalent (aºb), gdw. a
und b in allen t-Strukturen äquivalent sind. (3.3.7)
Lemma: (3.3.8)
1) (S |= a gdw. S |= "xa) für alle xÎVar.
S
|= a gdw. S |= "a.
2) a
und "a sind im allgemeinen nicht
logisch äquivalent. (Beispiel x<1)
3) a
und b sind äquivalent in S
gdw. S |= a«b.
4) a
º b gdw. a«b
logisch gültig ist.
Definition der prädikatenlogischen Tautologie. (3.3.10)
Definition: (3.3.16)
1) S heißt ein Modell von X,
gdw. S |= b für alle bÎX (S |= X).
2) X impliziert logisch a (X |= a ),
gdw. (S |= X Þ S
|= a für alle t-Strukturen S ). Für Æ |= a schreibt man auch |= a.
3) X heißt erfüllbar, gdw. es ein
Modell von X gibt.
Lemma: (3.3.17)
1) |= a gdw. a allgemeingültig.
2) Falls aÎAus, so gilt: a |= b gdw. a
® b allgemeingültig.
3) Falls a,bÎAus, so gilt: aºb gdw.
a |= b
und b |= a.
4) Falls aÎAus, so gilt: X |= a gdw.
XÈ{¬a}
nicht erfüllbar. (Widerspruchsbeweis)
a
ist allgemeingültig Û "a ist allgemeingültig Û ¬"a ist nicht erfüllbar. (3.3.18)
Definition: Kalkül, Axiom, Regel,
Erweiterung um Voraussetzungen, Beweis von w in K aus X (X |–K w). (3.4.1)
Lemma: Entscheidbarkeit der Beweise, Aufzählbarkeit der
Folgerungen, Kompaktheitssatz. (3.4.2)
Der prädikatenlogische Kalkül
Kalkül der Prädikatenlogik 1.
Stufe: (3.4.3)
R1:=Menge der prädikatenlogischen
Tautologien
R2:={"xa ® Sub| t frei für x in a}
R3:={Sub®
$xa
| t frei für x in a}
R4:={(a®b,a®"xb)
| x nicht frei in a}
R5:={(a®b,$xa®b)
| x nicht frei in a}
R6:={(a,a®b,b)}
Korrektheitssatz: X |–K a Þ X
|= a. (3.4.5)
Vollständigkeitssatz: X |= a Þ X
|–K a. (3.4.5) (hier ohne Beweis)
Kompaktheitssatz der
Prädikatenlogik 1. Stufe (3.4.7):
X |= a gdw. es existiert eine endliche Teilmenge YÍX mit Y |= a.
Beweisidee: X |= a Þ X
|–K a (Vollständigkeit)
Þ es existiert eine endliche Teilmenge YÍX mit Y |–K a
Þ es existiert eine endliche Teilmenge YÍX mit Y |= a
(Korrektheit).
Falls in t=(I,J) I und J rekursiv sind, ist die Menge der
allgemeingültigen Formeln vom Typ t
rekursiv-aufzählbar. (3.4.9)
Programme und Verifikationskalkül.
Beweis der Vollständigkeit der Prädikatenlogik
Jede Formel kann in eine äquivalente in pränexer Normalform
umgeformt werden. (3.5.2)
Jede Formelmenge X in pränexer
Normalform kann in eine in Skolemscher Normalform Sk(X) umgeformt werden, so
daß beide gleichzeitig erfüllbar sind oder nicht. (3.5.5) (Auswahlaxiom nötig!)
Definition von Herbrand-Universum
Ut,
Herbrand-Struktur über t,
Herbrand-Modell von XÍPF. (3.6.1,
3.6.3)
Sei X eine Menge von Aussagen in
Skolemscher Normalform. Dann ist X genau dann erfüllbar, wenn X ein
Herbrand-Modell besitzt. (3.6.4) (Beweis durch Induktion über die Anzahl #"(a))
Satz von Löwenheim-Skolem (3.6.5):
Falls X erfüllbar ist, besitzt X
ein Modell mit abzählbar-unendlicher Trägermenge.
Definition der Menge der Instanzen von XÍPF. (3.6.6)
Sei XÍAus in Skolemscher Normalform. Dann besitzt X genau dann ein Modell,
wenn Inst(X) erfüllbar ist. (3.6.7)
Satz von
Herbrand (3.6.9):
Sei XÍAus in Skolemscher Normalform. Dann ist X
genau dann erfüllbar, wenn jede endliche Teilmenge von Inst(X) erfüllbar ist.
(Beweis
durch Reduktion auf aussagenlogische Erfüllbarkeit und Benutzung des
Kompaktheitssatzes der Aussagenlogik)
Kompaktheitssatz der
Prädikatenlogik (3.6.10):
1) X erfüllbar Û X endlich erfüllbar.
2) X |= a Û es gibt eine endliche Teilmenge YÍX mit Y |= a.
Satz 3.6.11:
Sei t´=(Präd,Funk)
und t=(I,J) ein rekursiver Typ. Dann
gilt:
1) {aÎPFt´ | a
allgemeingültig} ist rekursiv-aufzählbar.
2) {aÎPFt | a allgemeingültig} ist rekursiv-aufzählbar.
3) {(a,b)ÎPFt´PFt | a
|= b} ist rekursiv-aufzählbar.
4) Für jede rek.-aufzählbare Menge
XÍPFt ist Kons(X) rek.-aufzählbar.
Aus diesem Satz folgt die Vollständigkeit der
Prädikatenlogik.
Beweis zu 1) durch Angabe eines
Programms, das bei Eingabe von a genau
dann hält, wenn a allgemeingültig ist:
1.
Falls a keine Formel, führe
Endlosschleife aus.
2.
Bilde b:="a.
3.
Bilde b´:=Skolemisierung der pränexen
Normalform von b.
4.
Teste der Reihe nach alle endlichen Teilmengen von
Y=IÍAF
auf aussagenlogische Erfüllbarkeit. Halte an,
falls eine unerfüllbare Menge gefunden
wurde.
Frage: Warum läßt sich aus diesem Programm nicht die
Entscheidbarkeit ableiten?
Unentscheidbarkeit der Prädikatenlogik
Satz 3.7.4: Es sei t0=(I,J)
ein Typ mit T,CÎI mit m(T)=1 und m(C)=3.
Dann ist die Menge {aÎPFt0
| |=
a} nicht entscheidbar.
Beweis durch Reduktion des Ableitbarkeitsproblems in
Semi-Thue-Systemen auf das Entscheidungsproblem der Prädikatenlogik. C bildet
dabei die Konkatenation und T die Ableitbarkeit eines Wortes ab.
Prädikatenlogik mit Gleichheit
Eine (t,=. )-Struktur ist eine t-Struktur S=(S,P,g) mit P=. =(=S). (3.8.1)
(=S ist definiert
als {(x,x) | xÎS})
Definition von =. -allgemeingültig, =. -logisch äquivalent, =. -logische Konsequenz, =. -erfüllbar. (3.8.2)
Die Gleichheit läßt sich nicht
durch eine Menge von Formeln L beschreiben. Sonst hätte jedes Model von LÈ{"x0"x1(x0=. x1)}
genau ein Element. Aber nach dem Satz von Löwenheim-Skolem gibt es ein Modell
mit abzählbar-unendlichem Träger.
Definition von Kt, Kongruenzrelation und Faktorisierung.
(3.8.3, 3.8.4)
Satz 3.8.7:
1) Falls S ein (t,=. )-Modell von X ist, dann ist S ein Modell von XÈKt.
2) Falls S ein Modell von XÈKt ist, dann ist S/P=.
ein (t,=. )-Modell von X.
X ist =. -erfüllbar Û XÈKt ist erfüllbar. (3.8.8)
Kompaktheitssatz (3.8.9):
1) X ist =. -erfüllbar Û Y
ist =. -erfüllbar für jede endliche
Teilmenge YÍX.
2) X |==.
a Û
es gibt eine endliche Teilmenge YÍX mit
Y |==.
a.
Satz von Löwenheim-Skolem
(3.8.10):
Falls X ein (t,=. )-Modell mit unendlicher Trägermenge besitzt, hat
X ein (t,=.)-Modell mit abzählbar-unendlicher Trägermenge.
(Zusatz nötig, da jedes (t,=. )-Modell von "x0"x1(x0=. x1) nur
ein Element besitzt!)
Satz 3.8.11:
1) {aÎPFt | a ist =. -allgemeingültig} ist rekursiv-aufzählbar.
2) {(a,b)ÎPFt´PFt | a
|==.
b} ist rekursiv-aufzählbar.
3) Für jede r.-a. Menge XÍPFt ist Kons(X):={aÎPFt | X |==.
a} r.-a.
Sei S eine (t,=. )-Struktur mit endlichem Individuenbereich. Dann gibt es
eine Menge XÍAust, so daß für alle (t,=. )-Strukturen S´
gilt:
S ist ein Modell von X Û S isomorph zu S´. (3.8.14) (ohne Beweis)
Dies ist ein Unterschied zur Prädikatenlogik ohne
Gleichheit. Zu n=2 ist die Formel wohl $x1$x2(Ø(x1=. x2)Ù"x0(x0=. x1Úx0=. x2))
und zu n=3 $x1$x2$x3(Ø(x1=. x2Úx1=. x3Úx2=. x3)Ù"x0(x0=. x1Úx0=. x2Úx0=. x3)).
Theorien
TH(N) :={a | N
|= a} heißt Theorie von N oder Arithmetik.
GrTh ist die
Gruppentheorie.
X heißt widerspruchsfrei gdw für
alle a gilt: nicht (X |= a und X |= Øa).
X heißt Theorie, gdw. X
widerspruchsfrei ist und für alle a
gilt:
X
|= a Þ
aÎX. (3.9.1)
Lemma 3.9.2:
1) X ist widerspruchsfrei, gdw. X
ist erfüllbar.
2) Kons(X) ist für
widerspruchsfreies X eine Theorie.
3) TH(S):={a | S |= a}
ist eine Theorie, genannt die Theorie von S:
TDLO:={a | DLO |= a}
ist die Theorie der dichten linearen Ordnung ohne Anfangs- und Endpunkt. (IR,{<,<IR),(=. ,=IR)},Æ)
und ( IQ,{<,<IQ),(=. ,=IQ)},Æ)
sind Modelle. Theorien von Strukturen legen diese nicht eindeutig fest. Z.B.
gibt es die Nicht-Standard-Modelle der Arithmetik: Für die Formelmenge
Y:={1+...+1<c} ist X:=Th(N)ÈY endlich erfüllbar. Also ist X nach dem
Kompaktheitssatz erfüllbar.
Die Theorie T heißt vollständig
gdw. für alle aÎAus gilt: aÎT oder ØaÎT.
Die Theorie T ist genau dann
vollständig, wenn T die Theorie einer Struktur ist. (3.9.4)
Vaught´s Test (3.9.5):
Falls T eine Theorie ist, die nur
Modelle mit unendlichem Träger besitzt und je zwei Modelle mit abzählbarem
Träger isomorph sind, ist T vollständig.
Satz von Cantor (3.9.6):
Falls S1:=(S1,{<,<S1),(=. ,=S1)},Æ) und S2:=(S2,{<,<S2),(=. ,=S2)},Æ) abzählbare dichte lineare Ordnungen ohne
Anfangs- und Endpunkt sind, sind S1
und S2
isomorph. (Beweis durch
Konstruktion des Graphen (si,ti)iÎIN des Isomorphismus mit
Hin-und-her-Methode)
TDLO
ist vollständig. (3.9.7) (folgt aus dem Satz von Cantor mit Vaught´s Test)
Vollständige rekursiv-aufzählbare
Theorien sind sogar entscheidbar. (3.9.8)
TDLO
ist entscheidbar. (3.9.9)
Th(NS) ist entscheidbar. (3.9.13) (Beweis
mit Quantorenelimination)
Ausdrucksstärke der Prädikatenlogik 1. Stufe
Elimination von
Funktionssymbolen
Die Prädikatenlogik mit
Funktionssymbolen läßt sich auf die ohne zurückführen. (3.10.3)
Definitorische
Erweiterungen
Die Ausdrucksstärke der PL ändert
sich nicht durch Hinzunahme definierbarer Prädikate und Funktionen. (3.10.5)
Axiomatisierung der
Mengenlehre
Die Theorie der Mengenlehre ist
nicht rekursiv aufzählbar. Deshalb hat sie keine rekursive Menge von Axiomen.
Das Axiomensystem von Zermelo-Fraenkel drückt nur notwendige Eigenschaften aus.
Das Russelsche Paradoxon legt die Frage nahe, ob die
Mengenlehre ein Modell von ZFC ist.
Kons(ZFC) ist keine vollständige
Theorie. Für die Kontinuumshypothese a
gilt weder ZFC |= a noch ZFC |= Øa. a
besagt, daß es eine Kardinalzahl k gibt mit À0<k<À1.
Mehrsortige
Prädikatenlogik der 1. Stufe
Die Ausdrucksstärke der PL ändert
sich nicht Mehrsortigkeit. (3.10.6)
Nicht-Charakterisierbarkeit
von Strukturen
Die Stuktur der reellen Zahlen
läßt sich nicht durch Formeln charakterisieren, da es nach Löwenheim-Skolem
auch abzählbare Modelle geben muß.
Die Stuktur der natürlichen Zahlen
läßt sich ebenfalls nicht durch Formeln charakterisieren, da es
Nicht-Standard-Modelle der Arithmetik gibt.
1. Gödelscher
Unvollständigkeitssatz
Es gibt wahre Aussagen der
Arithmetik, die nicht beweisbar sind.
2. Gödelscher
Unvollständigkeitssatz
Falls ZFC widerspruchsfrei ist,
läßt sich die Konsistenz von ZFC nicht aus ZFC herleiten.
Nicht-Ausdrückbarkeit
des Haltens von Programmen
Es gibt ein Programm, für das keine Formel existiert, die
genau dann gilt, wenn das Programm hält.
Die Logik der
schwachen zweiten Stufe
Die PL der schwachen 2. Stufe benutzt außer
Individuen-Variablen noch solche endlicher Teilmengen und die Î-Relation. Der Kompaktheitssatz gilt nicht
mehr. Die Struktur der natürlichen Zahlen ist bis auf Isomorphie durch Axiome
charakterisierbar.
Modale
Aussagenlogik
Einführung
Definition der Syntax der
Modallogik: Alphabet, Aussagensymbole AS, induktive Definition der Formeln MF
mit ⁄
und ◊. (5.1.1)
Definition der Semantik der
Modallogik: Rahmen R=(W,R) mit
Punktmenge W und Erreichbarkeitsrelation R, W-Belegung s:AS´W®{0,1}, modallogische Struktur M=(W,R,s), Wahrheitswert WWM,s(a)
mit
WWM,s(⁄a)=1 Û WWM,t(a)=1
für alle t mit (s,t)ÎR und
WWM,s(◊a)=1 Û WWM,t(a)=1
für ein t mit (s,t)ÎR.
Drei Arten von Gültigkeit: M |= a[s],
M |= a,
R |= a.
(5.1.1)
Koinzidenzlemma (5.1.5):
Für alle sÎW und n≥MR(a) und
alle W-Belegungen s1 und s2 gilt:
s1|A(s,n,a)
= s2|A(s,n,a)
Þ ((W,R,s1) |=
a[s] Û
(W,R,s2) |= a[s]),
wobei A(s,n,a):={(B,t) | BÎAS(a), tÎW,
(s,t)ÎR(n)}.
Überführungslemma: Ersetzungen können in der Formel oder in
der Belegung durchgeführt werden. (5.1.7)
Definition (5.1.9):
1) X |=r a
:Û (R
|= X Þ R |= a) für alle Rahmen R.
2) |=r a :Û Æ |= a
(a ist allgemeingültig).
R =(W,R) heißt zeitlogischer Rahmen, gdw. R irreflexiv und
transitiv ist. Eine modallogische Formel a
heißt zeitlogisch allgemeingültig, gdw. sie in allen zeitlogischen Rahmen gilt.
(5.1.15)
Sei X:={⁄b®⁄⁄b
| bÎMF}. Dann gilt:
X |=r a Û a gilt in allen transitiven Rahmen.
(5.1.17)
Sei X:={⁄b®⁄⁄b
| bÎMF}. Dann gilt: X |=r a
Û a ist zeitlogisch gültig. (5.1.22)
(Beweis durch Aufblähen des Rahmens zu einem irreflexiven Rahmen durch
((s,i),(t,j))ÎR* :Û (s,t)ÎR
und i<j.)
Die Irreflexivität läßt sich nicht modallogisch ausdrücken.
Entscheidbarkeit
Satz 5.2.7:
1) {aÎMF
| |=r a} ist entscheidbar.
2) {aÎMF
| a ist zeitlogisch gültig} ist
entscheidbar.
Beweisidee: Erzeuge systematisch zu Punktmengen {0,...,i-1},
die nicht mehr Elemente haben wie die Potenzmenge aller Teilformeln von a, alle zweistelligen Relationen und belege
die (B,k) für BÎAS(a) und k<i
mit allen Kombinationen von Wahrheitswerten. Teste ob a dann in allen Punkten k<i
gilt.
Von der Modallogik zur Temporalen Logik
Sei X:= {⁄a®◊a | aÎMF}È
{⁄a®⁄⁄a
| aÎMF}È
{⁄(⁄aÙa®b)Ú⁄(⁄bÙb®a) | a,bÎMF}È
{⁄(⁄a®a)®(◊⁄a®⁄a)
| aÎMF}.
Dann gilt für alle gÎMF: X |=r
g Û N |= g.
(5.3.1)
Definition: Prädikatenlogische Übersetzung von M (SM)
und von aÎMF (a*). (5.3.2)
Die Sprache der Prädikatenlogik
ist nicht schwächer als die der Modallogik:
M |= a[s] Û SM
|= a*[s] und M |= a Û SM
|= a*. (5.3.3, 5.3.4)
Definition 5.3.5: Sei aÎMF
und gÎPFt mit Fr(g)={x}.
1) a und g heißen äquivalent in M im Punkte s, gdw.
M |= a[s]
Û SM
|= g[s]. (Schreibweise M |= a[s]
g[s])
2) a und g heißen äquivalent in M, gdw. sie äquivalent in jedem Punkt s sind.
(Schreibweise M |= a
g)
Definition 5.3.6:
1) Der PAST-Operator P:MF®PFt ordnet jedem aÎMF die
Formel
$y(y<xÙSub) zu.
2) Der UNTIL-Operator U:MF´MF®PFt ordnet jedem aÎMF die Formel
$y(x<yÙ"z(x<zÙz<y®Sub)ÙSub) zu.
Die Sprache der Modallogik ist
schwächer als die der Prädikatenlogik : Der PAST-Operator P und der
UNTIL-Operator U sind nicht ausdrückbar. (5.3.7)
Definition der temporallogischen
Formeln (5.3.8):
Definiert wie die modallogischen
Formeln mit der zusätzlichen Regel {a,b}ÍTF
Þ (aUb)ÎTF.
U heißt UNTIL-Operator. Die Formel (^Ua) für aÎMF
schreibt man als Oa. O heißt
NEXTTIME-Operator.
Definition der Semantik des
UNTIL-Operators (5.3.9):
Sei M eine auf N basierende
Struktur, sÎIN und a,bÎTF. Dann gilt aUb im Punkt s, in Zeichen M |= aUb[s], gdw.
($tÎIN)(s<t und M |= b[t]
und ("uÎIN)(s<u<t
Þ M
|= a[u])).
Formeln heißen temporallogisch
allgemeingültig, gdw. sie im Rahmen N
gültig sind.
Es gilt N |= TUa«◊a,
N |= Oa®◊a
und N |= ⁄a®Oa.