Database: Free occurrence of a variable

Definition 21: We recursively define when a variable x is said to occur free in a statement.
(a) Base cases: If x occurs in a membership statement, then it occurs free in that membership statement.
(b) Recursion: If x occurs free in \phi , then it occurs free in the negation \neg \phi .
(c) Recursion: If x occurs free in at least one of \phi and \psi , then it occurs free the conjunction (\phi \wedge \psi) .
(d) Recursion: Given any variable y distinct from x , if x occurs free in \phi then x occurs free in the existence statement \exists y \phi .

This database entry builds on the following:

  1. Terminology: Class, membership
  2. Terminology: Statement
  3. Definition: Conjunction
  4. Definition: Negation
  5. Definition: Existential quantification
  6. Definition: Occurrence of a variable
  7. Terminology: Recursion, structural induction