Database: A variable is freely substitutable for a variable not occurring in the statement

Corollary 40: Given a statement \phi in which some variable y does not occur, each variable x is freely substitutable for y in \phi .

Proof: By [31], if y does not occur in \phi , then y does not occur quantified in \phi . The desired result follows by [39]. \square

This database entry builds on the following:

  1. Terminology: Class, statement
  2. Terminology: Class, statement
  3. Definition: Occurrence of a variable
  4. Definition: Occurrence of a variable
  5. Definition: Quantified occurrence of a variable
  6. Definition: Freely substitutable variable
  7. Definition: Freely substitutable variable
  8. Corollary: A variable not occurring in a statement does not occur quantified in the statement
  9. Lemma: A variable is freely substitutable for a variable not occurring quantified in the statement