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