FOLSätze

FOL-Sätze, oder Sätze der ersten Ordnung (First-Order Logic, FOL), sind geschlossene Formeln der ersten Ordnung. Sie enthalten keine freien Variablen; alle Variablen sind durch Quantifizierer gebunden. Die Sprache einer FOL besteht aus einer Signatur mit Funktionssymbolen, Prädikatensymbolen, Konstanten, Variablen, logischen Operatoren (wie ¬, ∧, ∨, →, ↔) und Quantifizierern (∀, ∃).

Aufbau: Termen werden aus Variablen, Konstanten und Funktionssymbolen gebildet. Atomares Formelbildet sich aus einem Prädikatensymbol angewandt auf eine Liste von Termen. Aus atomaren Formeln entstehen durch logische Verknüpfungen komplexe Formeln; Quantifizierer binden Variablen in Formeln. Ein Satz liegt vor, wenn alle Variablen in der Formel gebunden sind.

Sätze vs. offene Formeln: Eine FOL-Formel ist ein Satz, wenn sie keine freien Variablen enthält; offene Formeln haben mindestens eine freie Variable. Sätze können wahr oder falsch in einer gegebenen Interpretation sein, offene Formeln hingegen liefern unter einer Variablenzuweisung Werte.

Semantik: Eine Interpretation (Struktur) M besteht aus einer nichtleeren Domäne D und einer Interpretation der Symbolen (Funktionen, Relationen, Konstanten). Die Wahrheit eines Satzes φ in M wird durch die Semantik M ⊨ φ bestimmt. φ ist gültig, wenn M ⊨ φ in allen Strukturen M gilt. φ ist satisfizierbar, wenn es mindestens eine Struktur M gibt, in der M ⊨ φ gilt.

Beispiele: ∀x (P(x) → Q(x)) ist ein FOL-Satz, wenn P und Q eindimensionale Prädikate sind. ∃x R(x) ist ebenfalls ein Satz, sofern R ein Prädikat ist.

Verwendung: FOL-Sätze bilden die formale Grundlage der Mathematik, Informatik und formalen Linguistik. Allgemeine Entscheidbarkeit der ganzen FOL gilt nicht; aber Teilbereiche und spezielle Sprachen weisen andere Eigenschaften auf.