Gödelovo číslování

Gödelovo číslování  je funkce g , která přiřazuje každému objektu nějakého formálního jazyka jeho číslo. Lze jej použít k explicitnímu výčtu následujících jazykových objektů: proměnných, objektových konstant, funkčních symbolů, predikátových symbolů a vzorců z nich vytvořených. Konstrukce Gödelova číslování pro objekty teorie se nazývá aritmetizace teorie - umožňuje překládat výroky, axiomy, věty, teorie do objektů aritmetiky . Požaduje se, aby výčet g byl efektivně vypočitatelný a pro jakékoli přirozené číslo bylo možné určit, zda se jedná o číslo či nikoli, a pokud ano, pak sestrojit odpovídající objekt jazyka. Gödelovo číslování je velmi podobné kódování řetězců s čísly znak po znaku, s tím rozdílem, že ke kódování posloupností písmenových čísel se nepoužívá zřetězení čísel stejné délky, ale základní věta aritmetiky .

Gödelovo číslování použil Gödel jako nástroj pro prokázání neúplnosti formální aritmetiky .

Varianta Gödelova číslování formální teorie prvního řádu

Nechť je  teorie prvního řádu obsahující proměnné , objektové konstanty , funkční symboly a predikátové symboly , kde  je číslo a  je arita funkčního nebo predikátového symbolu.

Každý symbol libovolné teorie prvního řádu je spojen se svým Gödelovým číslem následovně: [1]

Gödelovo číslo libovolné posloupnosti výrazů je definováno takto: .

Existují také jiná Gödelova číslování formální aritmetiky.

Příklad

Zobecnění

Obecně se výčet množiny nazývá všude definované surjektivní mapování . If , then se nazývá číslo objektu . Konkrétní případy - jazyky a teorie.

Poznámky

  1. Mendelssohn, 1971 , § 4. Aritmetizace. Gödelova čísla., str. 151-152.

Literatura

Viz také