TLDR
- In any consistent formal system that’s strong enough to do basic arithmetic, there are true statements it can’t prove. (First incompleteness)
- Such a system also can’t prove its own consistency. (Second incompleteness)
Intuition: Gödel encodes statements as numbers and builds one that effectively says, “This statement is not provable here.” If the system proved it, it would be inconsistent; so if it’s consistent, the statement is true but unprovable.