In
mathematical logic
Mathematical logic is the study of Logic#Formal logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory (also known as computability theory). Research in mathematical logic com ...
, a Gödel numbering is a
function that assigns to each symbol and
well-formed formula
In mathematical logic, propositional logic and predicate logic, a well-formed formula, abbreviated WFF or wff, often simply formula, is a finite sequence of symbols from a given alphabet that is part of a formal language.
The abbreviation wf ...
of some
formal language
In logic, mathematics, computer science, and linguistics, a formal language is a set of strings whose symbols are taken from a set called "alphabet".
The alphabet of a formal language consists of symbols that concatenate into strings (also c ...
a unique
natural number
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
, called its Gödel number.
Kurt Gödel
Kurt Friedrich Gödel ( ; ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel profoundly ...
developed the concept for the proof of his
incompleteness theorems.
A Gödel numbering can be interpreted as an
encoding
In communications and Data processing, information processing, code is a system of rules to convert information—such as a letter (alphabet), letter, word, sound, image, or gesture—into another form, sometimes data compression, shortened or ...
in which a number is assigned to each
symbol
A symbol is a mark, Sign (semiotics), sign, or word that indicates, signifies, or is understood as representing an idea, physical object, object, or wikt:relationship, relationship. Symbols allow people to go beyond what is known or seen by cr ...
of a
mathematical notation
Mathematical notation consists of using glossary of mathematical symbols, symbols for representing operation (mathematics), operations, unspecified numbers, relation (mathematics), relations, and any other mathematical objects and assembling ...
, after which a sequence of
natural number
In mathematics, the natural numbers are the numbers 0, 1, 2, 3, and so on, possibly excluding 0. Some start counting with 0, defining the natural numbers as the non-negative integers , while others start with 1, defining them as the positive in ...
s can then represent a sequence of symbols. These sequences of natural numbers can again be represented by single natural numbers, facilitating their manipulation in formal theories of arithmetic.
Since the publishing of Gödel's paper in 1931, the term "Gödel numbering" or "Gödel code" has been used to refer to more general assignments of natural numbers to mathematical objects.
Simplified overview
Gödel noted that each statement within a system can be represented by a natural number (its ''Gödel number''). The significance of this was that properties of a statement—such as its truth or falsehood—would be equivalent to determining whether its Gödel number had certain properties. The numbers involved might be very large indeed, but this is not a barrier; all that matters is that such numbers can be constructed.
In simple terms, Gödel devised a method by which every formula or statement that can be formulated in the system gets a unique number, in such a way that formulas and Gödel numbers can be mechanically converted back and forth. There are many ways to do this. A simple example is the way in which English is stored as a sequence of numbers in computers using
ASCII
ASCII ( ), an acronym for American Standard Code for Information Interchange, is a character encoding standard for representing a particular set of 95 (English language focused) printable character, printable and 33 control character, control c ...
. Since ASCII codes are in the range 0 to 127, it is sufficient to pad them to 3 decimal digits and then to concatenate them:
* The word is represented by .
* The logical formula is represented by .
Gödel's encoding
Gödel used a system based on
prime factorization
In mathematics, integer factorization is the decomposition of a positive integer into a product of integers. Every positive integer greater than 1 is either the product of two or more integer factors greater than 1, in which case it is a comp ...
. He first assigned a unique natural number to each basic symbol in the formal language of arithmetic with which he was dealing.
To encode an entire formula, which is a sequence of symbols, Gödel used the following system. Given a sequence
of positive integers, the Gödel encoding of the sequence is the product of the first ''n'' primes raised to their corresponding values in the sequence:
:
According to the
fundamental theorem of arithmetic
In mathematics, the fundamental theorem of arithmetic, also called the unique factorization theorem and prime factorization theorem, states that every integer greater than 1 is prime or can be represented uniquely as a product of prime numbers, ...
, any number (and, in particular, a number obtained in this way) can be uniquely factored into
prime factor
A prime number (or a prime) is a natural number greater than 1 that is not a product of two smaller natural numbers. A natural number greater than 1 that is not prime is called a composite number. For example, 5 is prime because the only ways ...
s, so it is possible to recover the original sequence from its Gödel number (for any given number n of symbols to be encoded).
Gödel specifically used this scheme at two levels: first, to encode sequences of symbols representing formulas, and second, to encode sequences of formulas representing proofs. This allowed him to show a correspondence between statements about natural numbers and statements about the provability of theorems about natural numbers, the proof's key observation ().
There are more sophisticated (and more concise) ways to construct a
Gödel numbering for sequences.
Example
In the specific Gödel numbering used by Nagel and Newman, the Gödel number for the symbol "0" is 6 and the Gödel number for the symbol "=" is 5. Thus, in their system, the Gödel number of the formula "0 = 0" is 2
6 × 3
5 × 5
6 = 243,000,000.
Lack of uniqueness
Infinitely many different Gödel numberings are possible. For example, supposing there are ''K'' basic symbols, an alternative Gödel numbering could be constructed by invertibly mapping this set of symbols (through, say, an
invertible function ''h'') to the set of digits of a
bijective base-''K'' numeral system. A formula consisting of a string of ''n'' symbols
would then be mapped to the number
:
In other words, by placing the set of ''K'' basic symbols in some fixed order, such that the
-th symbol corresponds uniquely to the
-th digit of a bijective base-''K'' numeral system, ''each formula may serve just as the very numeral of its own Gödel number.''
For example, the numbering described
here has K=1000.
Application to formal arithmetic
Recursion
One may use Gödel numbering to show how functions defined by
course-of-values recursion are in fact
primitive recursive function
In computability theory, a primitive recursive function is, roughly speaking, a function that can be computed by a computer program whose loops are all "for" loops (that is, an upper bound of the number of iterations of every loop is fixed befor ...
s.
Expressing statements and proofs by numbers
Once a Gödel numbering for a formal theory is established, each
inference rule
Rules of inference are ways of deriving conclusions from premises. They are integral parts of formal logic, serving as norms of the logical structure of valid arguments. If an argument with true premises follows a rule of inference then the co ...
of the theory can be expressed as a function on the natural numbers. If ''f'' is the Gödel mapping and ''r'' is an inference rule, then there should be some
arithmetical function
In number theory, an arithmetic, arithmetical, or number-theoretic function is generally any Function (mathematics), function whose Domain of a function, domain is the set of natural number, positive integers and whose range is a subset of the co ...
''g
r'' of natural numbers such that if formula ''C'' is derived from formulas ''A'' and ''B'' through an inference rule ''r'', i.e.
:
then
:
This is true for the numbering Gödel used, and for any other numbering where the encoded formula can be arithmetically recovered from its Gödel number.
Thus, in a formal theory such as
Peano arithmetic
In mathematical logic, the Peano axioms (, ), also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nea ...
in which one can make statements about numbers and their arithmetical relationships to each other, one can use a Gödel numbering to indirectly make statements about the theory itself. This technique allowed Gödel to prove results about the consistency and completeness properties of
formal system
A formal system is an abstract structure and formalization of an axiomatic system used for deducing, using rules of inference, theorems from axioms.
In 1921, David Hilbert proposed to use formal systems as the foundation of knowledge in ma ...
s.
Generalizations
In
computability theory
Computability theory, also known as recursion theory, is a branch of mathematical logic, computer science, and the theory of computation that originated in the 1930s with the study of computable functions and Turing degrees. The field has since ex ...
, the term "Gödel numbering" is used in settings more general than the one described above. It can refer to:
#Any assignment of the elements of a
formal language
In logic, mathematics, computer science, and linguistics, a formal language is a set of strings whose symbols are taken from a set called "alphabet".
The alphabet of a formal language consists of symbols that concatenate into strings (also c ...
to natural numbers in such a way that the numbers can be manipulated by an
algorithm
In mathematics and computer science, an algorithm () is a finite sequence of Rigour#Mathematics, mathematically rigorous instructions, typically used to solve a class of specific Computational problem, problems or to perform a computation. Algo ...
to simulate manipulation of elements of the formal language.
#More generally, an assignment of elements from a countable mathematical object, such as a countable
group, to natural numbers to allow algorithmic manipulation of the mathematical object.
Also, the term Gödel numbering is sometimes used when the assigned "numbers" are actually strings, which is necessary when considering models of computation such as
Turing machine
A Turing machine is a mathematical model of computation describing an abstract machine that manipulates symbols on a strip of tape according to a table of rules. Despite the model's simplicity, it is capable of implementing any computer algori ...
s that manipulate strings rather than numbers.
Gödel sets
Gödel sets are sometimes used in set theory to encode formulas, and are similar to Gödel numbers, except that one uses sets rather than numbers to do the encoding. In simple cases when one uses a
hereditarily finite set
In mathematics and set theory, hereditarily finite sets are defined as finite sets whose elements are all hereditarily finite sets. In other words, the set itself is finite, and all of its elements are finite sets, recursively all the way down to t ...
to encode formulas this is essentially equivalent to the use of Gödel numbers, but somewhat easier to define because the tree structure of formulas can be modeled by the tree structure of sets. Gödel sets can also be used to encode formulas in
infinitary languages.
See also
*
Church encoding
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded d ...
*
Description number
*
Gödel numbering for sequences
*
Gödel's incompleteness theorems
Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the phi ...
*
Chaitin's incompleteness theorem
Notes
References
*
Further reading
* Defines and uses an alternative Gödel numbering.
* Includes the history of Gödel's numbering.
* Uses Gödel numbering to encode programs.
{{DEFAULTSORT:Godel numbering
Mathematical logic
Theory of computation
Numbering