Predicate Calculus (0)

The symbol '∈' is a predicate according to set theory. It reads "is a member of" or "is an element of". A sequence of three symbols containing a variable or a constant, then the predicate ∈, and again a variable or a constant is an atomic formula. The only constant in set theory is Ø. So, there exist four atomic formulae.

Ø ∈ Ø , Ø ∈ X , X ∈ Ø , X ∈ Y

The truth value of X ∈ Y is indeterminate because different substitutions for the variables X and Y yield different values. 

⊨P indicates that the formula P is universally valid (is true regardless of its variables) and there exists a proof of P that may require not only the use of propositional calculus but also predicate calculus.

A variable is an individual variable if and only if it occurs in an atomic formula involving predicates. A variable is a propositional variable if and only if it occurs in a propositional form involving logical connectives.

The symbols ∀ and ∃ are quantifiers and only individual variables are permitted to immediately follow these symbols. Example: If P is a logical formula and X is an individual variable then ∀X(P) and ∃X(P) are valid constructions. 

If X is an individual variable that occurs in a logical formula P, then X is bound in P if and only if X occurs immediately after a quantifier, or between ∀X( or ∃X( and its corresponding parenthesis ). X is free in P if and only if X is not bound in P. A logical formula is closed if and only if it does not contain any free variables. A logical sentence is a closed logical formula.

Subf(X,Z)P is the formula that results from substituting every free occurrence of X in P by Z assuming that X is a variable that does not already occur in P. Subb(X,Z)P is the formula that results from substituting every bound occurrence of X in P by Z.