Beyond Goedel incompleteness and lack of soundness/completeness of higher-order logics As I understand that there are at least two fundamental limits of the development of the mathematics:
1) Goedel incompeleteness theorems (or more clearly Church thesis) effectively says that there always will be unsolved mathematical problems (e.g. satisfiability of some formula or solution of some equation) that can not be solved by mechanical means but only by the creative thinking of some person. One can imagine that computer can be of help even for these problems, e.g. there is Connectionist approach to do symbolic computing by neural networks (or any other heuristic approach; there is journal "Connection Science" for this) and - as far as I understand - then neural networks in principle can generate solutions (and proofs) of these algorithmically unsolvable problems (although the developments are scarce in this field). There is even idea about computation beyond Turing limits (hypercomputation) that suggests that neural networks with irrational weights can go beyond Turing limits (as some physical machines, e.g. more powerful than the traditional non-relativistic low-energy quantum computers that relies on century old theories). So - this is fine and actually this is not a prohibitive limit.
2) The lack of soundness/completeness of some mathematical theories (higher-order logics) can be bigger problem: this means that the mathematical objects (ideas) can not be investigated by investigation of syntactical transformation of the words of some more or less formal language. The question is - what the other tools can be applied in such cases? Are those mathematical objects (ideas) are unavailable to the human reason and does mathematics stops here indeed? Is indeed the (experimental) physics necessary to uncover those objects (ideas)? Some years ago Hawking had to recognise the limits of theoretical physics arising from the Godel incompleteness theories. Does mathematicians should recognise their own limits?
I am sorry for such amateurish discussion and generally I am not thinking about these issues in my everyday activities but it would be interesting to know whether there are some trends in mathematics that are trying to overcome the mentioned limits. As was as I have read journals by the Association of Symbolic Logic (I guess, the best journals in mathematical logic and everything around it, e.g. reverse mathematics) or the Annals of Mathematics (I guess, the best journal in mathematic) then they are not especially concerned about such limits, they function quite happy within them. So - what is happening in this direction?
I guess that there is something going on in the philosophy of math and also some developments along the lines e.g. theorizing whether human brains are more powerful than Turing machine or not. 
Actually I am not interested in this kind of thinking. I am more interestend in applications. E.g. modal logics can be quite powerful for software analysis or for building smart control systems for robotic applications (of for legal reasoning, knowledge engineering and so on). But modal logics lack some expresiveness (those logics are buil to be sound, complete and preferably with low computation time limits) and mentioned limits in mathematics prohibits them to be made more expressive by the standard tools (and not loosing completeness and soundness). So, if competition in the markets for modal logic applications arise then those who can reach beyond Goedel or Turing limits can win. At present I can imagine only heuristic solutions (neural networks, genetic algorihtms) to such problems, but maybe there are some other kind of technical results as well?
p.s. I asked similar question in ncatlab.org, but got no answers there.
 A: 
Goedel incompeleteness theorems (or more clearly Church thesis) effectively says that there always will be unsolved mathematical problems (e.g. satisfiability of some formula or solution of some equation) that can not be solved by mechanical means but only by the creative thinking of some person.

A common mistake. Mechanical means are strictly more powerful than creative thinking, because by "mechanical means" we include even ridiculously inefficient means such as "assume we have infinite memory and infinite time, and try absolutely every possible thing that can be done until we find one that works".
A: Unless the Turing/Church thesis is wrong, you will not gain any more practical power from changing to a different logical system. This is because a Turing machine, can simulate any  algorithm. Peano arithmetic (PA), an axiomatic first order logic axiomatization of the natural numbers, is Turing universal. In practice however, you would be more efficient in many applications if you use heuristic models. However, in the end any of these models can be simulated by a Turing machine, so in this sense these algorithms are not more powerful than a Turing machine. There is a close relationship between Goedel's provavility and Turing computability (see Post's theorem) 
Few people really believe that computing beyond the Turing limit is physically possible, our universe at least, doesn't seem to meet the conditions (noise is one of them).
But mathematicians are studying extensions of theoretical machines that can perform hypercomputations. See for example Hamkins work on infinite time Turing machines
A: About "1) Goedel incompeleteness theorems (or more clearly Church thesis) effectively says that there always will be unsolved mathematical problems (e.g. satisfiability of some formula or solution of some equation) that can not be solved by mechanical means but only by the creative thinking of some person."
The limits set to "mechanical means" by Godel, Church and Turing results concern formal systems; they in turn are algorithmic ways of manipulatingformulae (strings of symbols). Up to now, Turing machine is the best model we have for representing a echanical procedure": its success is impressive and the lack of plausible contrexamples gives force to Turing/Church thesis (i.e. the "identification" of the mathematical theory of Turing computation with the intuitive idea of "mechanical procedure").
But the progress achieved in past centuries reagarding mathematical and scientific ideas tell us that faith in "ultimate" ideas and theory is often misconceived.
About "2) The lack of soundness/completeness of some mathematical theories (higher-order logics) can be bigger problem: this means that the mathematical objects (ideas) can not be investigated by investigation of syntactical transformation of the words of some more or less formal language. The question is - what the other tools can be applied in such cases? Are those mathematical objects (ideas) are unavailable to the human reason and does mathematics stops here indeed?"
I don't think that higher-order logics are not sound ... for sure, they are not "complete" in some strict technical sense. A lot of information can be achieved investigating mathematical theories as formal systems (machine for generating derivations) but this doesn't mean that we cannot achieve real knowledge with other tools, e.g. with insight. Goedel's Incompleteness Th, Church's Theorem, Turing theory are all pretty good examples of perfectly "sound" mathematical results (ideas) achieved with human reason.
