|
|
|
Viewing Version
10
of
'free and bound variables'
|
[ view 'free and bound variables'
|
back to history
]
| Title of object: |
free and bound variables |
| Canonical Name: |
FreeAndBoundVariables |
| Type: |
Definition |
| Created on: |
2002-06-02 20:46:16 |
| Modified on: |
2004-01-24 07:42:28 |
| Classification: |
msc:03B10, msc:03C07 |
Preamble:
% 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)} |
Content:
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}. A variable $x$ is bound if and only if $\exists x(\psi)$ or $\forall x(\psi)$ is a subformula of $\varphi$ for some $\psi$
The problem with this definition is that a variable can occur both free and bound in the same formula. For example, consider the following formula of the lenguage $\{+,\cdot,0,1\}$ of ring theory :
\begin{displaymath}
x+1=0\And\exists x(x+y=1)
\end{displaymath}
The variable $x$ occurs both free and bound here. 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$. |
|
|
|
|
|
