Definition:Well-Formed Part

From ProofWiki
(Redirected from Definition:Subformula)
Jump to navigation Jump to search

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