Definition:Well-Formed Part

Definition

Let $\FF$ be a formal language with alphabet $\AA$.

Let $\mathbf A$ be a well-formed formula of $\FF$.

Let $\mathbf B$ be a subcollation of $\mathbf A$.

Then $\mathbf B$ is a well-formed part of $\mathbf A$ if and only if $\mathbf B$ is a well-formed formula of $\FF$.

Proper Well-Formed Part

Let $\mathbf B$ be a well-formed part of $\mathbf A$.

Then $\mathbf B$ is a proper well-formed part of $\mathbf A$ if and only if $\mathbf B$ is not equal to $\mathbf A$.

Also known as

In sources where WFFs are referred to as formulas, the term subformula can often be seen.

Likewise, in sources where WFFs are called expressions, subexpression is the name of choice.

Sources

• 1993: M. Ben-Ari: Mathematical Logic for Computer Science ... (previous) ... (next): Chapter $2$: Propositional Calculus: $\S 2.4$: Logical equivalence and substitution: Definition $2.4.5$
• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
• 2000: Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems ... (previous) ... (next): $\S 1.3$: Propositional logic as a formal language
• 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.4$ Polish Notation: Definition $\mathrm{II}.4.4$
• 2012: M. Ben-Ari: Mathematical Logic for Computer Science (3rd ed.) ... (previous) ... (next): $\S 2.3.2$: Definition $2.30$