PlanetMath (more info)
 Math for the people, by the people.
Encyclopedia | Requests | Forums | Docs | Wiki | Random | RSS  
Login
create new user
name:
pass:
forget your password?
Main Menu
Owner confidence rating: Very high Entry average rating: No information on entry rating
subformula (Definition)

Let $ L$ be a first order language and suppose $ \varphi$ is a formula of $ L$. A subformula of $ \varphi$ is defined as any of the following:

  1. $ \varphi$ is a subformula of $ \varphi$;
  2. if $ \neg \psi$ is a subformula of $ \varphi$ for some $ L$-formula $ \psi$, then so is $ \psi$;
  3. if $ \alpha\wedge \beta$ is a subformula of $ \varphi$ for some $ L$-formulas $ \alpha,\beta$, then so are $ \alpha$ and $ \beta$;
  4. if $ \exists x (\psi)$ is a subformula of $ \varphi$ for some $ L$-formula $ \psi$, then so is $ \psi[t/x]$ for any $ t$ free for $ x$ in $ \psi$.
The phrase “$ t$ is free for $ x$ in $ \psi$” means that after substituting the term $ t$ for the variable $ x$ in the formula $ \psi$, no free variables in $ t$ will become bound variables in $ \psi[t/x]$.

For example, if $ \varphi=\alpha \vee \beta$, then $ \alpha$ and $ \beta$ are subformulas of $ \varphi$. This is so because $ \alpha\vee \beta = \neg(\neg \alpha \wedge \neg \beta)$, so that $ \neg \alpha\wedge \neg\beta$ is a subformula of $ \varphi$ by applications of 1 followed by 2 above. By 3 above, $ \neg \alpha$ and $ \neg \beta$ are subformulas of $ \varphi$. Therefore, by 2 again, $ \alpha$ and $ \beta$ are subformulas of $ \varphi$.

For another example, if $ \varphi=\exists x (\exists y (x^2+y^2=1))$, then $ \exists y (t^2+y^2=1)$ is a subformula of $ \varphi$ as long as $ t$ is a term that does not contain the variable $ y$. Therefore, if $ t=y+2$, then $ \exists y ((y+2)^2+y^2=1)$ is not a subformula of $ \varphi$. In fact, if $ y\in \mathbb{R}$, the equation $ (y+2)^2+y^2=1$ is never true.

Finally, it is easy to see (by induction) that if $ \alpha$ is a subformula of $ \psi$ and $ \psi$ is a subformula of $ \varphi$, then $ \alpha$ is a subformula of $ \varphi$. “Being a subformula of” is a reflexive transitive relation on $ L$-formulas.

Remark. There is also the notion of a literal subformula of a formula $ \varphi$. A formula $ \psi$ is a literal subformula of $ \varphi$ if it is a subformula of $ \varphi$ obtained in any one of the first three ways above, or if $ \exists x (\psi)$ is a literal subformula of $ \varphi$.

Note that any literal subformula of $ \varphi$ is a subformula of $ \varphi$, for if $ \varphi=\exists x (\psi)$, then $ x$ occurs free in $ \psi$ and $ \psi=\psi[x/x]$.

In the second example above, $ \exists y (x^2+y^2=1)$ and $ x^2+y^2=1$ are both literal subformulas of $ \varphi=\exists x (\exists y (x^2+y^2=1))$.



"subformula" is owned by CWoo. [ full author list (2) | owner history (1) ]
(view preamble)

View style:

Also defines:  literal subformula
Log in to rate this entry.
(view current ratings)

Cross-references: transitive relation, Reflexive, induction, easy to see, equation, contain, bound variables, free variables, variable, term, formula, first order language
There are 4 references to this entry.

This is version 8 of subformula, born on 2002-06-02, modified 2007-11-21.
Object id is 3001, canonical name is Subformula.
Accessed 2119 times total.

Classification:
AMS MSC03B10 (Mathematical logic and foundations :: General logic :: Classical first-order logic)
 03C07 (Mathematical logic and foundations :: Model theory :: Basic properties of first-order languages and structures)

Pending Errata and Addenda
None.
[ View all 1 ]
Discussion
Style: Expand: Order:
forum policy

No messages.

Interact
post | correct | update request | add derivation | add example | add (any)