FreeAndBoundVariables 2002-06-02 20:46:16 2007-11-14 17:56:59 Definition free variable bound variable % this is the default PlanetMath preamble. as your knowledge % of TeX increases, you will probably want to edit this, but % it should be fine as is for beginners. % almost certainly you want these \usepackage{amssymb} \usepackage{amsmath} \usepackage{amsfonts} \newcommand{\br}{[\![} \newcommand{\rb}{]\!]} \newcommand{\oq}{\text{``}} \newcommand{\cq}{\text{''}} \newcommand{\im}{\mathbf{Im}} \newcommand{\dom}{\mathbf{Dom}} \newcommand{\Or}{\vee} \newcommand{\Implies}{\Rightarrow} \newcommand{\Iff}{\Leftrightarrow} \newcommand{\proves}{\vdash} \renewcommand{\And}{\wedge} \newcommand{\Sup}{\bigwedge} \newcommand{\Inf}{\bigvee} \newcommand{\Z}{\mathbb{Z}} \newcommand{\F}{\mathbb{F}} \newcommand{\Q}{\mathbb{Q}} \newcommand{\R}{\mathbb{R}} \newcommand{\C}{\mathbb{C}} \newcommand{\Nat}{\mathbb{N}} \newcommand{\M}{\mathfrak{M}} \newcommand{\N}{\mathfrak{N}} \newcommand{\A}{\mathfrak{A}} \newcommand{\B}{\mathfrak{B}} \newcommand{\K}{\mathfrak{K}} \newcommand{\G}{\mathbb{G}} \newcommand{\Def}{\overset{\operatorname{def}}{:=}} \newcommand{\spec}{\text{{\bf Spec}}} \newcommand{\stab}{\text{{\bf Stab}}} \newcommand{\ann}{\text{{\bf Ann}}} \newcommand{\irr}{\text{{\bf Irr}}} \newcommand{\qt}{\text{{\bf Qt}}} \newcommand{\st}{\mathcal{Qt}} \newcommand{\ro}{\mathbf{r.o.}} \newcommand{\Endo}{\text{{\bf End}}} \newcommand{\mat}{\text{{\bf Mat}}} \newcommand{\der}{\text{{\bf Der}}} \newcommand{\rad}{\text{{\bf Rad}}} \newcommand{\trd}{\text{{\bf tr.d.}}} \newcommand{\cl}{\text{{\bf acl}}} \newcommand{\Int}{\text{{\bf int}}} \newcommand{\V}{\mathbb{V}} \newcommand{\D}{\mathbf{D}} \newcommand{\del}{\partial} \renewcommand{\O}{\mathcal{O}} \newcommand{\aut}{\mathbf{Aut}} \newcommand{\height}{\text{\bf Height}} \newcommand{\coheight}{\text{\bf Co-height}} \newcommand{\lcm}{\operatorname{lcm}} \newcommand{\Gal}{\operatorname{Gal}} \newcommand{\x}{\mathbf{x}} \newcommand{\y}{\mathbf{y}} \newcommand{\inner}[2]{\langle #1|#2\rangle} \renewcommand{\r}{{r}} \renewcommand{\t}{{t}} \newcommand{\restr}{\upharpoonright} \newcommand{\Matrix}[4]{\left(\begin{array}{cc} #1 & #2 \\ #3 & #4 \end{array}\right)} \PMlinkescapeword{bound} In the entry \PMlinkname{first-order language}{TermsAndFormulas}, 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: {\bf free} or {\bf bound}. Informally, a variable is said to occur {\em 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 : \begin{eqnarray*} FV(t_1=t_2) & = & Var(t_2)\cup Var(t_2) \\ FV(R(t_1,...,t_n)) & = & \bigcup_{k=1}^n Var(t_k) \\ FV(\neg\varphi) & = & FV(\varphi) \\ FV(\varphi\Or\psi) & = & FV(\varphi)\cup FV(\psi) \\ FV(\exists x(\varphi)) & = & FV(\varphi)\backslash\{x\} \end{eqnarray*} 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 {\bf 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 {\bf sentence}. If a variable never occurs free in $\varphi$ (and occurs as a symbol), then we say the variable is {\bf 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: \begin{eqnarray*} BV(\varphi) & = & \varnothing \quad \mbox{if }\varphi \mbox{ is an atomic formula}\\ BV(\neg\varphi) & = & BV(\varphi) \\ BV(\varphi\Or\psi) & = & BV(\varphi)\cup BV(\psi) \\ BV(\exists x(\varphi)) & = & BV(\varphi)\cup \{x\} \end{eqnarray*} 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 : \begin{displaymath} x+1=0\And\exists x(x+y=1) \end{displaymath} 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 : {\bf 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 $\proves \varphi\Iff\exists z(\psi[z/x])$, where $\psi[z/x]$ is the formula obtained from $\psi$ by replacing every free occurrence of $x$ by $z$.