原始的な帰納法のみでNにおける∈の無反射性を示す

\(\forall n\in\mathbb{N}[n\notin n]\)を、原始的な数学的帰納法のみを用いて示す。以下、\(n'\)は\({\rm Suc}(n)=n\cup\{n\}\)を意味する。
\(\beta(n):\forall k\in n'[k\notin k]\)と置くと、\(n\in n'\)により、各\(\beta(n)\)は\(n\notin n\)を含意する。そこで、\(\forall n\in\mathbb{N}[\beta(n)]\)を帰納法によって示せばよい。
まず\(\beta(\varnothing)\)は\(\varnothing\notin\varnothing\)により成立する。
\(\beta(n)\)を仮定し、\(k\)として\(n'\)を選べば\[n'\in n'\rightarrow n'\notin n'\]が得られるが、これは\(n'\notin n'\)のことである。したがって\(\beta(n')\)すなわち\(\beta(n)\wedge n'\notin n'\)も成立する。■