There are some axiomatic systems where there is a procedure, an algorithm, for proving or disproving statements in that system. Propositional logic has truth tables and tableaux, for example. I believe some axiomatizations of plane geometry have such algorithms.

That’s not quite what Gödel’s Incompleteness Theorem says. It states that in any consistent, sufficiently expressive formal axiomatic system (such as one capable of expressing basic arithmetic), there exist true statements about the natural numbers that cannot be proven within the system itself.

In other words, if you have a system where you can recursively enumerate all the theorems derivable from its axioms, there will still be statements that are true but not included in that set — meaning the set of such theorems is incomplete.

These unprovable statements aren’t just guesses or philosophical curiosities — they’re considered true based on reasoning outside the system, such as meta-mathematical analysis or by interpreting them in the standard model of arithmetic. But because the system’s axioms aren’t strong enough, you can’t prove them from within.

And this isn’t a rare edge case. Most of the systems we care about in mathematics — especially those involving arithmetic — are expressive enough to fall under Gödel’s Incompleteness Theorem. So incompleteness isn’t an exception; it’s a fundamental feature of formal systems that are powerful enough to be interesting.

Maybe your should start with formal logic.

Ignoring a lot of technical details, you are correct.

Some people assume we are somewhat magic and we can prove any theorem, but as you noted there are still a lot of potential theorems we have not proven and perhaps we will never can.

Since science begins with self consciousness isn’t it simpler to assume that consciousness transcends the product of consciousness - science