Definition:Bound Occurrence

Definition

Let $\LL_1$ be the language of predicate logic.

Let $\mathbf A$ be a WFF of $\LL_1$.

Let $Q x$ be an occurrence of a quantifier in $\mathbf A$.

Any occurrence of the variable $x$ in the scope of $Q$ is called a bound occurrence.

Also known as

This page has been identified as a candidate for refactoring of basic complexity. In particular: merge this with the same bit in Definition:Bound Variable/Also known as and name appropriately Until this has been finished, please leave {{Refactor}} in the code. New contributors: Refactoring is a task which is expected to be undertaken by experienced editors only. Because of the underlying complexity of the work needed, it is recommended that you do not embark on a refactoring task until you have become familiar with the structural nature of pages of $\mathsf{Pr} \infty \mathsf{fWiki}$. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{Refactor}} from the code.

Some authors gloss over the difference between:

a bound variable: a variable which exists in a WFF only as bound occurrences

and:

a bound occurrence of a variable which may otherwise exist as a free occurrence.

Also see

• Definition:Occurrence (Formal Systems)
• Definition:Free Occurrence, the complementary notion
• Definition:Alphabetic Substitution

• Definition:Bound Variable: a variable which occurs as a bound occurrence

Sources

• 1972: A.G. Howson: A Handbook of Terms used in Algebra and Analysis ... (previous) ... (next): $\S 1$: Some mathematical language: Variables and quantifiers
• 1996: H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability: $\S 2.3$
• 2009: Kenneth Kunen: The Foundations of Mathematics ... (previous) ... (next): $\mathrm{II}.5$ First-Order Logic Syntax: Definition $\mathrm{II}.5.5$