Editing Berry paradox (section)

== Formal analogues ==

Using programs or proofs of bounded lengths, it is possible to construct an analogue of the Berry expression in a formal mathematical language, as has been done by [[Gregory Chaitin]]. Though the formal analogue does not lead to a logical contradiction, it does prove  certain impossibility results.{{sfn|Chaitin|1995}}

{{harvtxt|Boolos|1989}} built on a formalized version of Berry's paradox to prove [[Gödel's incompleteness theorem]] in a new and much simpler way. The basic idea of his proof is that a [[proposition]] that holds of ''x'' if and only if ''x'' = ''n'' for some natural number ''n'' can be called a ''definition'' for ''n'', and that the set {(''n'', ''k''): ''n'' has a definition that is ''k'' symbols long} can be shown to be representable (using [[Gödel number]]s). Then the proposition "''m'' is the first number not definable in less than ''k'' symbols" can be formalized and shown to be a definition in the sense just stated.{{sfn|Boolos|1989}}