>>13856151To get a formal answer to this, you have to look at a formal system. And then there's 3 or 4 ways to read this.
1. The first is somewhat trivial: If you take a weak theory, then you can easily construct such a situation. E.g. there's a theory of groups TG (a few algebraic rules) and there's a theory of abelian groups TAG, where TAG is has the axioms of TG plus the axiom that all groups are commutative. Now something like the rotation group SO(3) is an object that fullfills the axioms of TG, so in some theory of math, there exist non-commutative groups. Given TAG (a theory where every group is abelian) as well an exmaple (in some much richer theory, like a set theory) of a non-abelian group, we conclude that the theory of groups TG cannot decide whether or not there exists a non-abelian group (or rather, whether there exists two group elements that don't commute). If it would prove there exists such a group, then TAG would be an inconsistent theory and if it proved such a group doesn't exist, then SO(3) would not be a group.
So the answer to your question about
>are there any mathematical problemstrivializes if we can choose a weak theory. We need a strong theory and then we ask again. If we take something like the set theoty ZF as "math", then the answer is that this situation still happens
https://en.wikipedia.org/wiki/List_of_statements_independent_of_ZFCThirdly, Gödel tells us, assuming arithmetic is consistent, that any theory which contains Robinson arithmetic (a theory with infinitely many things through which you can walk by successor and predecessor operations) and which is aximoized by a set of axioms that you can compute (including finite axiom sets), then there's statements P(n) such that "for all numbers n, P(n) holds" is unprovable.
This relates then extends to computably undecidable problems
https://en.wikipedia.org/wiki/List_of_undecidable_problemsSome of those are true by classical logic, but still have no algorithmic solution
