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
sections
Encyclopædia
Papers
Books
Expositions

meta
Requests (198)
Orphanage
Unclass'd
Unproven (490)
Corrections (7)
Classification

talkback
Polls
Forums
Feedback
Bug Reports

downloads
Snapshots
PM Book

information
News
Docs
Wiki
ChangeLog
TODO List
Legalese
About
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 MSC: 03B10 (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)