The Language of ZFC
Symbols
The basic symbols of the language are as follows:
Variables:
Predicate symbols:
- Equality:
- Membership:
Logical connectives:
- Negation:
- Implication:
Quantifier:
- Universal quantifier:
No function symbols or constant symbols are included in the basic language of ZFC.
Formulas
Formulas are defined inductively.
Atomic Formulas
The atomic formulas are:
Compound Formulas
If and are formulas, then the following are also formulas:
There are no other formulas beyond those generated by these rules.
Axioms of Predicate Logic
The deductive system for ZFC is based on a Hilbert-style axiom system for first-order predicate logic. The logical axioms include:
- , where the term remains free after substitution for the free occurrences of in . In particular, must not become bound by a quantifier .
- , provided that does not occur free in .
These axioms govern the logical behavior of implication, negation, and universal quantification.
Formal Proofs
Definition of Proof
Let be a set of formulas and a formula. We say that is provable from , written
if there exists a finite sequence of formulas
such that , and for each index , one of the following holds:
- is an axiom of predicate logic; or
- ; or
- there exist indices such that is of the form (i.e., follows from and by modus ponens); or
- there exists an index such that (universal generalization).