加法閉な対称集合は、倍数集合である

途中までだ。

A⊆N が、次の3つの性質を持つとする。

1. Aは空ではない ---(1)
2. n∈A ⇒ -n∈A ---(2)
3. n, m∈A ⇒ n+m∈A ---(3)

このとき、非負整数kがあって、

• n∈A ⇔ nはkの倍数 ---(4)

上のパラグラフをまとめると、

• $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4)

しかし、条件は全称が付いているはずだから、

1. Aは空ではない ---(1)
2. ∀n:N. n∈A ⇒ -n∈A ---(2)
3. ∀n, m:N. n, m∈A ⇒ n+m∈A ---(3)

また、自由変数AはPow(N)を走るので、

• ∀A st A⊆N.( $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4) )

お膳立てをすると

   |- ∀A st A⊆<b>N</b>.( $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4) )
  --------------------------------------------------------------------
   A⊆<b>N</b> |-  $(1)∧$(2)∧$(3) ⇒ ∃k st 非負整数.$(4)
  --------------------------------------------------------------------
   A⊆<b>N</b>, $(1)∧$(2)∧$(3) |- ∃k st 非負整数.$(4)
  --------------------------------------------------------------------
   A⊆<b>N</b>, $(1), $(2), $(3) |- ∃k st 非負整数.$(4)

準備： 部分関数 nnmin : Pow(N)⊇→N_≧0 の定義

• nnmin(A) := εx∈N.( (x∈A∧x≧0)∧∀k∈N.((k∈A∧k≧0)⇒n≦k) )

これで、形式上は定義されているが、well-definedかどうかは分からない。Aの範囲を限定して、そこでは全域関数になることを示す必要がある。

続きはまた後で。