# Lema de Konig

O Lema de König ou Lema da Infinitude de König é um teorema da teoria dos grafos creditado a Dénes Kőnig (1936). Ele fornece uma condição suficiente para que um grafo infinito tenha um ramo infinitamente longo. Os aspectos desse teorema relacionados à computabilidade têm sido minuciosamente estudados por pesquisadores da lógica matemática, especialmente na teoria da computabilidade. Tal teorema também desempenha papeis importantes na matemática construtiva e na teoria da prova.

## Afirmação do Lema

Se G é um grafo conectado com um número infinito de nós tal que cada nó possui grau finito (isto é, tem um número de nós adjacentes finito), então G possui uma ramificação simples infinitamente longa, isto é, uma ramificação que não possui nós repetidos.
Um caso especial dessa afirmação que acontece comumente é que toda árvore) que possui uma quantidade infinita de nós, em que cada um possui grau finito, possui ao menos uma ramificação simples que é infinita.
Perceba que o grau dos nós deve ser finito mas não precisa ser delimitado: é possível que um nó tenha grau 10 enquanto outro possui grau 100, um terceiro possui grau 1000 e assim por diante.

### Prova

Para a prova, assuma que o grafo consiste de uma quantidade infinita de nós n_i e é conectado.
Comece com qualquer nó n_1. Cada nó do conjunto infinito de nós de G pode ser alcançado a partir de n_1 através de um caminho simples e cada caminho desse deve começar com um dos nós do conjunto finito de nós adjacentes a n_1. Deve haver um desses nós adjacentes pelo qual um conjunto infinito de nós pode ser alcançado sem passar por n_1. Se não existisse, então o grafo inteiro seria a união de um conjunto finito de conjuntos finitos e, portanto, finito, contradizendo a suposição de que o grafo é infinito. Devemos, portanto, escolher um desses vértices e chamá-lo n_2.
Agora um número infinito de nós de G pode ser alcançado a partir de n_2 através de um caminho simples que não utiliza o nó n_1. Cada caminho desse deve começar com um nó do conjunto finito de nós adjacentes a n_2. Então um argumento similar ao apresentado acima mostra que deve haver um desses nós adjacentes através do qual uma quantidade infinita de nós pode ser alcançada; escolha um e chame de n_3.
Continuamente desta maneira, uma caminho simples infinito pode ser construído através de indução matemática. A cada passo, a hipótese de indução afirma que existe uma quantidade infinita de nós alcançáveis por um caminho simples a partir de um nó em particular v_i que não passa por um dos nós de um conjunto finito de nós. O argumento de indução é que um dos nós adjacentes n_i satisfaz a hipótese de indução, mesmo quando n_i é adicionado ao conjunto finito.
O resultado desse argumento de indução é que para todo k é é possível escolher um nó n_k da maneira descrita pela construção. O conjunto de nós escolhidos na construção é então uma cadeia no grafo por que cada um foi escolhido para ser adjacente ao nó anterior e a construção garante que o mesmo nó nunca é escolhido duas vezes.
Esta prova normalmente não é considerada uma prova por construção por que em cada passo utiliza uma prova por contradição para estabelecer que existe um nó adjacente a partir do qual uma quantidade infinita de nós pode ser alcançada. Fatos sobre aspectos computacionais do lema sugerem que nenhuma prova pode ser dada que pudesse ser considerada prova por construção pelas escolas fundamentais da matemática construtiva.

## Aspectos computacionais

Os aspectos computacionais dos lemas de König, foram cuidadosamente investigados. O lema de König mais conveniente para essa finalidade é o que afirma que qualquer infinito onde há uma ramificação finita da sub-árvore de $\omega ^{<\omega }\,$, tem um caminho infinito. Aqui indica o conjunto dos números naturais e a árvore canônica de todas as ordens finitas dos números naturais, organizados por extensão. Cada sequência finita pode ser identificada por uma função parcial delas mesmas, e cada combinação infinita pode ser identificada com uma função total. Isso permite uma análise utilizando as técnicas da teoria computacional.
Uma subarvore de $\omega ^{<\omega }\,$ na qual cada sequência tem apenas um número finito de extensões imediatas (ou seja, a árvore tem um grau finito quando vista como um grafo), é chamada de ramificação finita. Nem toda subárvore infinita de $\omega ^{<\omega }\,$ tem um caminho infinito, mas o lema de Konig mostra que qualquer subarvore de ramificação finita, deve ter um caminho infinito.
Para qualquer subárvore "T" $\omega ^{<\omega }\,$ a notação Ext(T) significa o conjunto de nós de T através dos quais existe um caminho infinito. Mesmo quando T é computável, o conjunto Ext(T) pode não ser computável. Toda subárvore "T" de $\omega ^{<\omega }\,$ que tem um caminho, tem um caminho computável de Ext(T).
Sabe-se que existem infinitas subarvores de ramificações computáveis de $\omega ^{<\omega }\,$ que não tem um caminho aritmético, nem mesmo um caminho hiper-aritmético. Todavia, toda subárvore computável de $\omega ^{<\omega }\,$ com um caminho, deve ter um caminho computável por Kleene’s O, o conjunto completo canônico $\Pi _{1}^{1}$. Isto se deve ao fato do conjunto Ext(T) ser sempre <formula> quando T é computável.
Uma cuidadosa análise tem sido feita nas árvores computacionalmente limitadas. Uma subarvore de $\omega ^{<\omega }\,$ é chamada computacionalmente limitada ou recursivamente limitada se existe uma função computável f de W para W tal que para todo n, não existe nenhuma sequência na árvore cujo n-ésimo elemento é maior do que f(n). Assim, f limita a “altura” da árvore. O seguinte teorema fundamental se aplica as subarvores de $\omega ^{<\omega }\,$ infinitas, computacionalmente limitadas e computáveis.
* Toda árvore desse tipo tem um caminho computável a partir de $0'$, o conjunto Turing completo que pode decidir o problema de parada.
* Toda árvore desse tipo tem um caminho baixo. Este caminho é conhecido como o teorema de base baixa.
* Toda árvore desse tipo tem um caminho que é completamente livre. Isto significa que qualquer função computável a partir deste caminho é dominada por uma função computável.
* Para todo subconjunto não-computável "X" de $\omega$, a árvore tem um caminho que não computa X.
Uma forma fraca do lema de Konigs que diz que toda árvore binária infinita tem um ramo infinito, é usado para definir o subsistema WKL$_0$ de aritmética de segunda-ordem. Este subsistema tem uma importante regra na matemática reversa. Aqui, uma árvore binária é aquela na qual todos os termos de todas as sequencias na árvore são 0 ou 1, que quer dizer que a árvore é computacionalmente limitada pela função constante 2. A forma completa do lema de Konigs não é demonstrada em WKL$_0$, mas ao subsistema forte ACA$_0$.

## Relações com a matemática construtiva e compacidade

O famoso teorema de E. L. J. Brower é, de um ponto de vista clássico, a contrapositiva de uma forma do lema de Konig. Um subconjunto "S" $\{0,1\}^{<\omega }\,$ é chamado um "bar", se alguma função de $\omega$ para $\{0,1\}$ tem algum segmento inicial em "S". Um "bar" é destacável se toda sequência está também no bar ou não está no bar (essa suposição é necessária porque é teorema é ordinariamente considerado em situações onde a lei da exclusão mútua não é considerada). Um bar é uniforme se existe algum numero "N" tal que toda função de $\omega$ to $\{0,1\}$ tenha um segmento inicial no bar de tamanho no máximo $N$. O teorema de Brower diz que todo bar destacável é uniforme.
Isto pode ser provado numa configuração clássica, considerando um bar como uma cobertura aberta do espaço topológico compacto $\{0,1\}^{\omega }$. Cada sequência no par representa um conjunto básico aberto do espaço, e estes conjuntos básicos abertos cobrem o espaço por suposição. Pela compacidade, isto cobre uma finita subcobertura. O "N" do teorema de Brower pode ter o valor do tamanho do maior sequência cujo conjunto básico aberto está na subcobertura finita. Esta prova topológica pode ser usada na matemática clássica para mostrar que a seguinte forma do teorema de Konig é válida: para todo numero natural "K", toda subarvore infinita da árvore $\{0,\ldots ,k\}^{<\omega }\,$ tem um caminho infinito.

## Relação com o Axioma da Escolha

O Lema de Konig pode ser considerado um princípio de escolha; a primeira prova acima ilustra a relação do lema com o Axioma da dependência de escolha. A cada passo da indução, um vértice com uma propriedade particular deve ser selecionado. Embora seja provado que ao menos um vértice apropriado existe, se existir mais de um vértice com tal característica, pode não haver escolha canônica.
Se o grafo for contável, os vértices são bem ordenados e qualquer um pode escolher canônicamente o menor vértice apropriado. Nesse caso, o lema de Konig é demonstrável em aritmética de segunda ordem com compreensão aritmética, e , provado logicamente pela teoria dos conjuntos de Zermelo-Fraenkel.
O lema de Konig é essencialmente a restrição do axioma da dependência de escolha a toda relação "R" tal que para cada "x" há apenas um número finito de z tal que xRz. Embora o axioma da escolha seja, em geral, mais forte que o o princípio da dependência de escolha, esta restrição de dependência de escolha é equivalente a restrição do axioma de escolha. Em particular, quando a ramificação em cada nó é feita em um subconjunto finito de um conjunto arbitrário supostamente não contável, a forma do lema de Konig diz "Toda toda árvore infinita de ramificação finita tem um caminho infinito" é equivalente ao princípio de que cada conjunto contável de conjuntos finitos tem uma função de escolha. Essa forma do axioma da escolha (e por isso do lema de Konig) não é provada na teoria dos conjuntos de Zermelo-Fraenkel.