No. Any finite algorithm can be performed on a Turing machine, so if no Turing machine can solve the halting problem, then nor can any finite algorithm.without any proof ?
For your example of coloured Turing machines, I gave an explicit way of doing so (by creating a Turing machine with a symbol for every colour-symbol combination in your coloured Turing machine). You then made the non-standard restriction that I'm not allowed to change the alphabet, but this is irrelevant because there's an easy algorithm to convert an arbitrary Turing machine into a 2-symbol Turing machine.
My point is that there's absolutely no need to apply a diagonal argument to the set of coloured Turing machines! The unsolvability of the halting problem by any finite algorithm is the logical conclusion of:because as I argued diagonalization argument does not apply to the set of colored turing machine (considering my new definition)
1. Turing machines cannot solve the halting problem
2. Anything that can be computed by a finite algorithm can be computed by a Turing machine
There's no diagonal argument involved in proving 2, which is the part that you're seeming to dispute.
There are plenty of such formal systems: the first-order theory of algebraically closed fields of characteristic zero has this property. The caveat is that such systems are necessarily weak in their expressive power; you can't formalise the halting problem in such a system.
Yes, and both approaches are futile. There was a time pre-Godel where mathematicians such as Hilbert pursued this goal -- see https://en.wikipedia.org/wiki/Hilbert%27s_program -- but this is no longer taken seriously because it's been proven impossible.