Replacement Theorem and Foundation of Mathematics

2021-02-24, updated 2021-02-24 next - previous

This note only to show with some examples that the Replacement Theorem of first-order logic is undoubtedly crucial in Foundations of Mathematics.

Fitting gave the following definitions of the Replacement Theorem and the Implicational Replacement Theorem for first-order logic [1, pp. 204–206]:

Let \(\Phi(A)\), X and Y be first-order formulas of language L, where A is an atomic formula . Let M be a model for L. If \(X \equiv Y\) is true in M, then \(\Phi(X) \equiv \Phi(Y)\) is also true in M.

Let \(\Phi(A)\) be a formula in which the formula A has only positive occurrences. Let X and Y be first-order formulas of language L, where A is an atomic formula . Let M be a model for L. If \(X \to Y\) is true in M, then \(\Phi(X) \to \Phi(Y)\) is also true in M.

What Fitting calls “Replacement Theorem” [1, pp. 21–22, 204–205] is also called “principle of substitution of logical equivalents” by Barwise and Etchemendy [2, pp. 118, 276–277].

Equality is an equivalence relation, it is reflexive, symmetric and transitive; in this respect “\(X \equiv Y\)” and “\(X = Y\)” can be considered as synonymous.

In the following example \(\Phi = card\), Y and X are respectively the first-order formulas which define respectively a counting a set of n elements and the exponentiation \(2^{n}\).

Cantor's theorem

In Cantorian set theory, the set of all subsets of any set \(\alpha\) (that is the power set of \(\alpha\) i.e. \(\mathcal{P}(\alpha)\)) has a cardinality which is strictly greater than the cardinality of \(\alpha\) itself, in formula: \[card(\mathcal{P}(\alpha)) > card(\alpha)\]

  1. The cardinality any set \(\alpha\) is the number n of the elements of \(\alpha\): \[card(\alpha) = n\]
  2. The cardinal number of power set of any Cantorian set \(\alpha\) (that is the set of subsets of \(\alpha\)) is: \[card(\mathcal{P}(\alpha)) = 2^{n}\]
  3. Note that for any non-negative integer n: \[2^{n} > n\]
  4. Therefore, by replacement: \[card(\mathcal{P}(\alpha)) > card(\alpha)\]

The structure of the proof above is:

\begin{equation} \label{eq:8} \Phi(Y) = b \end{equation} \begin{equation} \label{eq:9} \Phi(X) = a \end{equation} \begin{equation} \label{eq:10} R(a,b) \end{equation}


\begin{equation} \label{eq:11} R(\Phi(X), \Phi(Y)) \end{equation}

R being the order relation >.

Cantor's paradox.

The power set of set V of all sets has a cardinality strictly greater than the cardinality of V, therefore the set of all sets is not the set of all sets.

By replacement of \(\alpha\) by V in the proof above.

Specker's theorem.

The use of equivalence relations and replacements in proofs for NF and NFU is very frequent. See for example the proof of Specker’s theorem given by Holmes [3, p. 133] where the equality symbol is used 12 times. In the proof of proposition 2.3.20, Forster [4, pp. 68–69] wrote:

\([\dots]\) by substitutivity of the biconditional we can ensure that \([\dots]\)

which is an explicit use of the Replacement Theorem.


M. Fitting, First-Order Logic and Automated Theorem Proving, 2nd ed. Springer, 1990.
J. Barwise and J. Etchemendy, Language, Proof and Logic, 2nd ed. CSLI Publications, 2011.
M. R. Holmes, Elementary Set Theory with a Universal Set, vol. 10. Louvain-la-Neuve, Belgium: Academia-Bruylant, 1998.
T. E. Forster, Set Theory with a Universal Set: Exploring an Untyped Universe, 2nd ed. Oxford, U.K.: Clarendon Press, 1995.

Made with Emacs 27.1 (Org mode 9.4.4) and with org-export-head, a blog exporter.

The css file of this blog is mainly the result of Zhitao Gong's work.

orgmode emacs isso debian mxlinux