1 公理

1.1 andの縦表記

abbr … \(\begin{cases} P_{1} \\ \vdots \\ P_{\tt n} \end{cases}\) ≈ \(( P_{1} ) , \cdots , ( P_{\tt n} )\)

1.2 可換半環と帰納法

自然数を作らず、\(\mathbb{M}\) が \(0\)・\(1\)・\(+\)・\(\cdot\) について可換半環であること、\(x \mapsto x+1\) による帰納法、\(2 = 1 + 1\) だけを公理として置きます。
添字 \(n\) も値も同じ \(\mathbb{M}\) にあるので、任意の可換半環に値を取り自然数で添字づけた数列、という一般化とは異なります。
word(,s) … \(\mathbb{M}\)  \(0\)
word(,s) … \({\tt n}\)
word(ss,s) … \(+\)  \(\cdot\)
CSR𝕄 … \(\begin{cases} 0 \in \mathbb{M} , 1 \in \mathbb{M} \\ x , y \in \mathbb{M} \Longrightarrow x + y \in \mathbb{M} , x \cdot y \in \mathbb{M} \\ x , y , z \in \mathbb{M} \Longrightarrow x + y = y + x , x + ( y + z ) = ( x + y ) + z , x + 0 = x \\ x , y , z \in \mathbb{M} \Longrightarrow x \cdot y = y \cdot x , x \cdot ( y \cdot z ) = ( x \cdot y ) \cdot z , x \cdot 1 = x \\ x , y , z \in \mathbb{M} \Longrightarrow x \cdot ( y + z ) = x \cdot y + x \cdot z , x \cdot 0 = 0 \end{cases}\)
IND𝕄 … \(0 \in C , \forall m \in \mathbb{M} . ( m \in C \Longrightarrow m + 1 \in C ) \Longrightarrow \mathbb{M} \subset C\)
N2 … \(2 = 1 + 1\)

2 主定理

word(ss,s)F … \(\)
\(s(n)\) を初項 \(a\)、公差 \(d\) の等差数列の最初の \(n\) 項の和とします。
ここでは \(s\) を \(s(0) = 0\) と漸化式を満たす関数として仮定します（\(a\)・\(d\) は\(\mathbb{M}\) の元）。そのような \(s\) が存在することは示しません。したがって主定理は「そのような \(s\) があれば」という条件付きの形です（\(s\) が無ければ何も言っていません）。
\(\begin{cases} a , d \in \mathbb{M} \\ s ( 0 ) = 0 \\ \forall i \in \mathbb{M} . s ( i + 1 ) = s ( i ) + ( a + i \cdot d ) \end{cases} , n \in \mathbb{M} \Longrightarrow 2 \cdot s ( n + 1 ) = ( n + 1 ) \cdot ( 2 \cdot a + n \cdot d )\) \(\blacktriangleleft\) CSR𝕄 ，IND𝕄 ，N2