Running title • November 2012 • Vol. XXI, No. 1
Como a quantidade de programas possíveis em P é enumerável, podemos ter apenas uma
quantidade enumerável de funções computáveis, que podem ser enumeradas. Listamos acima a
imagem de todas as funções computáveis (em f 0 temos f 0 ( 0 ) = 0, f 0 ( 1 ) = 1, f 0 ( 2 ) = 1, f 0 ( 3 ) =
0, f 0 ( 4 ) = 1, f 0 ( 5 ) = 0, f 0 ( 6 ) = 0, ...). Podemos definir então um novo elemento f tomando para
cada um dos elementos listados um elemento diferente do conjunto: f ( 0 ) = 1, diferente de
f 0 ( 0 ) = 0, ou seja, f é diferente de f 0 , em seguida f ( 1 ) = 1, diferente de f 1 ( 1 ) . Continuando deste
modo teremos que cada f ( i ) será diferente de f i ( i ) , ou seja, f será diferente de cada uma das
enumerações f i e, portanto, um novo elemento.
A esse novo elemento definido de tal forma chamaremos de função não computável 2 . O que
feremos, portanto, será fixar f : N → { 0, 1 } , uma função não computável.
3.
Uma teoria para definir f
Definição 2. Vamos chamar de uma teoria uma coleção finita de axiomas e algumas regras de inferência.
Informalmente, uma regra de inferência é uma maneira de se “obter” afirmações a partir de
anteriores. Por exemplo, uma possível (e bastante comum) regra é a que diz que a partir das
afirmações “A” e “A → B”, obtemos a afirmação “B” (essa regra é conhecida por modus ponens
que em palavras quer dizer “sabemos que A vale e que toda vez que A vale, B vale, então B vale”).
Outro exemplo é a regra de substituição: se temos “ϕ ( x ) ” e temos que “x = y”, então temos
“ϕ ( y ) ”, onde ϕ é uma propriedade qualquer. Ao fixar uma teoria, também estamos fixando os
símbolos que podem ser usados nas afirmações (em geral, são coisas como → , ∀ , v 1 , etc).
Vamos fixar para o decorrer deste texto uma teoria T que seja “rica” o suficiente para que
possamos definir a f fixada acima.
Definição 3. : Fixada uma teoria, uma demonstração nada mais é que uma sequência ϕ 1 , ..., ϕ n onde cada
ϕ k é um axioma ou existem ϕ i ’s com i < k de forma que ϕ k é obtida a partir de uma das regras de inferência
da teoria a partir das ϕ i ’s.
Para entender melhor o que é uma demonstração vejamos um exemplo na teoria de grupos.
Podemos demonstrar, a partir de um dos axiomas de grupo (o que garante a existência do elemento
neutro), a unicidade do elemento neutro da operação definida. Veja:
∃ e ∈ G ∀ a ∈ G ( e · a = a ) ∧ ( a · e = a )
∃ x ∈ G ∀ a ∈ G ( x · a = a ) → ( x = e )
x · e = x
x · e = e
x = e
4.
axioma
hipótese
uso do axioma
uso da hipótese
uso de um axioma lógico
Programando
Agora com a nossa linguagem de programação P fixada vamos fazer alguns programas sobre
resultados em nossas teorias, afinal precisamos de métodos para saber se uma afirmação é ou
não uma demonstração. É importante destacar aqui que é crucial que os programas possam
ser executados em tempo finito, afinal seria difícil encontrar um computador que rodasse um
programa para sempre.
2 Com um raciocínio semelhante (chamado método de diagonalização de Cantor) poderíamos provar a não enumerabili-
dade do conjunto das funções f : N → { 0, 1 } , ou seja, provar que não existe uma bijeção das f ’s com os naturais, isto é,
“sobram” funções. Aqui essas funções “excedentes” são chamadas de funções não computáveis. Essas, de fato, são infinitas,
mas para nós a existência de pelo menos uma já é suficiente.
3