<blockquote>'''First Incompleteness Theorem''': "Any consistent formal system {{mvar|F}} within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of {{mvar|F}} which can neither be proved nor disproved in {{mvar|F}}." (Raatikainen 2020)<!-- this is a direct quote from (Raatikainen 2020) --></blockquote> == Boolos's short proof == [[George Boolos]] (1989) vastly simplified the proof of the First Theorem, if one agrees that the [[theorem]] is equivalent to: <blockquote> "There is no [[algorithm]] {{math|''M''}} whose output contains all true sentences of arithmetic and no false ones." </blockquote> "Arithmetic" refers to [[Peano axioms|Peano]] or [[Robinson arithmetic]], but the proof invokes no specifics of either, tacitly assuming that these systems allow '<' and '×' to have their usual meanings. Boolos proves the theorem in about two pages. His proof employs the language of [[first-order logic]], but invokes no facts about the [[logical connective|connectives]] or [[Quantifier (logic)|quantifier]]s. The [[domain of discourse]] is the [[natural number]]s. The [[Gödel sentence]] builds on [[Berry's paradox]]. — Boolos made a short proof, but it hinges in agreeing on a different expression of the theorem.