有限集合 \(S\) 上の対合 \(F\)（\(F\) で閉じていて、\(F(F(s)) = s\)）の不動点の個数 \(r\) と \(|S| = n\) について、\(n = r + 2j\)。Zagier の証明（20）で \(|S|\) の偶奇を調べるのに使う。

1 準備

1点を除く：個数 \(k+1\) の集合から1点を除くと個数 \(k\)。
Lrm … \(k \in \mathbb{M} , X \stackrel{\#}= k + 1 , x \in X \Longrightarrow X \mathop\setminus \{ x \} \stackrel{\#}= k , X \mathop\setminus \{ x \} \subset X , x \notin X \mathop\setminus \{ x \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s

2 対合の不動点の個数

個数 \(k\) の集合から相異なる2点 \(s, t\) を除くと個数 \(k - 2\)。
Lp1 … \(k \in \mathbb{M} , S \stackrel{\#}= k , s \in S , t \in S , \neg s = t \Longrightarrow \exists m \in \mathbb{M} . k = ( m + 1 ) + 1 , ( S \mathop\setminus \{ s \} ) \mathop\setminus \{ t \} \stackrel{\#}= m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，∈∖1 ，Lrm
不動点でない \(s\) とその像 \(t\) を除いても、\(F\) で閉じている・不動点は残る。
Lp2 … \(\forall s , t , u \, ( \langle s , t \rangle \in F , \langle s , u \rangle \in F \Longrightarrow t = u ) , \forall s , t \, ( \langle s , t \rangle \in F \Longrightarrow \langle t , s \rangle \in F ) , \langle s , t \rangle \in F , \neg s = t , \forall u \in S . \forall v \, ( \langle u , v \rangle \in F \Longrightarrow v \in S ) \Longrightarrow \forall u \in ( S \mathop\setminus \{ s \} ) \mathop\setminus \{ t \} . \forall v \, ( \langle u , v \rangle \in F \Longrightarrow v \in ( S \mathop\setminus \{ s \} ) \mathop\setminus \{ t \} )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，∈∖1 ，Lrm
Lp3 … \(\forall s , t , u \, ( \langle s , t \rangle \in F , \langle s , u \rangle \in F \Longrightarrow t = u ) , \forall s , t \, ( \langle s , t \rangle \in F \Longrightarrow \langle t , s \rangle \in F ) , \langle s , t \rangle \in F , \neg s = t , \neg \langle s , s \rangle \in F , \forall u \in R . \langle u , u \rangle \in F , R \subset S \Longrightarrow R \subset ( S \mathop\setminus \{ s \} ) \mathop\setminus \{ t \}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，∈∖1 ，Lrm
すべて不動点なら \(S = R\)。
Lp4 … \(S \subset U , R \subset S , \forall u \in R . \langle u , u \rangle \in F , \forall u \in S . \langle u , u \rangle \in F \Longrightarrow u \in R , \forall u \in S . \langle u , u \rangle \in F , n , r \in \mathbb{M} , S \stackrel{\#}= n , R \stackrel{\#}= r \Longrightarrow n = r\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，∈∖1 ，Lrm ，Lp1 ，Lp2 ，Lp3
帰納法の1歩（個数が小さいときの主張から）。
Lp5 … \(\forall s \in U . \exists t \, \langle s , t \rangle \in F , \forall s , t , u \, ( \langle s , t \rangle \in F , \langle s , u \rangle \in F \Longrightarrow t = u ) , \forall s , t \, ( \langle s , t \rangle \in F \Longrightarrow \langle t , s \rangle \in F ) , \forall u \in R . \langle u , u \rangle \in F , n , r \in \mathbb{M} , R \stackrel{\#}= r , \forall z \in \mathbb{M} . ( z < n \Longrightarrow \forall S \, ( S \stackrel{\#}= z , S \subset U , R \subset S , \forall u \in S . \forall v \, ( \langle u , v \rangle \in F \Longrightarrow v \in S ) , \forall u \in S . ( \langle u , u \rangle \in F \Longrightarrow u \in R ) \Longrightarrow \exists j \in \mathbb{M} . z = r + 2 \cdot j ) ) , S \stackrel{\#}= n , S \subset U , R \subset S , \forall u \in S . \forall v \, ( \langle u , v \rangle \in F \Longrightarrow v \in S ) , \forall u \in S . ( \langle u , u \rangle \in F \Longrightarrow u \in R ) \Longrightarrow \exists j \in \mathbb{M} . n = r + 2 \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，∈∖1 ，Lrm ，Lp1 ，Lp2 ，Lp3 ，Lp4
有限集合の対合：個数 \(n\) は不動点の個数 \(r\) と偶数の和（\(n\) についての強い帰納法）。
Lpar … \(\forall s \in U . \exists t \, \langle s , t \rangle \in F , \forall s , t , u \, ( \langle s , t \rangle \in F , \langle s , u \rangle \in F \Longrightarrow t = u ) , \forall s , t \, ( \langle s , t \rangle \in F \Longrightarrow \langle t , s \rangle \in F ) , \forall u \in R . \langle u , u \rangle \in F , n , r \in \mathbb{M} , R \stackrel{\#}= r , S \stackrel{\#}= n , S \subset U , R \subset S , \forall u \in S . \forall v \, ( \langle u , v \rangle \in F \Longrightarrow v \in S ) , \forall u \in S . ( \langle u , u \rangle \in F \Longrightarrow u \in R ) \Longrightarrow \exists j \in \mathbb{M} . n = r + 2 \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，∈∖1 ，Lrm ，Lp1 ，Lp2 ，Lp3 ，Lp4 ，Lp5