超フィルターを使ったRamseyの定理の証明の形式化
この記事は
Mathematical Logic Advent Calendar 2020( https://adventar.org/calendars/5002)の17日目の記事です．
内容はACAでのRameyの定理の証明です．
Prehomogeneous setを取る際に，よく知られたErdös/Radó treeを使う方法ではなく，
超フィルターを使った証明の形式化を与えました．
Ramsey型の定理で超フィルターが有効に働くのは，無限集合有限個の共通部分が再び無限集合となるように扱えるからですが，
Ramseyの定理を証明する際にはその部分の議論をRT
で代用できる，というのが基本的な議論です．
