Negation Complete
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.
Effectively Computable
Effectively Enumerable
Different ApproachHere 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?) |
