Before I took Mathematical Logic in graduate school I believed all kinds of nonsense about Godel’s theorems. Even after the class I still had false ideas about what it really meant. It took a while for the the recursively enumerable part to sink in as to why it is important.
I’ve heard what you say about second order axiom systems before but I don’t know enough about the subject. I naively think, “Why not just use the Second Order Peano Axioms?”. But people far more knowledgeable than me don’t like them so I defer to their judgement.
I don't qualify as far more knowledgeable than you, in fact I'm probably less knowledgeable but with a different point of view.
However with that disclaimer, the fundamental challenge is that when we start reasoning about reasoning, things that "should obviously work" run into trouble. (Most commonly due to variations on the liar's paradox.)
First order reasoning within a first order logic system that we think is good is "obviously correct" reasoning.
Second order reasoning introduces as much reasoning about reasoning as we think we can get away with, hopefully without causing problems. The result is that second order reasoning lets us talk about what kinds of unverifiable statements we can discuss the absolute truth of. But I'm uncomfortable with talking about the absolute truth of any unverifiable statements, which makes it feel like discussing the subtle shades of BS we fool ourselves into believing.
I’ve heard what you say about second order axiom systems before but I don’t know enough about the subject. I naively think, “Why not just use the Second Order Peano Axioms?”. But people far more knowledgeable than me don’t like them so I defer to their judgement.