All-inclusive

from Wikipedia, the free encyclopedia

A universal closure is a syntactic operation in predicate logic by which universal quantification, ie quantification using the universal quantifier ∀, is carried out for all so-called free variables of a formula F. Formally:

  • The all-inclusive ∀ (F) of a formula F is
  1. F, if F is closed (i.e. does not have free variables)
  2. ∀x 1 ... x n F if x 1 , ..., x n are free variables in F.

The all-inclusive can also be defined for formula quantities:

  • Let S be a set of formulas. Then the universal closure ∀S is the set ∀S: = {∀ (F) | F∈S}.

The analog to Allabschluss operation with the existential ∃'s existence completion .

Equivalence and general validity of the all-inclusive

The all-inclusive statement is generally not logically equivalent to the original formula, ie

  • F ∀ (F) does not apply to all F.

However, it preserves the generality of a formula, ie

  • If F is generally valid, then ∀ (F) is also generally valid.