Main Page: Difference between revisions

From formulasearchengine
Jump to navigation Jump to search
← Older edit
No edit summary
No edit summary
 
(587 intermediate revisions by more than 100 users not shown)
Line 1: Line 1:
{{For|numberings of the set of computable functions|Numbering (computability theory)}}
This is a preview for the new '''MathML rendering mode''' (with SVG fallback), which is availble in production for registered users.


In [[mathematical logic]], a '''Gödel numbering''' is a [[function (mathematics)|function]] that assigns to each symbol and [[well-formed formula]] of some [[formal language]] a unique [[natural number]], called its '''Gödel number'''. The concept was used by [[Kurt Gödel]] for the proof of his [[Gödel's incompleteness theorems|incompleteness theorems]]. ({{harvnb|Gödel|1931}})
If you would like use the '''MathML''' rendering mode, you need a wikipedia user account that can be registered here [[https://en.wikipedia.org/wiki/Special:UserLogin/signup]]
* Only registered users will be able to execute this rendering mode.
* Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere.


A Gödel numbering can be interpreted as an [[Semantics encoding|encoding]] in which a number is assigned to each [[symbol]] of a [[mathematical notation]], after which a sequence of [[natural number]]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.
Registered users will be able to choose between the following three rendering modes:


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.
'''MathML'''
:<math forcemathmode="mathml">E=mc^2</math>


== Simplified overview ==
<!--'''PNG'''  (currently default in production)
Gödel noted that statements within a system can be represented by natural numbers. The significance of this was that properties of statements - such as their truth and falsehood - would be equivalent to determining whether their Gödel numbers had certain properties. The numbers involved might be very long indeed (in terms of number of digits), but this is not a barrier; all that matters is that we can show such numbers can be constructed.
:<math forcemathmode="png">E=mc^2</math>


In simple terms, we devise a method by which every formula or statement that can be formulated in our system gets a unique number, in such a way that we can mechanically convert back and forth between formulas and Gödel numbers. Clearly there are many ways this can be done. Given any statement, the number it is converted to is known as its Gödel number. A simple example is the way in which English is stored as a sequence of numbers in computers using [[ASCII]] or [[Unicode]]:
'''source'''
:* The word '''<tt>HELLO</tt>''' is represented by 72-69-76-76-79 using decimal [[ASCII]].
:<math forcemathmode="source">E=mc^2</math> -->
:* The logical statement '''<tt>x=y => y=x</tt>''' is represented by 120-061-121-032-061-062-032-121-061-120 using decimal ASCII.


== Gödel's encoding ==
<span style="color: red">Follow this [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering link] to change your Math rendering settings.</span> You can also add a [https://en.wikipedia.org/wiki/Special:Preferences#mw-prefsection-rendering-skin Custom CSS] to force the MathML/SVG rendering or select different font families. See [https://www.mediawiki.org/wiki/Extension:Math#CSS_for_the_MathML_with_SVG_fallback_mode these examples].
Gödel used a system based on [[prime factorization]]. 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 <math>(x_1,x_2,x_3,...,x_n)</math> 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:
==Demos==


:<math>\mathrm{enc}(x_1,x_2,x_3,\dots,x_n) = 2^{x_1}\cdot 3^{x_2}\cdot 5^{x_3}\cdots p_n^{x_n}.\,</math>
Here are some [https://commons.wikimedia.org/w/index.php?title=Special:ListFiles/Frederic.wang demos]:


According to the [[fundamental theorem of arithmetic]], any number obtained in this way can be uniquely factored into [[prime factor]]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 key observation of the proof.
* accessibility:
** Safari + VoiceOver: [https://commons.wikimedia.org/wiki/File:VoiceOver-Mac-Safari.ogv video only], [[File:Voiceover-mathml-example-1.wav|thumb|Voiceover-mathml-example-1]], [[File:Voiceover-mathml-example-2.wav|thumb|Voiceover-mathml-example-2]], [[File:Voiceover-mathml-example-3.wav|thumb|Voiceover-mathml-example-3]], [[File:Voiceover-mathml-example-4.wav|thumb|Voiceover-mathml-example-4]], [[File:Voiceover-mathml-example-5.wav|thumb|Voiceover-mathml-example-5]], [[File:Voiceover-mathml-example-6.wav|thumb|Voiceover-mathml-example-6]], [[File:Voiceover-mathml-example-7.wav|thumb|Voiceover-mathml-example-7]]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-Audio-Windows7-InternetExplorer.ogg Internet Explorer + MathPlayer (audio)]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-SynchronizedHighlighting-WIndows7-InternetExplorer.png Internet Explorer + MathPlayer (synchronized highlighting)]
** [https://commons.wikimedia.org/wiki/File:MathPlayer-Braille-Windows7-InternetExplorer.png Internet Explorer + MathPlayer (braille)]
** NVDA+MathPlayer: [[File:Nvda-mathml-example-1.wav|thumb|Nvda-mathml-example-1]], [[File:Nvda-mathml-example-2.wav|thumb|Nvda-mathml-example-2]], [[File:Nvda-mathml-example-3.wav|thumb|Nvda-mathml-example-3]], [[File:Nvda-mathml-example-4.wav|thumb|Nvda-mathml-example-4]], [[File:Nvda-mathml-example-5.wav|thumb|Nvda-mathml-example-5]], [[File:Nvda-mathml-example-6.wav|thumb|Nvda-mathml-example-6]], [[File:Nvda-mathml-example-7.wav|thumb|Nvda-mathml-example-7]].
** Orca: There is ongoing work, but no support at all at the moment [[File:Orca-mathml-example-1.wav|thumb|Orca-mathml-example-1]], [[File:Orca-mathml-example-2.wav|thumb|Orca-mathml-example-2]], [[File:Orca-mathml-example-3.wav|thumb|Orca-mathml-example-3]], [[File:Orca-mathml-example-4.wav|thumb|Orca-mathml-example-4]], [[File:Orca-mathml-example-5.wav|thumb|Orca-mathml-example-5]], [[File:Orca-mathml-example-6.wav|thumb|Orca-mathml-example-6]], [[File:Orca-mathml-example-7.wav|thumb|Orca-mathml-example-7]].
** From our testing, ChromeVox and JAWS are not able to read the formulas generated by the MathML mode.


There are more sophisticated (and more concise) ways to construct a [[Gödel numbering for sequences]].
==Test pages ==


== Example ==
To test the '''MathML''', '''PNG''', and '''source''' rendering modes, please go to one of the following test pages:
*[[Displaystyle]]
*[[MathAxisAlignment]]
*[[Styling]]
*[[Linebreaking]]
*[[Unique Ids]]
*[[Help:Formula]]


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<sup>6</sup> × 3<sup>5</sup> × 5<sup>6</sup> = 243,000,000.
*[[Inputtypes|Inputtypes (private Wikis only)]]
 
*[[Url2Image|Url2Image (private Wikis only)]]
== Lack of uniqueness ==
==Bug reporting==
 
If you find any bugs, please report them at [https://bugzilla.wikimedia.org/enter_bug.cgi?product=MediaWiki%20extensions&component=Math&version=master&short_desc=Math-preview%20rendering%20problem Bugzilla], or write an email to math_bugs (at) ckurs (dot) de .
A Gödel numbering is not unique, in that for any proof using Gödel numbers, there are infinitely many ways in which these numbers could be defined.
 
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 numeration|bijective base-''K'' numeral system]]. A formula consisting of a string of ''n'' symbols <math> s_1 s_2 s_3 \dots s_n</math> would then be mapped to the number
 
:<math> h(s_1) \times K^{(n-1)} + h(s_2) \times K^{(n-2)} + \cdots + h(s_{n-1}) \times K^1 + h(s_n) \times K^0 .</math>
 
In other words, by placing the set of ''K'' basic symbols in some fixed order, such that the ''i''<sup>''th''</sup> symbol corresponds uniquely to the ''i''<sup>''th''</sup> digit of a bijective base-''K'' numeral system, ''each formula may serve just as the very numeral of its own Gödel number.''
 
== Application to formal arithmetic ==
 
Once a Gödel numbering for a formal theory is established, each [[rule of inference|inference rule]] of the theory can be expressed as a function on the natural numbers. If ''f'' is the Gödel mapping and if formula ''C'' can be derived from formulas ''A'' and ''B'' through an inference rule ''r''; i.e.
:<math> A, B \vdash_r C, \ </math>
then there should be some [[arithmetical function]] ''g<sub>r</sub>'' of natural numbers such that
:<math> g_r(f(A),f(B)) = f(C). \ </math>
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 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]]s.
 
== Generalizations ==
 
In [[computability theory]], 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]] to natural numbers in such a way that the numbers can be manipulated by an [[algorithm]] 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 (mathematics)|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]]s that manipulate strings rather than numbers.
<!--
There is a very different meaning of the term Gödel numbering relating to
[[numbering (computability theory)|numberings]] of the class of [[computable function]]s. COMMENTED OUT PER TALK -->
 
==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]] 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 logic|infinitary languages]].
 
== See also ==
* [[Church numeral]]
* [[Description number]]
* [[Gödel numbering for sequences]]
* [[Gödel's incompleteness theorems]]
* [[Kolmogorov_complexity#Chaitin.27s_incompleteness_theorem|Chaitin's incompleteness theorem]]
 
== References ==
 
* {{Citation|last=Gödel|first= Kurt |title=Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I |journal=Monatsheft für Math. und Physik |volume=38|year= 1931| pages=173&ndash;198 |url=http://www.w-k-essler.de/pdfs/goedel.pdf}}.
*''Gödel's Proof'' by [[Ernest Nagel]] and [[James R. Newman]] (1959). This book provides a good introduction and summary of the proof, with a large section dedicated to Gödel's numbering.
 
{{reflist}}
 
== Further reading ==
* ''[[Gödel, Escher, Bach|Gödel, Escher, Bach: an Eternal Golden Braid]]'', by [[Douglas Hofstadter]]. This book defines and uses an alternative Gödel numbering.
*''[[I Am a Strange Loop]]'' by [[Douglas Hofstadter]]. This is a newer book by Hofstadter that includes the history of Gödel's numbering.
 
{{DEFAULTSORT:Godel Number}}
[[Category:Mathematical logic]]
[[Category:Theory of computation]]
[[Category:Works by Kurt Gödel|Numering]]

Latest revision as of 22:52, 15 September 2019

This is a preview for the new MathML rendering mode (with SVG fallback), which is availble in production for registered users.

If you would like use the MathML rendering mode, you need a wikipedia user account that can be registered here [[1]]

  • Only registered users will be able to execute this rendering mode.
  • Note: you need not enter a email address (nor any other private information). Please do not use a password that you use elsewhere.

Registered users will be able to choose between the following three rendering modes:

MathML

E=mc2


Follow this link to change your Math rendering settings. You can also add a Custom CSS to force the MathML/SVG rendering or select different font families. See these examples.

Demos

Here are some demos:


Test pages

To test the MathML, PNG, and source rendering modes, please go to one of the following test pages:

Bug reporting

If you find any bugs, please report them at Bugzilla, or write an email to math_bugs (at) ckurs (dot) de .

Retrieved from "https://en.formulasearchengine.com/index.php?title=Main_Page&oldid=329754"