A formal system S is Negation Complete (AKA syntactically complete or deductively complete or maximally complete) if for each sentence (closed formula) φ of the language of the system either φ or ¬φ is a theorem of S.
Here is a video by Robert Harper where he gives an interesting take in this.
At about 37 min into this video he says: "what is true has unbounded quantifier complexity whereas any formalism is always relentlessly recursively innumerable" - Gödels theorem.
"there is a distinction between proof and truth"
(by formalism here I think he means formal logic?)