Eine syntaktisch gültige Ausdrucksfolge einer formalen Sprache, die aus atomaren Formeln und logischen Junktoren gemäß den Formationsregeln dieser Sprache konstruiert ist; häufig abgekürzt WFF.

Prinzip

Definiert die zulässigen Zeichenketten der Sprache durch rekursive Formationsregeln: atomare Formeln sind WFFs, und wenn A und B WFFs sind, dann sind bestimmte Kombinationen (z. B. ¬A, (A ∧ B), (A → B)) WFFs; Klammern und Operatoraritäten werden beachtet, um Mehrdeutigkeiten zu vermeiden.

Demonstration

Beispiele für WFFs in der Aussagenlogik: p, ¬q, (p ∧ ¬q), ((p → q) ∨ r). Eine Zeichenkette wie '∧ p q' oder 'p q ∧' ist in üblicher Infix-Notation ohne zusätzliche Formationskonventionen keine WFF.

Fehlanwendung

Zu meinen, jede intuitiv sinnvolle Zeichenkette sei eine Formel (z. B. Klammern weglassen oder Operatoraritäten ignorieren) oder einer schlecht geformten Zeichenfolge semantischen Gehalt zuzuweisen; natürliche Sprachverknüpfungen ohne formale Entsprechung zu verwenden.

Konsequenz

Wohlgeformte Formeln stellen sicher, dass syntaktische Operationen (Beweisregeln, Substitutionen) und semantische Bewertungen (Wahrheitstabellen, Bewertungen) eindeutig definiert sind; nur WFFs sind Eingaben für Beweissysteme und semantische Auswertungsfunktionen.

Umkehrung

Die Umkehr ist eine nicht wohlgeformte Zeichenfolge: eine Sequenz von Symbolen, die die Formationsregeln verletzt. Wenn man nicht wohlgeformte Zeichenfolgen wie Formeln behandelt, wird die Syntax zu semantisch nicht interpretierbarem Rauschen.

Abgrenzung

Gilt für die Objektsprache eines formalen Systems; schließt Metasprache-Kommentare, Beweisnotationen außerhalb der Grammatik und Sprachen mit anderen Formationsregeln (z. B. einige Programmiersprachen oder typentheoretische Syntaxen) aus.

Semantische Spannung

Spannung zwischen Lesbarkeit/Kürze und striktem Formalismus: Manche Notationen reduzieren Klammern oder ändern Assoziativitätskonventionen aus ergonomischen Gründen; dies muss mit dem strikten Begriff der Wohlgeformtheit in Einklang gebracht werden.

Synthese

Eine wohlgeformte Formel ist ein Ausdruck, der die rekursiven syntaktischen Formationsregeln einer formalen Sprache erfüllt und damit als gültiges Objekt für Deduktion und semantische Bewertung in diesem System fungiert.