# Connexions

You are here: Home » Content » First-Order Logic: bound variables, free variables

### Lenses

What is a lens?

#### Definition of a lens

##### Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

##### What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

##### Who can create a lens?

Any individual member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

#### Affiliated with (What does "Affiliated with" mean?)

This content is either by members of the organizations listed or about topics related to the organizations listed. Click each link to see a list of all content affiliated with the organization.
• Rice Digital Scholarship

This module is included in aLens by: Digital Scholarship at Rice UniversityAs a part of collection: "Intro to Logic"

Click the "Rice Digital Scholarship" link to see all content affiliated with them.

### Recently Viewed

This feature requires Javascript to be enabled.

# First-Order Logic: bound variables, free variables

In the previous examples we often re-used variable names, even within the same formula. This shouldn't be surprising or confusing, since we do the same thing in programs (another formal language). In fact, the same notions of bound and free variables occur in both situations. An occurrence of variable xx is bound if it is in the body of a quantifier xx … or xx …. Otherwise, the occurrence is free.

For example, in x:likesxyx likes x y , the variable yy is free but xx is not. So this is a statement about yy; we can't evaluate this to true/false until we get some context for yy. It's useful as a subpart for some bigger formula.

## A possible misunderstanding:

The concept “x free in φφ” does not talk about the context of φφ. So don't confuse it with “well, over on this part of the page, φφ happens to occur as the sub-part of another formula containing x: x , so xx really is bound.” (Just as 7 is prime, even though people sometimes use 7 in the context of 7+1.) Whether xx is free in a φφ can be determined by a function isFreexφ isFree x φ , needing no other information to produce an answer.

Looking back at our previous examples, we can see that many of the formulas we made had no free variables — all variables were bound by some quantifier in the formula. The truth of such formulas depends only on the interpretation and not on any additional knowledge about what any free variables refer to. Thus, these formulas are common and important enough that we give them a special name, sentences.

A given variable name can actually have both bound and free occurrences within the same formula, as in Rxx:¬Rx Rx x R x . (This formula about xx is satisfiable: it says that RR is true about xx, but isn't true about everything.) In essence, there are two different underlying variables going on, but they each happen to have the same name; from scope it can be decided which one each occurence refers to. In programming language terms, we'd say that the inner xx (the local variable) shadows the outer xx (the enclosing variable). In these terms, free variables in logic correspond to global variables in programs.

Clearly x:Rx x R x is always equivalent to y:Ry y R y ; variable names are entirely arbitrary (except maybe for their mnemonic value). So the previous formula might be more clearly re-written as Rxy:¬Ry Rx y R y . (This careful re-writing while respecting a variable's scope is called αα-renaming.) Even if 17 quantifiers each used the same variable (name) xx, we could carefully αα-renaming 17 times, and end up with an equivalent formula where all quantifiers use distinct variables. This will be useful to avoid potential confusion, especially in the upcoming inference rules, where we'll be introducing and eliminating quantifiers.

## Example 1

The formula x:Axx:Bxx:Cx x A x x B x x C x is equivalent to the more readable x:Axy:Byz:Cz x A x y B y z C z .

## Content actions

PDF | EPUB (?)

### What is an EPUB file?

EPUB is an electronic book format that can be read on a variety of mobile devices.

My Favorites (?)

'My Favorites' is a special kind of lens which you can use to bookmark modules and collections. 'My Favorites' can only be seen by you, and collections saved in 'My Favorites' can remember the last module you were on. You need an account to use 'My Favorites'.

| A lens I own (?)

#### Definition of a lens

##### Lenses

A lens is a custom view of the content in the repository. You can think of it as a fancy kind of list that will let you see content through the eyes of organizations and people you trust.

##### What is in a lens?

Lens makers point to materials (modules and collections), creating a guide that includes their own comments and descriptive tags about the content.

##### Who can create a lens?

Any individual member, a community, or a respected organization.

##### What are tags?

Tags are descriptors added by lens makers to help label content, attaching a vocabulary that is meaningful in the context of the lens.

| External bookmarks