Database: Bound occurrence of a variable

Definition 17: We recursively define when a variable x occurs bound in a statement.
(a) Base cases: For any statement \phi in which x occurs, x occurs bound in the existence statement \exists x \phi .
(b) Recursion: If x occurs bound in \phi , it occurs bound in the negation \neg \phi .
(c) Recursion: If x occurs bound in at least one of \phi and \psi , then it occurs bound the conjunction (\phi \wedge \psi) .
(d) Recursion: Given a variable y , if x occurs bound in \phi then x occurs bound in \exists y \phi .

This database entry builds on the following:

  1. Terminology: Recursive definition
  2. Terminology: Class, statement
  3. Definition: Conjunction
  4. Definition: Negation
  5. Definition: Existential quantification
  6. Definition: Occurrence of a variable