Inom matematisk logik, propositionslogik och predikatlogik är en välformad formel, förkortad WFF eller wff, en sekvens av symboler från ett givet alfabet, som är en del av ett formellt språk, och som uttrycker meningen av ett logiskt objekt. Symbolerna av olika typer måste då komma i en viss ordning, som bestäms av språkets formella grammatik.

Exempel En formell grammatik i kan definieras i Backus-Naur-form på följande sätt:

<satsvariabel> ::= p | q | r | s <formel> ::= <satsvariabel> | ¬<formel> | (<formel>∧<formel>) | (<formel>∨<formel>) | (<formel>→<formel>) | (<formel>↔<formel>)

Med hjälp av denna grammatik blir sekvensen av symboler (((p → q) ∧ (r → s)) ∨ (¬q ∧ ¬s)) en välformad formel, eftersom den är grammatiskt korrekt. Sekvensen av symboler ((p → q)→(qq))p)) är däremot inte en inte en välbildad formel, eftersom den inte överensstämmer med grammatiken.

Kategori:Metalogik