Incompleteness Theorems, Large Cardinals, and Automata over Infinite Words

Abstract

We prove that there exist some 1-counter Büchi automata $\mathcal {A}_n$ for which some elementary properties are independent of theories like $T_n$ =: ZFC + “There exist (at least) n inaccessible cardinals", for integers $n\ge 1$. In particular, if $T_n$ is consistent, then “$L(\mathcal {A}_n)$ is Borel", “$L(\mathcal {A}_n)$ is arithmetical", “$L(\mathcal {A}_n)$ is $\omega$-regular", “$L(\mathcal {A}_n)$ is deterministic", and “$L(\mathcal {A}_n)$ is unambiguous" are provable from ZFC + “There exist (at least) $n+1$ inaccessible cardinals" but not from ZFC + “There exist (at least) n inaccessible cardinals". We prove similar results for infinitary rational relations accepted by 2-tape Büchi automata.