1 準備

word(ss,s)F … \(\)
列 \(f\) の1点の値だけを変えた列があること（upd𝕄・73 と同じ）を仮定します。
upd𝕄 … \(\exists g \, ( g ( k ) = p , \forall i \in \mathbb{M} . ( i \neq k \Longrightarrow g ( i ) = f ( i ) ) )\)
長さ \(P\) の有限列を対 \(\langle x,P\rangle\) で表します。\(x \upuparrows P\)：増加列。\(\langle x,P\rangle \sqsubseteq \langle v,L\rangle\)：\(x\) の値はどれも \(v\) の値。\(c \models_0 \langle x,P\rangle\)：色付け \(c\) で \(x\) のどの2点も赤（値 0）。\(\models_1\) は青（値 \(\ne 0\)）。
word(ss,s)F … \(\mathsf{pr}\)
abbr … \(\langle X , Y \rangle\) ≈ \(\mathsf{pr} ( X , Y )\)
word(ss,p) … \(\upuparrows\)  \(\sqsubseteq\)  \(\models_0\)  \(\models_1\)
⇈. … \(x \upuparrows P \Longleftrightarrow \forall i \in \mathbb{M} . ( i < P \Longrightarrow x ( i ) \in \mathbb{M} ) , \forall i \in \mathbb{M} . \forall j \in \mathbb{M} . ( i < j , j < P \Longrightarrow x ( i ) < x ( j ) )\)
⊑. … \(\langle x , P \rangle \sqsubseteq \langle v , L \rangle \Longleftrightarrow \forall i \in \mathbb{M} . ( i < P \Longrightarrow \exists j \in \mathbb{M} . j < L , x ( i ) = v ( j ) )\)
⊨₀. … \(c \models_0 \langle x , P \rangle \Longleftrightarrow \forall i \in \mathbb{M} . \forall j \in \mathbb{M} . ( i < j , j < P \Longrightarrow ( c ( x ( i ) ) ) ( x ( j ) ) = 0 )\)
⊨₁. … \(c \models_1 \langle x , P \rangle \Longleftrightarrow \forall i \in \mathbb{M} . \forall j \in \mathbb{M} . ( i < j , j < P \Longrightarrow ( c ( x ( i ) ) ) ( x ( j ) ) \neq 0 )\)
R0Q … \(Q \in \mathbb{M} \Longrightarrow \forall c \, \forall v \, \forall L \in \mathbb{M} . ( v \upuparrows L , 0 \le L \Longrightarrow \exists x \, ( ( x \upuparrows 0 , \langle x , 0 \rangle \sqsubseteq \langle v , L \rangle , c \models_0 \langle x , 0 \rangle ) \mathbin{\rm o\!r} ( x \upuparrows Q , \langle x , Q \rangle \sqsubseteq \langle v , L \rangle , c \models_1 \langle x , Q \rangle ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄
RP0 … \(P \in \mathbb{M} \Longrightarrow \forall c \, \forall v \, \forall L \in \mathbb{M} . ( v \upuparrows L , 0 \le L \Longrightarrow \exists x \, ( ( x \upuparrows P , \langle x , P \rangle \sqsubseteq \langle v , L \rangle , c \models_0 \langle x , P \rangle ) \mathbin{\rm o\!r} ( x \upuparrows 0 , \langle x , 0 \rangle \sqsubseteq \langle v , L \rangle , c \models_1 \langle x , 0 \rangle ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄
Lsplit … \(a , b , n , m \in \mathbb{M} , n + m \le a + b \Longrightarrow n \le a \mathbin{\rm o\!r} m \le b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，1.

2 数える

最後の頂点 \(v(m)\) より前の頂点を、\(v(m)\) と赤で結ばれるものの列 \(r\) と青で結ばれるものの列 \(u\) に振り分けます（ENUM）。
ENUM … \(m , M \in \mathbb{M} , v \upuparrows m \textit{+1} , M \le m \Longrightarrow \exists a \in \mathbb{M} . \exists b \in \mathbb{M} . a + b = M , \exists r \, ( r \upuparrows a , \langle r , a \rangle \sqsubseteq \langle v , M \rangle , \forall i \in \mathbb{M} . ( i < a \Longrightarrow ( c ( r ( i ) ) ) ( v ( m ) ) = 0 ) ) , \exists u \, ( u \upuparrows b , \langle u , b \rangle \sqsubseteq \langle v , M \rangle , \forall i \in \mathbb{M} . ( i < b \Longrightarrow ( c ( u ( i ) ) ) ( v ( m ) ) \neq 0 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，upd𝕄

3 付け足す

赤の隣の中の赤の完全部分に \(v(m)\) を付け足すと、\(v\) の中の1つ大きい赤の完全部分（APPR）。青も同じ（APPB）。

4 帰納法の1段

赤の隣が \(n\) 個以上なら、そこに \((P, Q+1)\) の場合を当て、赤の完全部分なら \(v(m)\) を付け足します。青の隣が \(k\) 個以上なら同様です。\(n + k \le m\) なのでどちらかが起きます（Lsplit）。
STEP … \(P , Q , n , k , m \in \mathbb{M} , \forall c \, \forall v \, \forall L \in \mathbb{M} . ( v \upuparrows L , n \le L \Longrightarrow \exists x \, ( ( x \upuparrows P , \langle x , P \rangle \sqsubseteq \langle v , L \rangle , c \models_0 \langle x , P \rangle ) \mathbin{\rm o\!r} ( x \upuparrows Q \textit{+1} , \langle x , Q \textit{+1} \rangle \sqsubseteq \langle v , L \rangle , c \models_1 \langle x , Q \textit{+1} \rangle ) ) ) , \forall c \, \forall v \, \forall L \in \mathbb{M} . ( v \upuparrows L , k \le L \Longrightarrow \exists x \, ( ( x \upuparrows P \textit{+1} , \langle x , P \textit{+1} \rangle \sqsubseteq \langle v , L \rangle , c \models_0 \langle x , P \textit{+1} \rangle ) \mathbin{\rm o\!r} ( x \upuparrows Q , \langle x , Q \rangle \sqsubseteq \langle v , L \rangle , c \models_1 \langle x , Q \rangle ) ) ) , v \upuparrows m \textit{+1} , ( n + k ) \textit{+1} \le m \textit{+1} \Longrightarrow \exists x \, ( ( x \upuparrows P \textit{+1} , \langle x , P \textit{+1} \rangle \sqsubseteq \langle v , m \textit{+1} \rangle , c \models_0 \langle x , P \textit{+1} \rangle ) \mathbin{\rm o\!r} ( x \upuparrows Q \textit{+1} , \langle x , Q \textit{+1} \rangle \sqsubseteq \langle v , m \textit{+1} \rangle , c \models_1 \langle x , Q \textit{+1} \rangle ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，upd𝕄 ，1.

5 Ramsey の定理

どの \(P, Q\) にも、長さ \(N\) 以上のどの増加列 \(v\) とどの色付け \(c\) についても、\(v\) の中に大きさ \(P\) の赤の完全部分か大きさ \(Q\) の青の完全部分がある、という \(N\) があります。\(P\) と \(Q\) についての二重の帰納法で、\(N\) は \((n + k) + 1\) と取ります（STEP）。
Ramsey … \(P , Q \in \mathbb{M} \Longrightarrow \exists N \in \mathbb{M} . \forall c \, \forall v \, \forall L \in \mathbb{M} . ( v \upuparrows L , N \le L \Longrightarrow \exists x \, ( ( x \upuparrows P , \langle x , P \rangle \sqsubseteq \langle v , L \rangle , c \models_0 \langle x , P \rangle ) \mathbin{\rm o\!r} ( x \upuparrows Q , \langle x , Q \rangle \sqsubseteq \langle v , L \rangle , c \models_1 \langle x , Q \rangle ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，upd𝕄 ，1.