I believe it is correct to say there are undecidable theorems in some limited type systems which cannot be proven, but which can be once you extend the type sys

I believe it is correct to say there are undecidable theorems in some limited type systems which cannot be proven, but which can be once you extend the type system (e.g. by making it higher-level or dependent). So in those limited systems we know there are things that are "true" or "false", but which can only be proven when we have a superset of the original tools available. And by extension, maybe in our more complete type system there are things which can't be proven yet, but could perhaps be if there were better tools available? Maybe another angle to look at it: one of the things which is difficult to prove is the halting problem. Maybe you can't prove that a given program will terminate. But you could run that program and watch it terminate, and then you'd know it does. In that sense there is a "true" answer, but one which couldn't have been proved in advance from type theory. But I admit I only have a high-level understanding of these things. Type theory and axiomatic mathematics is something I'd like to know more about.