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 (232)
Orphanage
Unclass'd
Unproven (519)
Corrections (23)
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
free and bound variables (Definition)

In the entry first-order language, I have mentioned the use of variables without mentioning what variables really are. A variable is a symbol that is supposed to range over the universe of discourse. Unlike a constant, it has no fixed value.

There are two ways in which a variable can occur in a formula: free or bound. Informally, a variable is said to occur free in a formula $ \varphi$ if and only if it is not within the “scope” of a quantifier. For instance, $ x$ occurs free in $ \varphi$ if and only if it occurs in it as a symbol, and no subformula of $ \varphi$ is of the form $ \exists x.\psi$. Here the $ x$ after the $ \exists$ is to be taken literally : it is $ x$ and no other symbol.

The set $ FV(\varphi)$ of free variables of $ \varphi$ is defined by well-founded induction on the construction of formulas. First we define $ Var(t)$, where $ t$ is a term, to be the set or all variables occurring in $ t$, and then :

$\displaystyle FV(t_1=t_2)$ $\displaystyle =$ $\displaystyle Var(t_2)\cup Var(t_2)$  
$\displaystyle FV(R(t_1,...,t_n))$ $\displaystyle =$ $\displaystyle \bigcup_{k=1}^n Var(t_k)$  
$\displaystyle FV(\neg\varphi)$ $\displaystyle =$ $\displaystyle FV(\varphi)$  
$\displaystyle FV(\varphi\vee \psi)$ $\displaystyle =$ $\displaystyle FV(\varphi)\cup FV(\psi)$  
$\displaystyle FV(\exists x(\varphi))$ $\displaystyle =$ $\displaystyle FV(\varphi)\backslash\{x\}$  

When for some $ \varphi$, the set $ FV(\varphi)$ is not empty, then it is customary to write $ \varphi$ as $ \varphi(x_1,...x_n)$, in order to stress the fact that there are some free variables left in $ \varphi$, and that those free variables are among $ x_1,...,x_n$. When $ x_1,...,x_n$ appear free in $ \varphi$, then they are considered as place-holders, and it is understood that we will have to supply “values” for them, when we want to determine the truth of $ \varphi$. If $ FV(\varphi)=\emptyset$, then $ \varphi$ is called a sentence.

If a variable never occurs free in $ \varphi$ (and occurs as a symbol), then we say the variable is bound. Bound variables can be inductively defined as well: let $ \varphi$ be a formula, then we define the set $ BV(\varphi)$ of bound variables as follows:

$\displaystyle BV(\varphi)$ $\displaystyle =$ $\displaystyle \varnothing$   if $\displaystyle \varphi$    is an atomic formula  
$\displaystyle BV(\neg\varphi)$ $\displaystyle =$ $\displaystyle BV(\varphi)$  
$\displaystyle BV(\varphi\vee \psi)$ $\displaystyle =$ $\displaystyle BV(\varphi)\cup BV(\psi)$  
$\displaystyle BV(\exists x(\varphi))$ $\displaystyle =$ $\displaystyle BV(\varphi)\cup \{x\}$  

Thus, a variable $ x$ is bound if and only if $ \exists x(\psi)$ or $ \forall x(\psi)$ is a subformula of $ \varphi$ for some $ \psi$

Note that it is possible for a variable to be both free and bound. For example, consider the following formula $ \varphi$ of the lenguage $ \{+,\cdot,0,1\}$ of ring theory :

$\displaystyle x+1=0\wedge \exists x(x+y=1) $
Then $ FV(\varphi)=\lbrace x,y\rbrace$ and $ BV(\varphi)=\lbrace x\rbrace$: the variable $ x$ occurs both free and bound. However, the following lemma tells us that we can always avoid this situation :

Lemma 1. It is possible to rename the bound variables without affecting the truth of a formula. In other words, if $ \varphi=\exists x(\psi)$, or $ \forall x(\psi)$, and $ z$ is a variable not occurring in $ \psi$, then $ \vdash \varphi\Leftrightarrow \exists z(\psi[z/x])$, where $ \psi[z/x]$ is the formula obtained from $ \psi$ by replacing every free occurrence of $ x$ by $ z$.



"free and bound variables" is owned by CWoo. [ full author list (3) | owner history (2) ]
(view preamble | get metadata)

View style:

Also defines:  free variable, bound variable
Log in to rate this entry.
(view current ratings)

Cross-references: occurrence, theory, ring, sentence, order, term, well-founded induction, subformula, quantifier, formula, occur in, fixed, constant, universe of discourse, range, variables
There are 13 references to this entry.

This is version 13 of free and bound variables, born on 2002-06-02, modified 2007-11-14.
Object id is 3008, canonical name is FreeAndBoundVariables.
Accessed 4397 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 5 ]
Discussion
Style: Expand: Order:
forum policy
Space of hilbert space linear operators by ratboy on 2004-06-27 23:48:05
If F and G are hilbert spaces, is the banach space L(F,G) of bounded linear operators from F to G necessarily a hilbert space?


[ reply | up ]
Interact
post | correct | update request | add derivation | add example | add (any)