It's more or less explained in 1.2. A system is "sound" if it's consistent AND can only prove true things. To see the difference between sound and consistent,

It's more or less explained in 1.2. A system is "sound" if it's consistent AND can only prove true things. To see the difference between sound and consistent, suppose you have a formal system A which you know is sound. You can then (by Godel's construction) make a proposition G that says A can't prove or disprove G. We know that G is true because A can't in fact prove or disprove G, by construction. Make a new formal system by taking the axioms of A and adding the negation of G, that is, B=A+not(G). B is consistent but not sound. It's consistent because A can't prove G, so adding not(G) as an axiom can't possibly lead to a contradiction. And it's not sound because it can prove a falsehood, namely not(G) (granted, it's a very easy proof, since it's an axiom). Scott Aaronson calls systems like B "self-hating" [1], because they "believe" they're not consistent (even though they are). [1] https://www.scottaaronson.com/blog/?p=710 https://www.scottaaronson.com/blog/?p=710