素数 \(p = 4k + 1\) は \(x^2 + y^2\) の形に書ける（Zagier の一文証明）。\(S = \{(x,y,z) : x^2 + 4yz = p\}\)（正の整数）の上に対合 \(f\)（不動点は \((1,1,k)\) だけ）と \(g(x,y,z) = (x,z,y)\) がある。有限集合の対合では「個数 ≡ 不動点の個数（mod 2）」だから \(|S|\) は奇数で、\(g\) にも不動点（\(y = z\)、\(p = x^2 + (2y)^2\)）がある。

1 組み立て

1点だけの集合は個数 1。
LR1 … \(\forall u \, ( u \in R \Longleftrightarrow u = a ) \Longrightarrow R \stackrel{\#}= 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
\(F\) に Lpar を当てる：不動点は \((1,1,k)\) の1個なので \(|S|\) は奇数。
LPF … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , \forall u \, ( u \in R \Longleftrightarrow u = \langle 1 , \langle 1 , k \rangle \rangle ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , \exists n \in \mathbb{M} . S \stackrel{\#}= n \Longrightarrow \exists n \in \mathbb{M} . \exists j \in \mathbb{M} . S \stackrel{\#}= n , n = 1 + 2 \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LmS ，LF1 ，LF2 ，LF3 ，LF4 ，LFixI ，LFixR ，Lpar ，LR1
集合 \(R \subset S\) も有限。
LRfin … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{M} , R \subset S \Longrightarrow \exists k \in \mathbb{M} . R \stackrel{\#}= k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，L4m ，LmS ，Lsl ，LbX ，LbY ，Lcn ，LSsub
\(g\) 側：\(|S|\) は奇数なので \(g\) の不動点（\(y = z\)）が在り、\(p = x^2 + (2y)^2\)。
LPG … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , \forall u \, ( u \in R \Longleftrightarrow u \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . u = \langle x , \langle y , y \rangle \rangle ) , p \in \mathbb{M} , \exists n \in \mathbb{M} . \exists j \in \mathbb{M} . S \stackrel{\#}= n , n = 1 + 2 \cdot j \Longrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . p = x \cdot x + 4 \cdot ( y \cdot y )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，L4m ，LmS ，Lsl ，LbX ，LbY ，Lcn ，LSsub ，LRfin ，LG1 ，LG2 ，LG3 ，LG4 ，LG5 ，Lpar

2 特性式を使わない形の閉性

閉じていること（F の特性なしの形）。
LF1D … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{P} , s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) \Longrightarrow t \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，Lsq ，L4m ，IA ，IB ，IC ，Lpo ，Lns ，Lex1 ，Lex2 ，Lcl1 ，Lcl2 ，Lcl3 ，Lcl4 ，Lcls ，LxAB ，LxAC ，LxBC ，LmS ，Lnp ，LF1A ，LF1B ，LF1C
閉じていること（G の特性なしの形）。
LG1D … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle \Longrightarrow t \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，LmS ，Lnp
集合 \(S, F, G, R, T\) が特徴づけを満たすとき \(p = x^2 + (2y)^2\)（LPF と LPG をつなぐ）。
LFin … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , \forall s , t \, ( \langle s , t \rangle \in F \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) , \forall s , t \, ( \langle s , t \rangle \in G \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) , \forall u \, ( u \in R \Longleftrightarrow u = \langle 1 , \langle 1 , k \rangle \rangle ) , \forall u \, ( u \in T \Longleftrightarrow u \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . u = \langle x , \langle y , y \rangle \rangle ) , p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} , \exists n \in \mathbb{M} . S \stackrel{\#}= n \Longrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . p = x \cdot x + 4 \cdot ( y \cdot y )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LPF ，LPG ，LF1 ，LG1 ，LRfin ，Lℙ

3 集合を具体的に作る

\(S, F, G, T\) を \(\{ x \mid \cdots \}\) の形の集合として取り、特徴づけを示す。
LCS … \(p \in \mathbb{M} \Longrightarrow \forall s \, ( s \in ( \{ s \mid \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p \} ) \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，L4m ，LmS ，Lsl ，LbX ，LbY ，Lcn
LCF … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{P} \Longrightarrow \forall s , t \, ( \langle s , t \rangle \in ( \{ w \mid \exists s , t \, ( w = \langle s , t \rangle , s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) ) \} ) \Longleftrightarrow s \in S , ( \exists x \in \mathbb{N} . \exists z \in \mathbb{N} . \exists w \in \mathbb{N} . s = \langle x , \langle ( ( x + z ) + w ) , z \rangle \rangle , t = \langle ( x + 2 \cdot z ) , \langle z , w \rangle \rangle \mathbin{\rm o\!r} \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . \exists a \in \mathbb{N} . \exists c \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , 2 \cdot y = x + a , x + z = y + c , t = \langle a , \langle y , c \rangle \rangle \mathbin{\rm o\!r} \exists y \in \mathbb{N} . \exists b \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle ( 2 \cdot y + b ) , \langle y , z \rangle \rangle , t = \langle b , \langle ( ( y + b ) + z ) , y \rangle \rangle ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LF1D ，LmS
LCG … \(\forall s \, ( s \in S \Longleftrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , x \cdot x + 4 \cdot ( y \cdot z ) = p ) , p \in \mathbb{P} \Longrightarrow \forall s , t \, ( \langle s , t \rangle \in ( \{ w \mid \exists s , t \, ( w = \langle s , t \rangle , s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle ) \} ) \Longleftrightarrow s \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . \exists z \in \mathbb{N} . s = \langle x , \langle y , z \rangle \rangle , t = \langle x , \langle z , y \rangle \rangle )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，LG1D ，LmS
LCT … \(\forall u \, ( u \in ( \{ u \in S \mid \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . u = \langle x , \langle y , y \rangle \rangle \} ) \Longleftrightarrow u \in S , \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . u = \langle x , \langle y , y \rangle \rangle )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
正の整数の2倍は正の整数。
L2n … \(y \in \mathbb{N} \Longrightarrow 2 \cdot y \in \mathbb{N}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

4 組み立て（Zagier）

以上をまとめる：\(S\) の個数は奇数なので \(g\) に不動点が在り、\(p = x^2 + (2y)^2\)。
Zagier … \(p \in \mathbb{P} , p = 4 \cdot k + 1 , k \in \mathbb{M} \Longrightarrow \exists x \in \mathbb{N} . \exists y \in \mathbb{N} . p = x ^ 2 + y ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，L44 ，L2n ，LSfin ，LFin ，LCS ，LCF ，LCG ，LCT ，Lℙ ，↑𝕄