This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are prov

This isn’t quite right, though perhaps a nit, plenty of formal systems are provably sound (only true things are provable) and complete (all true things are provable). For example, the predicate calculus you learn in Logic 101. Formal systems become provably incomplete when they are able to express arithmetic (e.g., Peano axioms).