Well-Formed Formula

In the formal language of propositional logic, a well-formed formula is one that obeys a strict set of rules so that it is unambiguous to evaluate.

Also see general well-formed formulae, under arbitrary formal languages.

Definition §

Well-formed Formula ^definition-wff

A formula, $f$, is well-formed if belongs to some formal language, $L$:

$$f\in L\subseteq {\Sigma }^{\ast }$$

Alternatively, a well-formed formula is one that can be interpreted unambiguously as an expression tree.

Formal Syntax - The parenthesis must be added

For both the definitions below, the parenthesis cannot be ignored! This is precisely why wffs are considered extremely strict. Even extremely trivial propositions like $A\wedge B$ are not wffs unless they have the accompanying parenthesis (in this case, it should be $(A\wedge B)$)

Propositional Logic §

Well-formed Formula (Propositional Logic) ^definition

In the formal language of propositional logic, a well-formed formula (i.e. a well-formed proposition) $\phi$ is defined, recursively in Backus-Naur form as: $\phi ::=P|\perp |\top |(\neg \phi )|(\phi \wedge \phi )|(\phi \vee \phi )|(\phi \to \phi )$

• $::=$ : Is defined to be
• $P$ : The set of all atoms (not just $P$!)
• $\top ,\perp$ : True and False respectively
• We can interpret any $\phi$’s in the right hand side as some other well-formed formula (hence the recursive defitinition)
• See logical connectives for the remaining symbols

Predicate Logic §

Well-formed Formula (Predicate Logic) ^definition

In the formal language of predicate logic, a well-formed formula $\phi$ is defined, recursively in Backus-Naur form as: $\phi ::=P|P(t_1,t_1,\dots )|\perp |\top |(\neg \phi )|(\phi \wedge \phi )|(\phi \vee \phi )|(\phi \to \phi )|(\forall x,\phi )|(\exists x,\phi )$

• $::=$ : Is defined to be
• $P$ : Any atomic predicate
  • $P$ (without any inputs) : Can be thought of as a proposition (technically a 0-ary, nullary predicate)
  • $P(t_1,t_2,\dots )$ : A predicate consisting of one or more terms
• $t$ : A term
• $x$ : A variable
• $\top ,\perp$ : True and False respectively
• We can interpret any $\phi$’s in the right hand side as some other well-formed formula (hence the recursive defitinition)
• See logical connectives for definitions of $\neg ,\wedge ,\vee ,\to ,$
• See logical quantifiers for definitions of $\forall ,\exists$

Evaluation §

For example, if we want to evaluate whether the following proposition is a wff:

$$((P\wedge Q)\to X),$$

we can do so by splitting it up into valid wffs:

1. $(\phi \to \phi )$: Need to check if $(P\wedge Q)$ and $X$ are wff’s
   1. $(\phi \wedge \phi )$: Need to check if $P$ and $Q$ are wff’s
      1. $P$ is an atom, therefore a wff.
      2. $Q$ is an atom, therefore a wff.
   2. $X$ is an atom, therefore wff.

Examples §

Examples §

• $P,Q,R,\dots$ : Any atom is a wff
• $(P\wedge Q)$ is a wff
• $((P\wedge Q)\to (X\vee Y))$ is a wff

Non-examples §

• $P\wedge Q$ is not a wff, as it is missing the parenthesis
• $\neg P$ is not a wff, again because of missing parentheses
• $(P\wedge Q)\vee (P\wedge W)$ is missing outer parenthesis