Trying to find a formal system that encodes unbounded infinitary mathematical objects including most of maths, but yet to require that all statements are decidable within a finite number of steps...

Is it contradiction in the proof, or rather a contradiction in assumptions?

More on logic that permits all that *Bounded* Turing Machine does: https://arxiv.org/abs/2106.13309