Predicate calculus is concerned with formulas that involve variables that can be quantified. Some common quantifiers are:
A related topic is substitution. [A/x] φ means that A is being substituted for x into the expression φ.
Axioms 1-3 are the axioms of logic.