I think the closest thing to what you are looking for are the logical systems studied in Cook and Nguyen's recent book Logical Foundations of Proof Complexity. These are systems in which the provably total functions lie in certain well-defined computational complexity classes. This line of research goes back at least to Buss (as mentioned by Andrej Bauer), who defined systems of bounded arithmetic that are closely related to the levels of the polynomial hierarchy (a hierarchy of complexity classes whose lowest levels are $P$ and $NP$). More generally, the field known as "proof complexity" is devoted to studying the relationship between computational complexity classes (particularly circuit complexity classes) and formal systems for arithmetic with suitably weakened induction axioms.

This all assumes that you are satisfied with the idea that "better than brute force" means something like "polytime solvable." There are limitations with the concept of polynomial time solvability, notably its emphasis on asymptotic behavior and its focus on worst-case complexity. (Although average-case complexity has been studied, the natural questions there are very difficult to answer and the theory is much less developed.) Still, a lot of interesting insights have emerged from studying proof complexity and I think it is a very promising avenue for further research.

I think the closest thing to what you are looking for are the logical systems studied in Cook and Nguyen's recent book Logical Foundations of Proof Complexity. These are systems in which the provably total functions lie in certain well-defined computational complexity classes. In particular, existence proofs in these systems imply that the object whose existence is asserted can be computed "easily."

This line of research goes back at least to Buss (as mentioned by Andrej Bauer), who defined systems of bounded arithmetic that are closely related to the levels of the polynomial hierarchy (a hierarchy of complexity classes whose lowest levels are $P$ and $NP$). More generally, the field known as "proof complexity" is devoted to studying the relationship between computational complexity classes (particularly circuit complexity classes) and formal systems for arithmetic with suitably weakened induction axioms.

This all assumes that you are satisfied with the idea that "better than brute force" means something like "polytime solvable." There are limitations with the concept of polynomial time solvability, notably its emphasis on asymptotic behavior and its focus on worst-case complexity. (Although average-case complexity has been studied, the natural questions there are very difficult to answer and the theory is much less developed.) Still, a lot of interesting insights have emerged from studying proof complexity and I think it is a very promising avenue for further research.