# [Math] Please help with understanding a logic definition: Subformula

definitionlogic

Alright, so I am reading "Computability and Logic" by Boolos and Jeffrey, specifically I'm on chapter 9 "A Precis of First-Order Logic: Syntax. There has been more than a handful of definitions in this chapter, and I believe I've come to be able to understand what each of them are except one in particular which begins on pg. 110. Namely, the following:

"We officially define a string of consecutive symbols within a given formula to be a ${subformula}$ of the given formula if it is itself a formula."

So, I've tried to break this down and see where I am getting confused. I followed entirely what is being said until "…if it is itself a formula." The reason I am getting confused is why is this last part added? I was given a formula shouldn't "it" be a formula if that is what we are given?

Any help would be much appreciated!

I don't know what notation B&J use, but the point will be something like this. If you have a formula $$\forall x (P(x)\to(\neg Q(x)))$$ then for example $$x(P$$ is a string of consecutive symbols from this formula. However $x(P$ is not a grammatically (syntactically) correct formula, therefore it is not a subformula.
On the other hand, $P(x)$ is a string of consecutive symbols from the above formula, and $P(x)$ is itself a grammatically correct formula, so $P(x)$ is a subformula of the above.