Godel's first incompleteness theorem states roughly that you can't write down a finite list of axioms that can decide all statements about arithmetic: any such formal system is incomplete. I feel like I have a pretty good understanding of what this means concretely, but that's because there are concrete examples of formal systems that are complete.
Godel's second incompleteness theorem states that no formal system that can talk about arithmetic can prove its own consistency. I don't really appreciate this one as much on a gut level because I sort of feel like, well, duh - how could any formal system possibly prove its own consistency? Of course I know about Godel numbering and what not, but still, what I'd really like is an explicit example of a simple formal system, with a proof in that system of the system's own consistency. Does such a thing exist?