Incompleteness theorems, large cardinals, and automata over infinite words

Abstract

We prove that there exist some 1-counter Büchi automataAn forwhich some elementary properties are independent of theories like Tn =: ZFC + “There exist (at least) n inaccessible cardinals”, for integers n ≥ 1. In particular, if Tnis consistent, then “L(An) is Borel”, “L(An) is arithmetical”, “L(An) is ω-regular”, “L(An) is deterministic”, and “L(An) 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.