この記事は Mathematical Logic Advent Calendar 2022の 6日目の記事です． ACA0からという形の文(は算術的)が証明可能なとき，XからYを一様に与える算術的に定義可能なfunctionalが存在することを示し，それを利用したATR0の特徴づけを与えました． drive.g…