Would a type system that can verify whether array access is always in-bound implicitly encode arithmetic somehow? My gut feeling says yes, since I don't know how one would prove bounds without arithmetic, but I don't have the mathematical knowledge to back this up.

It would need a certain amount of arithmetic, but Presburger arithmetic (addition and constant multiplication, essentially) is complete and consistent and might be enough for all the array use we care about?